This paper revisits the theory-independent MCSat framework as a proof system to provide a modern perspective that refines the original formulation of MCSat, and presents a general, theory-agnostic rule scheme for MCSat and instantiate it for several theories, including propositional logic, non-linear real arithmetic, and uninterpreted functions.
Abstract
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.
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.
Florian Pollitt, Mathias Fleury, Katalin Fazekas et al.· 0 citations
The satisfiability problem of propositional logic, SAT for short, is the first algorithmic problem that was shown to be NP-complete, and is the cornerstone of virtually all NP-completeness proofs. The SAT problem consists of deciding whether a given Boolean formula has a “solution”, in the sense of an assignment to the variables making the entire formula to evaluate to true. Over the last few years very powerful algorithms have been devised being able to solve SAT problems with hundreds of thousands of variables. For difficult (or randomly generated) formulas these algorithms can be compared to the proverbial search for the needle in a haystack. This book explains how such algorithms work, for example, by exploiting the structure of the SAT problem with an appropriate logical calculus, like resolution. But also algorithms based on “physical” principles are considered.
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.
Julian Danner, Martin Kreuzer· Journal of Artificial Intell...· 0 citations
We present a formal verification of an abstract transition-system presentation of the Davis-Putnam-Logemann-Loveland (DPLL) procedure in the Rocq proof assistant. Following Nieuwenhuis et al., SAT solving is modeled as a set of rule-based transitions between states rather than as a concrete algorithm. We formalize the syntax and semantics of propositional formulas, define the classical and base DPLL transition systems, and prove their key metatheoretic properties. In particular, we establish correctness and completeness with respect to satisfiability, and we prove termination by showing that the transition relation is well-founded. The formalization extends the original abstract system by also including the pure literal rule. Building on the verified transition system, we introduce an abstract notion of strategy and derive a terminating solver from any strategy satisfying suitable conditions. We then implement a concrete strategy in Rocq and show that it satisfies the strategy specification.
