Module pr 

The PR (propagation-redundancy) checker — the trust tier for model-removing clause additions, and the keystone that makes certified symmetry breaking possible.

RUP (crate::rup) certifies only clauses implied by the formula. A symmetry-breaking predicate is different in kind: it deletes satisfying assignments (keeping at least one per symmetry orbit), so it is satisfiability-preserving but not implied — RUP must and does reject it. Propagation redundancy (Heule, Kiesl & Biere, CADE 2017) closes exactly this gap: a clause C is redundant w.r.t. F with witness ω iff ω satisfies C and F|α ⊢₁ F|ω, where α = ¬C is the assignment falsifying C and ⊢₁ is implication by unit propagation. Adding such a C preserves satisfiability, with an independently checkable certificate.

Two witness forms are checked, each with its own well-specified criterion:

• Witness::Assignment ω — the classic PR criterion ω ⊨ C and F|α ⊢₁ F|ω. This is the general redundancy tier (vivification, BVE, …).
• Witness::Substitution σ — the substitution-redundancy criterion for a symmetry. Repair a model τ of F ∧ ¬C by composing with σ: the result τ∘σ satisfies F automatically when σ(F) = F, and satisfies C exactly when τ ⊨ σ(C). So C is redundant iff σ is an automorphism of the database AND F ∧ ¬C ⊢₁ σ(C) (Heule & Biere, substitution redundancy). The automorphism is checked against the current database, so an earlier predicate that breaks a later generator’s symmetry simply makes that check fail — fail-closed, no generator-ordering hazard.

The checker reuses the very same tiny unit-propagation core as crate::rup: its simplicity IS the trust, and it is wrapped by a brute-force equisatisfiability oracle over BOTH witness forms in the tests so it can never bless a clause that turns a satisfiable formula unsatisfiable.

Functions

check_pr_refutation

Verify a refutation made of ProofSteps over original. Each step’s added clause must check (RUP or PR) against the database built so far; then the empty clause must be RUP. Returns false if any step fails to check — a bogus or unsound proof is rejected.

check_pr_refutation_fast

check_pr_refutation accelerated by an incrementally-maintained AutomorphismIndex — the same verdict, but each substitution step’s automorphism re-check costs O(support) rather than O(|db|). Falls back to the stateless checker if the proof deletes clauses (the index is append-only, and certified symmetry refutations do not delete).

is_pr

Is clause propagation-redundant w.r.t. db under witness?

is_pr_indexed

is_pr with the automorphism re-check served by a pre-built incremental AutomorphismIndex (which must hold exactly the clauses of db). Identical verdict to is_pr — the index is an acceleration structure — but the substitution path no longer rebuilds the membership set per call, the difference between an O(n⁴) and an O(n³) certified refutation.