pub fn greedy_2sat_backdoor(clauses: &[Vec<Lit>], num_vars: usize) -> Vec<usize>Expand description
Greedily find a backdoor to 2-SAT: a set of variables U such that every clause has at most
two literals outside U. Then under any assignment to U, each clause is either satisfied or
shrinks to width ≤ 2, so the residual is 2-SAT — poly-decidable. Built by repeatedly fixing the
variable that appears in the most still-too-wide clauses (a hitting set of the wide clauses).