pub fn eliminate_variable(v: usize, clauses: &[Vec<Lit>]) -> Vec<Vec<Lit>>Expand description
Carve out a dimension. Eliminate variable v by resolution (Davis–Putnam): drop every clause
mentioning v, and add the non-tautological resolvents of each v-clause against each ¬v-clause.
Geometrically this projects the cube’s v-axis away — the formula over n dimensions becomes an
equisatisfiable one over n-1. Sound: a model of the projection lifts to a model of the original.