Module sym_certify 

Certified symmetry breaking — the centerpiece. Given a formula and a set of verified symmetry generators, add lex-leader symmetry-breaking predicates as PR steps (each self-checked, fail-closed), solve the augmented formula, and emit a single composed refutation that an independent checker accepts against the original formula alone.

This closes the soundness gap of the old path (where the symmetry-broken formula was RUP- certified but the model-removing addition was only argued informally): here every SBP clause carries a propagation-redundancy witness derived from its symmetry, so the whole UNSAT result — symmetry steps included — is machine-checkable. The decisive wiring invariant is that check_pr_refutation runs against formula ALONE; the SBP clauses appear only as PR steps, never as free original clauses.

Structs

CertifiedRefutation

The outcome of a certified-symmetry-breaking solve.

Functions

certified_unsat

Solve formula with certified symmetry breaking under the given generators (each must be a genuine automorphism — they are re-checked implicitly by the per-clause PR self-check).

certified_unsat_auto

Solve formula with FULL certified symmetry breaking, discovering the symmetries itself.

certified_unsat_lex

heule_clique_ranked

The steered clique-coloring refutation with its rank function attached — the analogue of heule_php_ranked over the coloring encoding, so a clique refutation also ships a checkable O(n²) size certificate (rank = active vertices remaining).

heule_clique_refutation

Full-chain structural steering of clique_coloring(n, k) (UNSAT for k < n): the Heule pigeonhole refutation transplanted onto the coloring encoding, wielding the a-priori vertex-swap symmetry rather than detecting it. k + 1 mutually-adjacent vertices already form a PHP(k+1, k), so the proof forces those k+1 vertices out of the colors one at a time — each clause ¬x(i, color) certified by the substitution “swap vertex i with the last active vertex”, whose SR check clashes at once on the corresponding at-most-one clause. The whole stream is verified against the original clique formula alone.

heule_php_ranked

The Heule PHP(n) refutation with its rank function attached — each symmetry-breaking step is tagged by the round (m = active items remaining) it belongs to, a non-increasing measure whose descent bounds the proof size. The closing RUP steps take the bottom rank 1. Feed the result to crate::complexity::RankedRefutation::certify to get a checkable O(n²) size bound alongside the correctness check.

heule_php_refutation

The Heule–Kiesl–Biere short PR refutation of PHP(n): a polynomial-size, fully certified proof — where the lex-leader provably cannot scale on UNSAT instances.

lex_leader_clauses

Build the full lex-leader symmetry-breaking predicate for sigma over the moved-variable order, enforcing x ≤ₗₑₓ σ(x). Returns the clauses (over base variables plus fresh auxiliary “tied-so-far” variables e_i, allocated starting at aux_start) and the number of aux variables used. This is the linear-size encoding that prunes the entire non-leader half of every σ-orbit — the real search-collapse predicate.

symmetry_break_certified

Solve formula with FULL certified lex-leader symmetry breaking. For each generator, add the complete lex-leader chain (enforcing x ≤ₗₑₓ σ(x)) as PR steps — each clause certified by a principled witness — then solve and append the learned clauses as RUP steps. This prunes the non-leader half of every σ-orbit (real search collapse), with the whole refutation checked against formula alone. A generator whose chain cannot be fully certified is skipped (fail-closed); the result stays sound. Augment formula with the certified full lex-leader symmetry-breaking clauses for each generator, committing a generator’s chain only when every clause of it certifies (else the generator is skipped — fail-closed). Returns the augmented clause set, the extended variable count (base + auxiliaries), and the PR proof steps that justify the added clauses. This is the symmetry-breaking front half shared by certified solving and by search-collapse measurement.