pub fn semantic_symmetry_pairs(
num_vars: usize,
clauses: &[Vec<Lit>],
) -> (Vec<(usize, usize)>, bool)Expand description
The semantic symmetries (variable transpositions) of a CNF: pairs (a,b) whose swap preserves the
MODEL SET, F ≡ swap(F), even when it does NOT preserve the clause set. Checked by implication: F ⊨ swap(F) (and, by the involution swap² = id, that is full equivalence). Returns the semantic pairs
and whether any is non-syntactic (clause set changed) — i.e. genuinely beyond what the syntactic
detector (crate::sym_break::variable_automorphism_generators) can see.