More Like this

1. Clausal Proofs for Pseudo-Boolean Reasoning

   https://doi.org/10.1007/978-3-030-99524-9_25  

   Bryant, Randal E.; Heule, Marijn J. (January 2022, International Conference on Tools and Algorithms for the Construction and Analysis of Systems)

   Fisman, D.; Rosu, G. (Ed.)

   When augmented with a Pseudo-Boolean (PB) solver, a Boolean satisfiability (SAT) solver can apply apply powerful reasoning methods to determine when a set of parity or cardinality constraints, extracted from the clauses of the input formula, has no solution. By converting the intermediate constraints generated by the PB solver into ordered binary decision diagrams (BDDs), a proof-generating, BDD-based SAT solver can then produce a clausal proof that the input formula is unsatisfiable. Working together, the two solvers can generate proofs of unsatisfiability for problems that are intractable for other proof-generating SAT solvers. The PB solver can, at times, detect that the proof can exploit modular arithmetic to give smaller BDD representations and therefore shorter proofs. 

   more » « less
2. Producing Proofs of Unsatisfiability with Distributed Clause-Sharing SAT Solvers

   https://doi.org/10.1007/s10817-025-09725-w  

   Michaelson, Dawn; Schreiber, Dominik; Heule, Marijn_J H; Kiesl-Reiter, Benjamin; Whalen, Michael W (June 2025, Journal of Automated Reasoning)

   Distributed clause-sharing SAT solvers can solve challenging problems hundreds of times faster than sequential SAT solvers by sharing derived information among multiple sequential solvers. Unlike sequential solvers, however, distributed solvers have not been able to produce proofs of unsatisfiability in a scalable manner, which limits their use in critical applications. In this work, we present a method to produce unsatisfiability proofs for distributed SAT solvers by combining the partial proofs produced by each sequential solver into a single, linear proof. We first describe a simple sequential algorithm and then present a fully distributed algorithm for proof composition, which is substantially more scalable and general than prior works. Our empirical evaluation with over 1500 solver threads shows that our distributed approach allows proof composition and checking within around 3x its own (highly competitive) solving time. 

   more » « less
3. Generating Extended Resolution Proofs with a BDD-Based SAT Solver

   https://doi.org/10.1007/978-3-030-72016-2_5  

   Bryant, Randal E.; Heule, Marijn J. (January 2021, Tools and Algorithms for the Construction and Analysis of Systems)

   Groote, J. F.; Larsen, K. G. (Ed.)

   In 2006, Biere, Jussila, and Sinz made the key observation that the underlying logic behind algorithms for constructing Reduced, Ordered Binary Decision Diagrams (BDDs) can be encoded as steps in a proof in the extended resolution logical framework. Through this, a BDD-based Boolean satisfiability (SAT) solver can generate a checkable proof of unsatisfiability. Such proofs indicate that the formula is truly unsatisfiable without requiring the user to trust the BDD package or the SAT solver built on top of it. We extend their work to enable arbitrary existential quantification of the formula variables, a critical capability for BDD-based SAT solvers. We demonstrate the utility of this approach by applying a prototype solver to obtain polynomially sized proofs on benchmarks for the mutilated chessboard and pigeonhole problems—ones that are very challenging for search-based SAT solvers. 

   more » « less
4. Strong Extension-Free Proof Systems

   https://doi.org/10.1007/s10817-019-09516-0  

   Heule, Marijn J.; Kiesl, Benjamin; Biere, Armin (February 2019, Journal of Automated Reasoning)

   We introduce proof systems for propositional logic that admit short proofs of hard formulas as well as the succinct expression of most techniques used by modern SAT solvers. Our proof systems allow the derivation of clauses that are not necessarily implied, but which are redundant in the sense that their addition preserves satisfiability. To guarantee that these added clauses are redundant, we consider various efficiently decidable redundancy criteria which we obtain by first characterizing clause redundancy in terms of a semantic implication relationship and then restricting this relationship so that it becomes decidable in polynomial time. As the restricted implication relation is based on unit propagation---a core technique of SAT solvers---it allows efficient proof checking too. The resulting proof systems are surprisingly strong, even without the introduction of new variables---a key feature of short proofs presented in the proof-complexity literature. We demonstrate the strength of our proof systems on the famous pigeon hole formulas by providing short clausal proofs without new variables. 

   more » « less
5. Simulating Strong Practical Proof Systems with Extended Resolution

   https://doi.org/10.1007/s10817-020-09554-z  

   Kiesl, Benjamin; Rebola-Pardo, Adrián; Heule, Marijn J.; Biere, Armin (July 2020, Journal of Automated Reasoning)

   Proof systems for propositional logic provide the basis for decision procedures that determine the satisfiability status of logical formulas. While the well-known proof system of extended resolution—introduced by Tseitin in the sixties—allows for the compact representation of proofs, modern SAT solvers (i.e., tools for deciding propositional logic) are based on different proof systems that capture practical solving techniques in an elegant way. The most popular of these proof systems is likely DRAT, which is considered the de-facto standard in SAT solving. Moreover, just recently, the proof system DPR has been proposed as a generalization of DRAT that allows for short proofs without the need of new variables. Since every extended-resolution proof can be regarded as a DRAT proof and since every DRAT proof is also a DPR proof, it was clear that both DRAT and DPR generalize extended resolution. In this paper, we show that—from the viewpoint of proof complexity—these two systems are no stronger than extended resolution. We do so by showing that (1) extended resolution polynomially simulates DRAT and (2) DRAT polynomially simulates DPR. We implemented our simulations as proof-transformation tools and evaluated them to observe their behavior in practice. Finally, as a side note, we show how Kullmann’s proof system based on blocked clauses (another generalization of extended resolution) is related to the other systems. 

   more » « less