Factoring Learned Clauses

Conflict-Driven SAT Solving using XOR-OR-AND Normal Forms

Background: Classical solvers for Boolean polynomial systems are usually based on the Conjunctive Normal Form (CNF) and the resolution calculus, or on the algebraic normal form (ANF) and the polynomial calculus, i.e., on Gröbner basis methods. Here we develop a new solver which is based on the XOR-OR-AND normal form (XNF) and the XLIN proof system. XNF formulae allow compact encodings of XOR-rich problems, which, for instance, occur naturally in cryptography. Objectives: The paper has the following goals: lay a solid complexity-theoretic foundation for the new propositional logic proof system XLIN, devise XLIN-based conflict learning methods for formulae in XNF, create a variant of this framework optimized for practical efficiency, implement it in an actual solver called Xorricane, and finally apply this solver to benchmark suites consisting of random examples and cryptographic examples to prove its viability. Methods: As a first step, we show that the new propositional logic proof system XLIN is polynomially equivalent equivalent to the well-studied proof systems RES(⊕) and SRES. It follows that there is an exponential separation between XLIN and the CNF-based resolution proof system RES. In the next step, we devise XLIN-based conflict-learning methods for formulae in XNF which are analogous to the CDCL methods of classical SAT solvers. Using Gaußian Constraint Propagation and a suitable version of conflict analysis, we obtain a conflict-driven framework CDXCL for XNF SAT-solving. To ensure practical efficiency, we also present a variant, called CDXCLlite, which uses a weaker propagation mechanism but retains the same learning method. Results: These theoretical advances result in Xorricane, an implementation of the latter XNF SAT-solving framework featuring novel lazy data structures. This implementation is compared to state-of-the-art algebraic and logic solving approaches on random and cryptographic benchmark suites. Although it still lacks several optimizations, it performs well on the benchmark problems and matches or outperforms modern CNF and CNF-XOR based SAT-solvers for XOR-rich problem instances. Conclusions: Solving Boolean polynomial systems, or equivalently, SAT-solving, based on the XNF and the XLIN proof system outperforms classical methods not only theoretically, but based on the new conflict-driven XNF clause learning methods developed here, it is possible to implement an XNF solver with good practical efficiency. The advantage of XNF-based SAT-solving is strongest for XOR-rich examples such as the ones derived from cryptographic attacks.

CaDiCaL 3.0

This system description reports on how Kissat’s award-winning techniques were adapted to the full-featured incremental SAT solver CaDiCaL, including clausal congruence closure, clausal equivalence sweeping, and bounded variable addition, to support efficient linear proof production with hints.

From Literals to Atomic Constraints: Generalising Conflict-Driven Clause Learning for Constraint Programming

This work presents the first systematic analysis of how leading LCG solvers maintain their SAT encodings, based on source-code inspection and developer correspondence, and proposes a native CDCL framework for CP, replacing SAT literals with atomic constraints, enabling conflict analysis, nogood learning, and nogood propagation directly at the CP level.

PALSAT: Deep Cooperation of Unit Propagation and Local Search in Incomplete SAT Solving

Conditional Autarkies: Hard Formulas Made Easy

From LLM Suggestions to Lean Proofs: Verified Redundant Constraints for MiniZinc

This work presents a pipeline that combines LLM-based constraint generation with empirical evaluation and formal verification, and handles MiniZinc’s partial semantics by requiring the base model to be safe and separately proving that the proposed constraint is well-defined for all instances and solutions of the base model.