Module symmetry_detect 

General symmetry detection for CNF — the engine behind certified symmetry breaking.

A symmetry of a formula is a literal permutation σ (respecting negation) that maps the clause set onto itself: σ(F) = F. Such a σ permutes models, so adding a lex-leader predicate that keeps the canonical representative of each orbit is satisfiability-preserving — and, with the witness σ, independently certifiable by the PR checker (crate::pr).

The cornerstone is the soundness gate perm_is_automorphism: whatever search produces a candidate generator, it is re-verified here by clause-multiset invariance before any use. A detector that emits a non-symmetry is caught and dropped; a detector that misses a symmetry only costs search speed. So the intricate part — finding generators — is never soundness-critical; this gate is.

Structs

AutomorphismIndex

An incrementally-maintained clause database for fast repeated automorphism checks.

Functions

aut_order

|Aut(F)| — the exact number of formula automorphisms, via the Schreier–Sims backend.

automorphism_group

The formula’s automorphism group as a BSGS — Schreier–Sims as the symmetry backend. The detected generators (find_generators) are bridged to permutations of the 2·num_vars literal points and a base + strong generating set is built, so the symmetry layer can compute |Aut(F)| (crate::permgroup::Bsgs::order) and decide membership / cosets (crate::permgroup::Bsgs::contains) in polynomial time — group computations it previously could not do (it worked only with the raw generators). The stabilizer chain is the symmetry break, generalized from the abelian linear engines to an arbitrary (non-abelian) permutation group.

find_generators

Find a generating set of the symmetry group of clauses — literal permutations σ with σ(F) = F. Each returned generator is independently verified by perm_is_automorphism.

perm_is_automorphism

Is sigma a genuine automorphism of clauses — does applying it map the clause set exactly onto itself? The independent re-verification every generator must pass.