pub fn carve(num_vars: usize, clauses: &[Vec<Lit>]) -> CarveOutcomeExpand description
Carve away the hypercube. Peel the formula down by the three classic simplifications, iterated to a fixpoint: unit propagation (a unit clause carves the cube in half by forcing a variable), pure-literal assignment (carves an autark section), and subsumption (drops a blocker contained in a stronger one). All three preserve satisfiability, so the result is either a verdict or the irreducible core that genuine hardness leaves behind. Pigeonhole carves to itself.