pub fn restrict(
clauses: &[Vec<Lit>],
assignment: &[Option<bool>],
) -> Vec<Vec<Lit>>Expand description
The residual CNF after fixing variables: assignment[v] = Some(b) fixes v, None leaves it
free. Clauses satisfied by a fixed literal are dropped; falsified literals are removed. An empty
clause in the result means the restriction already falsifies the formula.