Beyond Core-Guided MaxSAT

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.

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.

Factoring Learned Clauses

This paper revisits previous work on ER, which factors out repeated parts of learned clauses during conflict analysis, and explores how their original strategy benefits from 15 years of improvements in the state-of-the-art solver CaDiCaL, and proposes a new, less intrusive inprocessing approach based on factoring XOR and ITE gates from learned clauses globally.

A Modern View on MCSat

The Model Constructing Satisfiability (MCSat) approach has shown strong performance in solving complex SMT problems, in particular in algebraic SMT theories such as non-linear integer and real arithmetic. In this paper we revisit the theory-independent MCSat framework as a proof system to provide a modern perspective that refines the original formulation of MCSat. By closely formalizing the implementation of MCSat within the Yices2 SMT solver, we incorporate design decisions that diverge from those in the seminal MCSat paper and thereby capture the current state-of-the-art in MCSat-based SMT reasoning. We present a general, theory-agnostic rule scheme for MCSat and instantiate it for several theories, including propositional logic, non-linear real arithmetic, and uninterpreted functions. We provide several detailed examples to illustrate the applicability of the presented calculus.

SAT in Saturation: A Satisfied Match

CaDiCaL 3.0