pub fn color_refinement(num_vars: usize, clauses: &[Vec<Lit>]) -> Vec<usize>Expand description
Color refinement (1-dimensional Weisfeiler–Leman) of a formula’s variable–clause incidence graph —
the coarsest equitable partition of the variables, computed in polynomial time. Variables and clauses
are coloured (clauses initialised by width); each round recolours a clause by the sorted multiset of its
incident (variable colour, sign) pairs and a variable by the sorted multiset of its incident
(clause colour, sign) pairs, to a fixpoint. The result cell[v] is the variable’s colour.
This is the polynomial foundation of symmetry detection (the pre-filter saucy/nauty run before the
exponential search) and a SOUND over-approximation of the orbit partition: every phase-free variable
automorphism preserves the colouring, so orbit(v) ⊆ cell(v) — variables of different colours are
provably in different orbits. Returns dense cell indices 0..k.