Module sym_dynamic 

Dynamic symmetry breaking — Symmetric Explanation Learning (SEL), the in-search tier.

Static symmetry breaking adds predicates up front (Phase 1). SEL is reactive: it watches what the solver learns and multiplies each learned clause by the formula’s symmetry group, so the search never has to re-derive the symmetric twin of a lemma it already paid for. On a symmetry-rich UNSAT instance that is the whole game — the exponential blow-up resolution suffers is exactly the repeated rediscovery of symmetric variants.

The certification is free. If a learned clause C is RUP w.r.t. the database and σ is an automorphism of that database, then σ(C) is RUP too: apply σ to C’s unit-propagation refutation and every clause it touches maps back into σ(F) = F. So a symmetric clause enters the proof as a plain ProofStep::Rup — DRAT/LRAT-checkable, no PR witness needed. We add a σ(C) only after re-confirming it is RUP against the current database (rup::is_rup), so the procedure is fail-closed: an amplification that does not check is silently dropped, never trusted.

The loop alternates a conflict-budgeted solve (Solver::solve_budgeted) with an amplification pass over the round’s learned clauses, accumulating a single RUP refutation that crate::pr::check_pr_refutation_fast verifies against the original formula alone.

Enums

SelOutcome

The result of an SEL refutation attempt.

Functions

sel_refute

Refute clauses with Symmetric Explanation Learning, or report SAT / Unknown. The conflict budget per round and the round cap bound the work; symmetric amplification is what makes the total conflict count collapse on symmetry-rich instances.