Module symmetry 

Symmetry breaking for the general solver — the second pillar (with crate::pigeonhole cardinality reasoning) for winning on pigeonhole.

CDCL refutes a symmetric UNSAT formula by re-deriving the same conflict once per symmetric copy of the problem — for the pigeonhole principle the pigeons are interchangeable, so the refutation cost is multiplied by n!. Adding sound symmetry-breaking predicates (SBPs) collapses each symmetry orbit to a single lexicographically-least representative, so the solver searches the quotient instead of the whole symmetric space.

We detect a cheap, sound class: ROW-INTERCHANGE symmetries. The at-least-one rows of a pigeonhole-shaped formula (positive clauses over disjoint variable blocks) are candidate interchangeable units; for each adjacent pair we verify the column-aligned row swap is a genuine automorphism of the entire clause set (apply the swap, check the clause multiset is invariant) before adding the lex-leader “row i ≤ₗₑₓ row i+1” SBP.

Soundness. A verified automorphism σ leaves the formula F invariant, so the lex-leader SBP_σ preserves satisfiability (it keeps the lex-least model of each orbit). Hence F ∧ SBP_σ is UNSAT iff F is — refuting the augmented formula refutes the original. The lex-leader encoding is pinned exhaustively against a brute-force oracle, and we add an SBP only for a swap we have proven is an automorphism; a wrong symmetry could delete the only model, so verified-or-nothing.

Functions

break_symmetries

Augment e with lex-leader SBPs for every adjacent row-interchange symmetry we can verify. Returns e unchanged when the formula is not a readable clause set, has no rows, or no verified symmetry — symmetry breaking is purely additive and never changes the SAT/UNSAT verdict.

lex_le

“X ≤ₗₑₓ Y” over equal-length boolean vectors (false < true), MSB-first: at the first index where they differ, X has false and Y has true. Encoded with a chain of “equal-so-far” auxiliaries {aux}_eq_{k} (distinct constraints must use distinct aux). Returns a tautology for empty/ length-1-or-shorter vectors handled position-by-position.