More Like this

1. Preprocessing of Propagation Redundant Clauses

   https://doi.org/10.1007/978-3-031-10769-6_8  

   Reeves, Joseph E.; Bryant, Randal E.; Heule, Marijn J. (August 2022, Lecture notes in computer science)

   Blanchette, Jasmin; Kovacs, Laura; Pattinson, Dirk (Ed.)

   The propagation redundant (PR) proof system generalizes the resolution and resolution asymmetric tautology proof systems used by conflict-driven clause learning (CDCL) solvers. PR allows short proofs of unsatisfiability for some problems that are difficult for CDCL solvers. Previous attempts to automate PR clause learning used hand-crafted heuristics that work well on some highly-structured problems. For example, the solver SaDiCaL incorporates PR clause learning into the CDCL loop, but it cannot compete with modern CDCL solvers due to its fragile heuristics. We present prExtract, a preprocessing technique that learns short PR clauses. Adding these clauses to a formula reduces the search space that the solver must explore. By performing PR clause learning as a preprocessing stage, PR clauses can be found efficiently without sacrificing the robustness of modern CDCL solvers. On a large portion of SAT competition benchmarks we found that preprocessing with prExtract improves solver performance. In addition, there were several satisfiable and unsatisfiable formulas that could only be solved after preprocessing with prExtract. prExtract supports proof logging, giving a high level of confidence in the results. 

   more » « less
2. G2SAT: Learning to Generate SAT Formulas

   You, J.; Wu, H.; Barrett, C.; Ramanujan, R.; Leskovec, J. (December 2019, Advances in neural information processing systems)

   The Boolean Satisfiability (SAT) problem is the canonical NP-complete problem and is fundamental to computer science, with a wide array of applications in planning, verification, and theorem proving. Developing and evaluating practical SAT solvers relies on extensive empirical testing on a set of real-world benchmark formulas. However, the availability of such real-world SAT formulas is limited. While these benchmark formulas can be augmented with synthetically generated ones, existing approaches for doing so are heavily hand-crafted and fail to simultaneously capture a wide range of characteristics exhibited by real-world SAT instances. In this work, we present G2SAT, the first deep generative framework that learns to generate SAT formulas from a given set of input formulas. Our key insight is that SAT formulas can be transformed into latent bipartite graph representations which we model using a specialized deep generative neural network. We show that G2SAT can generate SAT formulas that closely resemble given real-world SAT instances, as measured by both graph metrics and SAT solver behavior. Further, we show that our synthetic SAT formulas could be used to improve SAT solver performance on real-world benchmarks, which opens up new opportunities for the continued development of SAT solvers and a deeper understanding of their performance. 

   more » « less
3. 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
4. From Clauses to Klauses

   Reeves, Joseph E; Heule, Marijn; Bryant, Randal E (July 2024, International Conference on Computer Aided Verification (CAV-24))

   Satisfiability (SAT) solvers have been using the same input format for decades: a formula in conjunctive normal form. Cardinality constraints appear frequently in problem descriptions: over 64% of the SAT Competition formulas contain at least one cardinality constraint, while over 17% contain many large cardinality constraints. Allowing general cardinality constraints as input would simplify encodings and enable the solver to handle constraints natively or to encode them using different (and possibly dynamically changing) clausal forms. We modify the modern SAT solver CaDiCaL to handle cardinality constraints natively. Unlike the stronger cardinality reasoning in pseudo-Boolean (PB) or other systems, our incremental approach with cardinality-based propagation requires only moderate changes to a SAT solver, preserves the ability to run important inprocessing techniques, and is easily combined with existing proof-producing and validation tools. Our experimental evaluation on SAT Competition formulas shows our solver configurations with cardinality support consistently outperform other SAT and PB solvers. 

   more » « less
5. Local Search for Fast Matrix Multiplication

   https://doi.org/10.1007/978-3-030-24258-9_10  

   Heule, Marijn; Kauers, Manuel; Seidl, Martina (June 2019, International Conference on Theory and Applications of Satisfiability Testing)

   Laderman discovered a scheme for computing the product of two 3 x 3 matrices using only 23 multiplications in 1976. Since then, some more such schemes were proposed, but nobody knows how many such schemes there are and whether there exist schemes with fewer than 23 multiplications. In this paper we present two independent SAT-based methods for finding new schemes using 23 multiplications. Both methods allow computing a few hundred new schemes individually, and many thousands when combined. Local search SAT solvers outperform CDCL solvers consistently in this application. 

   more » « less