pub fn canonical_form(
num_vars: usize,
clauses: &[Vec<Lit>],
) -> Option<Vec<Vec<(usize, bool)>>>Expand description
The canonical form of a formula’s variable structure, computed by individualization–refinement (the
algorithm behind nauty/saucy/bliss). It is an isomorphism invariant: two formulas equal up to a
variable permutation that preserves the clause structure have the same canonical form, and — since
I-R is complete — two that are not get different canonical forms (so it decides isomorphism exactly,
unlike Weisfeiler–Leman). Built on color_refinement as its refinement step. None if the search
exceeds its node budget (gate to moderate num_vars).