pub fn bounded_variable_elimination(
num_vars: usize,
clauses: &[Vec<Lit>],
) -> Vec<Vec<Lit>>Expand description
Bounded variable elimination — carve away every dimension whose projection doesn’t grow the formula (resolvents ≤ clauses removed). Iterated to a fixpoint, it peels the cube down dimension by dimension wherever it’s free to do so; the variables that would explode (pigeonhole’s, by Haken) are left for the cuts. Satisfiability-preserving.