pub fn provably_asymmetric_variables(
num_vars: usize,
clauses: &[Vec<Lit>],
) -> Vec<usize>Expand description
The variables that color refinement places in a singleton cell — provably fixed by every (phase-free)
automorphism, since orbit(v) ⊆ cell(v) and |cell(v)| = 1 forces |orbit(v)| = 1. A polynomial
certificate of asymmetry: these variables can be skipped entirely when detecting or breaking symmetry.