pub fn eliminate_variable(
clauses: &[Vec<Lit>],
x: Var,
) -> Option<(Vec<Vec<Lit>>, Vec<ProofStep>)>Expand description
Try to eliminate variable x from clauses by Davis-Putnam resolution. Returns the new clause
set and the proof steps (RUP resolvents, then the deletions of x’s clauses) — but only when
x actually occurs and elimination does not grow the clause count (the standard BVE bound).
None otherwise. Verdict-invariant: a model of the result extends to a model of the input.