pub fn components(num_vars: usize, clauses: &[Vec<Lit>]) -> Vec<Vec<Vec<Lit>>>Expand description
Partition a formula into its independent components — maximal clause groups sharing no variable (the connected components of the variable-interaction graph). The formula is the conjunction of its components, so it is UNSAT iff any component is, and each can be attacked on its own. A structured UNSAT component buried in a big mixed formula — invisible to the monolithic cut — is laid bare here.