Module sdcl 

Satisfaction-Driven Clause Learning (Heule, Kiesl & Seidl) — the engine that reasons at the Extended-Frege level by discovering propagation-redundant clauses, not just learning implied ones. It is symmetry breaking taken to its limit: where certified symmetry breaking needs an automorphism to supply a witness, SDCL finds the witness by solving the positive reduct — a smaller SAT problem — so it works on any structure, symmetric or not.

When the search is stuck at a partial assignment α it cannot extend, the clause C = ¬α would block that subtree. C is propagation-redundant iff the positive reduct {C} ∪ {D ∈ F : α ⊨ D} is satisfiable; a satisfying ω is the witness. Every clause this finds is gated through the independent PR checker (crate::pr::is_pr), so it is sound by construction and emits a checkable PR step — the same machine-checkable currency as the rest of the campaign.

Enums

CertifiedOutcome

The verdict of the unified certified solver.

Functions

find_pr_clause

From a “stuck” partial assignment alpha (its true-literals), try to discover a PR clause C = ¬alpha that blocks it, via the positive reduct. Returns the clause and its witness, both verified by the PR checker (fail-closed). This is the SDCL primitive — a universal, automorphism-free generalization of certified symmetry breaking.

find_pr_clause_unified

The unified PR-clause finder: the universal SDCL discovery (positive-reduct assignment witness) PLUS the scalable symmetry path (substitution witnesses from the supplied generators). The assignment witness is general but can fail to certify at scale (it needs F|α UP-refutable); a substitution witness from a live automorphism certifies the lead clauses at any size via an immediate conflict. Trying both gives SDCL that discovers AND scales.

plain_cdcl_refutation

A plain CDCL refutation of clauses as RUP proof steps — always re-checkable. The certified fallback that guarantees solve_certified and sdcl_refute never emit an unchecked proof, and the universal source of a cake_lpr-checkable LRAT certificate for any UNSAT instance.

sdcl_refute

solve_certified

The unified certified solver — the apex of the campaign. Given ANY formula it (1) auto-discovers propagation-redundant clauses via SDCL (positive reduct + live symmetry), then (2) solves the augmented formula with the modernized CDCL core. On UNSAT it returns a single machine-checked refutation composed of every step; on SAT a model (valid for the original, since SDCL only adds satisfiability-preserving clauses). Symmetry breaking, SDCL, and CDCL, fused into one certified engine.