2026· International Conference on Theory and Applications of Satisfiability Testing· pp. 8:1-8:18· 0 citations· 29 references
Computer Science
TL;DR
It is shown that adding conditional autarkies (as set-blocked clauses) on top of resolution allows efficient refutations of a number of natural combinatorial principles that may occur in SAT benchmarks.
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.
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.
Florian Pollitt, Zachary Battleman, Mathias Fleury et al.· International Conference on...· 1 citation
The top-down solver TD is a generic fixpoint algorithm that can be used to compute partial post-solutions of equation systems for abstract interpretation. We consider two extensions of the TD to deal with infinite strictly ascending chains. For the TD extended with warrowing, we formally prove that it always returns partial post-solutions, while for the TD extended with widening and narrowing in phases, we prove termination provided that the set of unknowns is finite. By proving the equivalence of the two extensions, we deduce the total correctness of both solvers. For the equivalence to hold, we in particular assume the equation system to have right-hand sides that are both monotonic and have monotonic dependencies. We demonstrate with counterexamples that the violation of any of the assumptions may compromise the equivalence. All proofs have been formalized using the interactive theorem prover Isabelle.
Sarah Tilscher, Alexandra Graß, Helmut Seidl et al.· Journal of automated reasoni...· 0 citations
A proof checker called Nörgler is introduced that builds upon and extends the established approach pioneered by GDV and supports checking propositional, (untyped and typed) first-order, and higher-order refutations represented in TSTP.
Melanie Taprogge, H. Sariyanto, Alexander Steen· 0 citations
A tailored integration of SAT solving for detecting variants of subsumption in superposition using the Vampire prover and showing that SAT encodings improve literal matching, and thus subsumption, in first-order theorem proving is presented.
Laura Kovács, Tu Wien, Austria et al.· 0 citations
We use cookies to run the site and, with your consent, for analytics and to show ads.
See our Cookie Policy.
