More Like this

1. Propositional Proof Skeletons

   https://doi.org/10.1007/978-3-031-30823-9_17  

   Reeves, Joseph E.; Kiesl-Reiter, Benjamin; Heule, Marijn J. (April 2023, Springer)

   Sankaranarayanan, S.; Sharygina, N. (Ed.)

   Modern SAT solvers produce proofs of unsatisfiability to justify the correctness of their results. These proofs, which are usually represented in the well-known DRAT format, can often become huge, requiring multiple gigabytes of disk storage. We present a technique for semantic proof compression that selects a subset of important clauses from a proof and stores them as a so-called proof skeleton. This proof skeleton can later be used to efficiently reconstruct a full proof by exploiting parallelism. We implemented our approach on top of the award-winning SAT solver CaDiCaL and the proof checker DRAT-trim. In an experimental evaluation, we demonstrate that we can compress proofs into skeletons that are 100 to 5,000 times smaller than the original proofs. For almost all problems, proof reconstruction using a skeleton improves the solving time on a single core, and is around five times faster when using 24 cores. 

   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. 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
4. Satisfiability Modulo Theories: A Beginner’s Tutorial

   https://doi.org/10.1007/978-3-031-71177-0_31  

   Barrett, Clark; Tinelli, Cesare; Barbosa, Haniel; Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Zohar, Yoni (September 2024, Springer Nature Switzerland)

   Platzer, Andre; Rozier, Kristin Yvonne; Pradella, Matteo; Rossi, Matteo (Ed.)

   Abstract Great minds have long dreamed of creating machines that can function as general-purpose problem solvers. Satisfiability modulo theories (SMT) has emerged as one pragmatic realization of this dream, providing significant expressive power and automation. This tutorial is a beginner’s guide to SMT. It includes an overview of SMT and its formal foundations, a catalog of the main theories used in SMT solvers, and illustrations of how to obtain models and proofs. Throughout the tutorial, examples and exercises are provided as hands-on activities for the reader. They can be run using either Python or the SMT-LIB language, using either thecvc5or the Z3 SMT solver. 

   more » « less
5. Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification

   https://doi.org/10.23919/DATE54114.2022.9774587  

   Kaufmann, Daniela; Beame, Paul; Biere Armin; Nordstrom, Jakob (March 2022, 2022 Design, Automation & Test in Europe Conference & Exhibition (DATE))

   Bolchini, Cristiana; Verbauwhede, Ingrid; Vatajelu, Ioana (Ed.)

   Algebraic reasoning has proven to be one of the most effective approaches for verifying gate-level integer multipliers, but it struggles with certain components, necessitating the complementary use of SAT solvers. For this reason validation certificates require proofs in two different formats. Approaches to unify the certificates are not scalable, meaning that the validation results can only be trusted up to the correctness of compositional reasoning. We show in this paper that using dual variables in the algebraic encoding, together with a novel tail substitution and carry rewriting method, removes the need for SAT solvers in the verification flow and yields a single, uniform proof certificate. 

   more » « less