Skip to main content

semantic_symmetry_pairs

Function semantic_symmetry_pairs 

Source
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.