Volume
LIPIcs, Volume 377
29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)
Event
Editors
- Department of Data Science and Artificial Intelligence, Monash University, Clayton, Australia
Publication Details
- published at: 2026-07-16
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-431-4
Access Numbers
- Detailed Access Statistics available here
-
Total Accesses (updated on a weekly basis)
0Documents
Documents
No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 377, SAT 2026, Complete Volume
Abstract
LIPIcs, Volume 377, SAT 2026, Complete Volume
Cite as
29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 1-730, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@Proceedings{ignatiev_et_al:LIPIcs.SAT.2026,
title = {{LIPIcs, Volume 377, SAT 2026, Complete Volume}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {1--730},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026},
URN = {urn:nbn:de:0030-drops-270346},
doi = {10.4230/LIPIcs.SAT.2026},
annote = {Keywords: LIPIcs, Volume 377, SAT 2026, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 0:i-0:xx, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{ignatiev_et_al:LIPIcs.SAT.2026.0,
author = {Ignatiev, Alexey and Szeider, Stefan},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {0:i--0:xx},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.0},
URN = {urn:nbn:de:0030-drops-263060},
doi = {10.4230/LIPIcs.SAT.2026.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
SAT in Saturation: A Satisfied Match (Invited Talk)
Abstract
Saturation is the leading concept behind the proof-search algorithms of state-of-the-art first-order theorem provers [Filip Bártek et al., 2025; Christoph Weidenbach et al., 2009; Stephan Schulz et al., 2019]. The key idea behind saturation-based proof search is to reduce the problem of proving validity of a first-order formula to the problem of establishing unsatisfiability of the respective formula, by using a sound inference system, such as resolution and superposition [Leo Bachmair and Harald Ganzinger, 2001; Robert Nieuwenhuis and Albert Rubio, 2001]. Central to efficient saturation-based proof search is the implementation of redundancy in the form of simplification rules [John Alan Robinson, 1965; Laura Kovács and Andrei Voronkov, 2013]: such rules do not add new formulas to search space, but instead simplify/delete redundant formulas from the search space, while not loosing refutational completeness of superposition. Redundancy in first-order theorem proving is controlled via term/clause ordering and literal selection functions in extension of standard superposition: redundant clauses are logical consequences of smaller clauses with respect to the considered ordering.
While redundancy is essential for efficient proof search, establishing whether an arbitrary first-order formula is redundant is as hard as proving whether it is valid. First-order provers therefore implement sufficient conditions towards proving redundancy, so that these conditions can be efficiently checked, ideally using only syntactic arguments over formulas. One such condition comes with the notion of subsumption, yielding one of the most important simplification rules in automated reasoners [Leo Bachmair and Harald Ganzinger, 1994]. It is common that millions of subsumption checks are performed during a single solver run [Jakob Rath et al., 2022]. However, in contrast to propositional subsumption as used by SAT solvers and implemented using sophisticated polynomial algorithms, first-order subsumption in first-order theorem proving involves NP-complete search queries, turning the efficient use of first-order subsumption into a huge practical burden.
This talks presents a tailored integration of SAT solving for detecting variants of subsumption in superposition. Key to our approach is retrieving clauses from the search space and checking whether subsumption with retrieved clauses can be applied, using multi-literal matching. A solution to our SAT-based encoding gives a concrete application of (variants of) subsumption, allowing the first-order prover to apply that instance of subsumption as a simplification rule during saturation [Bernhard Gleiss et al., 2020; Jakob Rath et al., 2022; Robin Coutelier et al., 2025]. Our SAT encoding captures subset relations among literals/clauses and formalizes matching of literals between inference premises/conclusions. We show that SAT encodings improve literal matching, and thus subsumption, in first-order theorem proving. In particular, our experimental results using the Vampire prover demonstrate the practical benefits of using SAT solving for variants of first-order subsumption.
Cite as
Laura Kovács. SAT in Saturation: A Satisfied Match (Invited Talk). In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{kovacs:LIPIcs.SAT.2026.1,
author = {Kov\'{a}cs, Laura},
title = {{SAT in Saturation: A Satisfied Match}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {1:1--1:2},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.1},
URN = {urn:nbn:de:0030-drops-263076},
doi = {10.4230/LIPIcs.SAT.2026.1},
annote = {Keywords: Automated Reasoning, First-Order Theorem Proving, Superposition, Subsumption, Redundancy, SAT Solving, Vampire}
}
Document
Invited Talk
Trustable Explainable AI - SAT to the Rescue (Invited Talk)
Abstract
Explainable Artificial Intelligence (XAI) aims to help human decision makers in understanding the operation of complex AI models. However, many XAI solutions, based on non-symbolic methods, offer no formal guarantees and can produce erroneous results. In contrast, logic-based XAI guarantees the rigor of computed explanations, and this is paramount in high-stakes uses of AI. This talk overviews several flagship applications of Boolean satisfiability (SAT) solvers in reasoning about logic-based explanations.
Cite as
Joao Marques-Silva. Trustable Explainable AI - SAT to the Rescue (Invited Talk). In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 2:1-2:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{marquessilva:LIPIcs.SAT.2026.2,
author = {Marques-Silva, Joao},
title = {{Trustable Explainable AI - SAT to the Rescue}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {2:1--2:10},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.2},
URN = {urn:nbn:de:0030-drops-263086},
doi = {10.4230/LIPIcs.SAT.2026.2},
annote = {Keywords: Explainable AI, Boolean Satisfiability}
}
Document
Proof Systems for QBF Synthesis: Extracting Skolem and Herbrand Functions
Abstract
Strategy extraction in QBF proof systems usually attempts to extract winning strategies from valid proofs. However, an alternative (and arguably more powerful) view is to extract Skolem/Herbrand functions, or equivalently synthesis of the game values at all intermediate points. In this paper, we investigate the existence and properties of such proof systems from which one can extract Skolem and Herbrand functions. We propose such a proof system for QBF, which we show is sound and complete, and from which extraction of Skolem/Herbrand functions can be performed, and game values computed, in polynomial time. We also show that this system is optimal among all proof systems that allow efficient extraction of Skolem/Herbrand functions. We provide conditional lower bound results for our new proof system and compare it to several existing/standard proof systems for QBF that have been studied in the literature, showing interesting orthogonality results. Finally, we provide a compilation algorithm that takes an arbitrary QBF and synthesizes a proof in our system, from which Skolem and Herbrand functions can be easily computed.
Cite as
S. Akshay, Olaf Beyersdorff, Supratik Chakraborty, Lea Kasche, Meena Mahajan, and Luc Nicolas Spachmann. Proof Systems for QBF Synthesis: Extracting Skolem and Herbrand Functions. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 3:1-3:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{akshay_et_al:LIPIcs.SAT.2026.3,
author = {Akshay, S. and Beyersdorff, Olaf and Chakraborty, Supratik and Kasche, Lea and Mahajan, Meena and Spachmann, Luc Nicolas},
title = {{Proof Systems for QBF Synthesis: Extracting Skolem and Herbrand Functions}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {3:1--3:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.3},
URN = {urn:nbn:de:0030-drops-263096},
doi = {10.4230/LIPIcs.SAT.2026.3},
annote = {Keywords: Quantified Boolean Formulas, Skolem and Herbrand functions, Automated synthesis, Knowledge compilation, Proof systems and complexity}
}
Document
Simplify, Order, Break, Repeat
Abstract
Existing symmetry-breaking techniques for SAT constrain the search space without simplifying the formula. Lex-leader predicates, the most widely used approach, add global ordering constraints to remove symmetric solutions, but often at the cost of substantial formula blowup and large proofs. Moreover, they ignore structural properties of the formula, such as connectedness, that could enable stronger symmetry breaking. In this paper, we present a new algorithm that treats symmetry breaking not merely as a restriction mechanism, but as a simplification mechanism. Notably, it only adds unit and binary symmetry-breaking clauses, which enables strong formula simplifications. This can expose additional symmetries and in turn allows for multiple rounds of symmetry breaking. Crucially, we exploit connectivity in the formula’s graph representation, including the presence of cliques, to guide the order of symmetry breaking. We implemented our algorithm in the satsuma tool and evaluated it on a large set of benchmarks. As a preprocessing step for CaDiCaL, it improves PAR-2 scores by 22% on the SAT competition 2025 and by 12% on the SAT anniversary track. It also substantially outperforms lex-leader and orbitopal fixing while producing compact proofs.
Cite as
Markus Anders, Cayden Codel, and Marijn J. H. Heule. Simplify, Order, Break, Repeat. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 4:1-4:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{anders_et_al:LIPIcs.SAT.2026.4,
author = {Anders, Markus and Codel, Cayden and Heule, Marijn J. H.},
title = {{Simplify, Order, Break, Repeat}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {4:1--4:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.4},
URN = {urn:nbn:de:0030-drops-263109},
doi = {10.4230/LIPIcs.SAT.2026.4},
annote = {Keywords: Boolean satisfiability, symmetry handling, preprocessing, Schreier-Sims}
}
Document
Extending CDCL to Disjunctions of Parity Equations
Abstract
Because CDCL produces proofs in the Resolution proof system, problems provably hard for Resolution are also provably hard for CDCL. Exponentially shorter proofs can sometimes be found using stronger proof systems such as Res(⊕), a generalization of Resolution to XNF formulas, whose constraints are disjunctions of parity equations ("linear clauses") such as (x ⊕ y)∨¬(y ⊕ z). While some modern solvers like CryptoMiniSAT reason on Boolean clauses with separate parity equations, reasoning about more general linear clauses is less explored.
We present CDCL(⊕), a generalization of CDCL to XNF formulas, and prove a bidirectional connection with Res(⊕): CDCL(⊕) not only produces Res(⊕) proofs, but also polynomially simulates Res(⊕) given nondeterministic decisions and restarts, mirroring the classical relationship between CDCL and Resolution. Our key technical tool is a new set of inference rules for Res(⊕) that helps us translate Resolution-based subroutines such as 1-UIP clause learning. Altogether, CDCL(⊕)’s parity reasoning includes branching on arbitrary parity equations, linear-algebraic reasoning during unit propagation, and learning linear clauses through conflict analysis.
We provide a proof-of-concept implementation of CDCL(⊕) called Xorcle, which includes adaptations of existing CDCL heuristics to XNF formulas and an extension of LRUP proof logging that we call LRUP(⊕). On a selected suite of benchmarks focusing on native XNF formulas, Xorcle outperforms existing solvers such as Kissat and CryptoMiniSAT. Additionally, on Tseitin formulas written in CNF, even without preprocessing, Xorcle’s running time appears to scale nearly polynomially.
Cite as
Paul Beame and Glenn Sun. Extending CDCL to Disjunctions of Parity Equations. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 5:1-5:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{beame_et_al:LIPIcs.SAT.2026.5,
author = {Beame, Paul and Sun, Glenn},
title = {{Extending CDCL to Disjunctions of Parity Equations}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {5:1--5:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.5},
URN = {urn:nbn:de:0030-drops-263112},
doi = {10.4230/LIPIcs.SAT.2026.5},
annote = {Keywords: SAT, CDCL, Proof Complexity, Parity Reasoning}
}
Document
Proof Systems Based on Structured Circuits
Abstract
Since their introduction by Atserias, Kolaitis, and Vardi in 2004, proof systems where each line is represented by an ordered binary decision diagram (OBDD) have been intensively studied as they allow to compactly represent Boolean functions. We extend this line of work by considering representation formats that can be even more succinct than OBDDs and have gained a lot of attention in the area of knowledge compilation: sentential decision diagrams (SDDs) and deterministic structured DNNF circuits (d-SDNNFs). We show that both variants can provide strictly smaller refutations of unsatisfiable CNFs than their OBDD counterparts. Furthermore, we investigate the relative strength of these systems depending on which of the three fundamental derivation rules join, reordering, and weakening are allowed. Here we obtain several separations and identify interesting open problems. To streamline our proofs we establish a sat-to-unsat lifting theorem that might be of independent interest: it turns satisfiable CNFs that are hard to represent by SDDs and d-SDNNFs into unsatisfiable CNFs that are hard to refute in the corresponding proof system.
Cite as
Christoph Berkholz and Matthäus Micun. Proof Systems Based on Structured Circuits. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 6:1-6:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{berkholz_et_al:LIPIcs.SAT.2026.6,
author = {Berkholz, Christoph and Micun, Matth\"{a}us},
title = {{Proof Systems Based on Structured Circuits}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {6:1--6:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.6},
URN = {urn:nbn:de:0030-drops-263123},
doi = {10.4230/LIPIcs.SAT.2026.6},
annote = {Keywords: Proof Complexity, Sentential Decision Diagram, DNNF, OBDD}
}
Document
Towards Understanding the Complexity of CAQE: A Proof-Theoretic Analysis of Its Core Procedure
Abstract
CAQE (Clausal Abstraction for Quantifier Elimination) is currently the most successful algorithmic paradigm for solving Quantified Boolean Formulas (QBF) practice-wise, clearly dominating recent QBF competitions. While apparently being a very strong solver, not much is known about CAQE theory-wise. We propose a framework for formalising runs in the basic CAQE algorithm (where failed assumptions are not considered) as proofs in a proof system CAQE^CORE, which we use to analyse the algorithm proof-theoretically and provide methods for future work to separate it from optimized versions of CAQE that are used in practice.
We show that one can perform strategy extraction on the CAQE^CORE proof system in such a way that strategy size serves as a lower bound for basic CAQE runs. Furthermore, we introduce a measure, which we call CAQE width, which not only acts as a lower bound on CAQE^CORE proofs, but - with the quantifier depth as exponent - as an upper bound as well. Using this analysis, we prove that on QBFs of bounded quantifier complexity, both QCDCL (Quantified Conflict Driven Clause Learning, formalised as a proof system) and Q-resolution p-simulate CAQE^CORE and are indeed strictly stronger.
Cite as
Benjamin Böhm and Olaf Beyersdorff. Towards Understanding the Complexity of CAQE: A Proof-Theoretic Analysis of Its Core Procedure. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 7:1-7:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{bohm_et_al:LIPIcs.SAT.2026.7,
author = {B\"{o}hm, Benjamin and Beyersdorff, Olaf},
title = {{Towards Understanding the Complexity of CAQE: A Proof-Theoretic Analysis of Its Core Procedure}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {7:1--7:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.7},
URN = {urn:nbn:de:0030-drops-263138},
doi = {10.4230/LIPIcs.SAT.2026.7},
annote = {Keywords: QBF, CAQE, CDCL, resolution, proof complexity, simulations, lower bounds}
}
Document
Conditional Autarkies: Hard Formulas Made Easy
Abstract
State-of-the-art SAT solvers increasingly use techniques beyond resolution. For instance, adding redundant clauses allows the solver to reduce the solution space, e.g., to break symmetries. We investigate the strength of relatively weak redundancy reasoning: conditional autarkies and set-blocked clauses, with no new variables and no deletions.
We show 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. In particular, we give efficient proofs of the perfect matching on a grid, the mutilated chessboard, the counting principle modulo 3, and the relativized pigeonhole principle.
Cite as
Ilario Bonacina, Maria Luisa Bonet, Antonina Kolokolova, and Massimo Lauria. Conditional Autarkies: Hard Formulas Made Easy. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{bonacina_et_al:LIPIcs.SAT.2026.8,
author = {Bonacina, Ilario and Bonet, Maria Luisa and Kolokolova, Antonina and Lauria, Massimo},
title = {{Conditional Autarkies: Hard Formulas Made Easy}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {8:1--8:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.8},
URN = {urn:nbn:de:0030-drops-263145},
doi = {10.4230/LIPIcs.SAT.2026.8},
annote = {Keywords: conditional autarkies, perfect matching principle, pigeonhole principle, redundancy rules, proof complexity}
}
Document
Beyond Core-Guided MaxSAT
Abstract
Several proof systems for MaxSAT have been proposed in the literature, including MaxSAT resolution and, more recently, systems based on polynomial calculus and tableaux. Although these systems are sound and complete and have varying strengths, they fail to capture the specific inferential strategies used by practical MaxSAT solvers, particularly those used in core-guided approaches. As a result, a formula that is hard to prove in these proof systems may not be hard for a solver, and vice versa.
In this paper, we describe a new proof system for MaxSAT, the Comparator Calculus (CC), which models the inferential strategies used in core-guided MaxSAT solvers. Inspired by this formalism, we introduce two new MaxSAT algorithms: a core-guided one (CSimple) and one non-core-guided (CSat), which uses heuristics to construct new soft formulas and calls a SAT solver on a single soft formula. We also define a hybrid mechanism (core-guided CSat) that uses cores to guide the heuristics.
We evaluate and compare our solvers with OLL on instances from the MaxSAT evaluation 2024, random 2-CNFs, and PHP formulas. Experimental results suggest that, in general, the performance of the different MaxSAT solvers depends on the structure of the instances. On the set of industrial instances of the MaxSAT Evaluation 2024, CSimple performs better than the others (including OLL).
Cite as
Ilario Bonacina, Jordi Levy, and Ion Mikel Liberal. Beyond Core-Guided MaxSAT. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{bonacina_et_al:LIPIcs.SAT.2026.9,
author = {Bonacina, Ilario and Levy, Jordi and Liberal, Ion Mikel},
title = {{Beyond Core-Guided MaxSAT}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {9:1--9:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.9},
URN = {urn:nbn:de:0030-drops-263154},
doi = {10.4230/LIPIcs.SAT.2026.9},
annote = {Keywords: MaxSAT, Proof Systems, Solvers, Optimization}
}
Document
A Canonical Generalization of OBDD
Abstract
We introduce Tree Decision Diagrams (TDD) as a model for Boolean functions that generalizes OBDD. They can be seen as a restriction of structured d-DNNF; that is, d-DNNF that respect a vtree T. We show that TDDs enjoy the same tractability properties as OBDD, such as model counting, enumeration, conditioning, and apply, and are more succinct. In particular, we show that CNF formulas of treewidth k can be represented by TDDs of FPT size, which is known to be impossible for OBDD. We study the complexity of compiling CNF formulas into deterministic TDDs via bottom-up compilation and relate the complexity of this approach with the notion of factor width introduced by Bova and Szeider.
Cite as
Florent Capelli, YooJung Choi, Stefan Mengel, Martín Muñoz, and Guy Van den Broeck. A Canonical Generalization of OBDD. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 10:1-10:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{capelli_et_al:LIPIcs.SAT.2026.10,
author = {Capelli, Florent and Choi, YooJung and Mengel, Stefan and Mu\~{n}oz, Mart{\'\i}n and Van den Broeck, Guy},
title = {{A Canonical Generalization of OBDD}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {10:1--10:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.10},
URN = {urn:nbn:de:0030-drops-263167},
doi = {10.4230/LIPIcs.SAT.2026.10},
annote = {Keywords: Boolean functions, Model counting, Knowledge Compilation}
}
Document
Strong (D)QBF Dependency Schemes via Pure Paths with Applications to Proof Checking
Abstract
Certification for Quantified Boolean Formulas (QBF) and Dependency Quantified Boolean Formulas (DQBF) is an ongoing challenge. Recent proof complexity work has shown that the majority of QBF and DQBF techniques can be p-simulated by using the independent extension rule.
In propositional logic, extension rules are supported by proof checkers using a more general RAT (Resolution Asymmetric Tautology) rule. The next step in (D)QBF certification would be to update these modern RAT formats to match the strength of this independent extension rule.
In this paper we first introduce a new dependency scheme called 𝒟^{∀pure}. This rule is the missing ingredient that when added to Blinkhorn’s proof system DQRAT allows it to be provably p-equivalent to the Independent Extended QU-Res, the most powerful of the known QBF and DQBF proof systems. Up until now, DQRAT has only existed in theory, so we implement a prototype checker DQRAT-check which includes our extra rule.
In addition to its inclusion in our proof checker we show 𝒟^{∀pure} has other properties that have been found for previous dependency schemes, and each of these observations has potential in solving/checking including the sound integration into the dependency learning solver Qute.
Cite as
Leroy Chew and Tomáš Peitl. Strong (D)QBF Dependency Schemes via Pure Paths with Applications to Proof Checking. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 11:1-11:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{chew_et_al:LIPIcs.SAT.2026.11,
author = {Chew, Leroy and Peitl, Tom\'{a}\v{s}},
title = {{Strong (D)QBF Dependency Schemes via Pure Paths with Applications to Proof Checking}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {11:1--11:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.11},
URN = {urn:nbn:de:0030-drops-263171},
doi = {10.4230/LIPIcs.SAT.2026.11},
annote = {Keywords: DQBF, QBF, Qute, Proof Systems, Dependency Schemes, Dependency Learning, Skolem functions}
}
Document
Long-Distance Q(D^std)-Consensus Is Sound
Abstract
We describe a procedure that extracts existential strategies from verification proofs in the Long-Distance Consensus (i.e., Term Resolution) proof system when augmented with dependency schemes. We prove that when the standard dependency scheme 𝙳^std is used, the extracted strategies are winning strategies, thus establishing soundness of the proof system LDQ(D^std)-Consensus. We show through a counterexample that this approach fails to show soundness for LDQ(D^rrs)-Consensus.
Cite as
Abhimanyu Choudhury, Meena Mahajan, and Friedrich Slivovsky. Long-Distance Q(D^std)-Consensus Is Sound. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 12:1-12:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{choudhury_et_al:LIPIcs.SAT.2026.12,
author = {Choudhury, Abhimanyu and Mahajan, Meena and Slivovsky, Friedrich},
title = {{Long-Distance Q(D^std)-Consensus Is Sound}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {12:1--12:12},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.12},
URN = {urn:nbn:de:0030-drops-263181},
doi = {10.4230/LIPIcs.SAT.2026.12},
annote = {Keywords: Quantified Boolean Formulas, Proof systems, Long-Distance Term Resolution / Consensus, Dependency Schemes}
}
Document
The Compilability Thresholds of 2-CNF to OBDD
Abstract
We prove the existence of two thresholds regarding the compilability of random 2-CNF formulas to OBDDs. The formulas are drawn from F₂(n,δn), the uniform distribution over all 2-CNFs with δ n clauses and n variables, with δ ≥ 0 a constant. We show that, with high probability, the random 2-CNF admits OBDDs of size polynomial in n if 0 ≤ δ < 1/2 or if δ > 1. On the other hand, for 1/2 < δ < 1, with high probability, the random 2-CNF admits only OBDDs of size exponential in n. It is no coincidence that the two "compilability thresholds" are δ = 1/2 and δ = 1. Both are known thresholds for other CNF properties, namely, δ = 1 is the satisfiability threshold for 2-CNF while δ = 1/2 is the treewidth threshold, i.e., the point where the treewidth of the primal graph jumps from constant to linear in n with high probability.
Cite as
Alexis de Colnet, Alfons Laarman, and Joon Hyung Lee. The Compilability Thresholds of 2-CNF to OBDD. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 13:1-13:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{decolnet_et_al:LIPIcs.SAT.2026.13,
author = {de Colnet, Alexis and Laarman, Alfons and Lee, Joon Hyung},
title = {{The Compilability Thresholds of 2-CNF to OBDD}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {13:1--13:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.13},
URN = {urn:nbn:de:0030-drops-263190},
doi = {10.4230/LIPIcs.SAT.2026.13},
annote = {Keywords: Knowledge Compilation, OBDD, Random CNF, Phase Transition}
}
Document
Generalizing CDCL with Graph Backtracking
Abstract
We present graph backtracking, a novel, fine-grained backtracking scheme for CDCL-based SAT solving, parametrized by a user-defined weight function. For conflict repair, we challenge the decision level abstraction and use the implication graph as a precise guiding structure to minimize the weight of literals that are unassigned. Graph backtracking is sound, complete, and terminating. We show that it is a generalization of chronological and non-chronological backtracking by simulating them with specific weight functions. Our approach is implemented in the experimental solver NapSAT. Empirical results show that graph backtracking requires fewer literal propagations than standard approaches, leading to improved solver runtime.
Cite as
Robin Coutelier, Thomas Hader, and Laura Kovács. Generalizing CDCL with Graph Backtracking. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{coutelier_et_al:LIPIcs.SAT.2026.14,
author = {Coutelier, Robin and Hader, Thomas and Kov\'{a}cs, Laura},
title = {{Generalizing CDCL with Graph Backtracking}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {14:1--14:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.14},
URN = {urn:nbn:de:0030-drops-263203},
doi = {10.4230/LIPIcs.SAT.2026.14},
annote = {Keywords: SAT Solving, Backtracking, Conflict Analysis, CDCL}
}
Document
SAT Modulo Well-Founded Semantics
Abstract
The well-founded semantics (WFS) for logic programs yields a unique three-valued model that serves as an efficient core for skeptical reasoning, but lacks built-in mechanisms for choice and case-based reasoning, limiting its expressiveness for problems such as decision making and planning. Propositional SAT solvers excel at combinatorial problems like the latter but, unlike WFS, do not naturally support reasoning under incomplete information or encoding transitive closure properties. We present an integration of a choice operator into WFS that preserves the suitability of the semantics for scalable, partial-information reasoning. From a propositional perspective, our semantics gracefully captures semantically unassigned atoms and constraints; we illustrate this approach in a setting for reasoning about actions under uncertainty. Furthermore, classical propositional satisfiability can not only be embedded into our framework, but now also be extended with reasoning over transitive closures. In terms of program evaluation, we show that the choice operator can be materialized by a SAT solver while propagating the consequences of choices through an extension of the alternating fixpoint algorithm for WFS with conflicts that are propagated back to the SAT solver. To further increase computational performance, we develop clause learning and syntactic decomposition techniques for logic programs with choices.
Cite as
Thomas Eiter, Tobias Nießen, and Davide Soldà. SAT Modulo Well-Founded Semantics. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 15:1-15:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{eiter_et_al:LIPIcs.SAT.2026.15,
author = {Eiter, Thomas and Nie{\ss}en, Tobias and Sold\`{a}, Davide},
title = {{SAT Modulo Well-Founded Semantics}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {15:1--15:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.15},
URN = {urn:nbn:de:0030-drops-263214},
doi = {10.4230/LIPIcs.SAT.2026.15},
annote = {Keywords: Well-Founded Semantics, SAT, Satisfiability, Logic Programming, Least Fixpoint Computation}
}
Document
Bilateral Treewidth for QBF: Where Strategies and Resolution Meet
Abstract
Treewidth is a well-studied decompositional parameter to measure the tree-likeness of a graph. While the propositional satisfiability problem (Sat) is known to be tractable when parameterized by the treewidth of the underlying primal graph, the evaluation of quantified Boolean formulas (QBFs) remains PSPACE-complete even on formulas of constant treewidth. Intuitively, this is because ordinary treewidth does not take into account the prefix of the QBF: it neither distinguishes between existential and universal variables, nor accounts for the order in which they are quantified. In the past, several weaker variants of treewidth have been devised to incorporate prefix-sensitive information. To establish tractability for QBFs under these notions, prior work has employed either strategy- or resolution-based techniques, thereby dividing the parameterized complexity landscape of QBF into two regimes that are incomparable in strength. We establish fixed-parameter tractability with respect to bilateral treewidth, a novel and strictly more powerful decompositional parameter that combines these rivaling approaches by simultaneously allowing for branching on strategies and performing Q-resolution. As in previous works in this direction, our algorithm assumes that a suitable tree decomposition is provided on the input.
Cite as
Robert Ganian and Marlene Gründel. Bilateral Treewidth for QBF: Where Strategies and Resolution Meet. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 16:1-16:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{ganian_et_al:LIPIcs.SAT.2026.16,
author = {Ganian, Robert and Gr\"{u}ndel, Marlene},
title = {{Bilateral Treewidth for QBF: Where Strategies and Resolution Meet}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {16:1--16:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.16},
URN = {urn:nbn:de:0030-drops-263227},
doi = {10.4230/LIPIcs.SAT.2026.16},
annote = {Keywords: QBF, Treewidth, Fixed Parameter Tractability, Dependency Schemes}
}
Document
A Natively Parallel Proof Framework for Clause-Sharing SAT Solving
Abstract
Unsatisfiability proofs are valuable artifacts in propositional satisfiability (SAT) since they can provide correctness guarantees and thus complete trust in reported results. In powerful parallel and distributed clause-sharing SAT solvers, existing proof technology either funnels all solver threads' relevant reasoning steps into a single proof file, which leads to scalability problems for large setups and long running times, or checks proof information in parallel in real-time, which is fully scalable but leaves no persistent artifact. We suggest an alternative approach to achieve the best of both worlds. Specifically, we consider parallel proof files that are logged and also checked in parallel. To this end, we introduce PalRUP - an LRUP-based proof format and a bottleneck-free, decentralized parallel checking procedure that only uses the (parallel) file system and is composed of a set of small, sequential trusted components. In evaluations on up to 3072 cores, we observe that our approach allows for low-overhead proof logging during solving and substantially outscales prior proof producing approaches in terms of checking performance.
Cite as
Ruben Götz, Michael Dörr, and Dominik Schreiber. A Natively Parallel Proof Framework for Clause-Sharing SAT Solving. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 17:1-17:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{gotz_et_al:LIPIcs.SAT.2026.17,
author = {G\"{o}tz, Ruben and D\"{o}rr, Michael and Schreiber, Dominik},
title = {{A Natively Parallel Proof Framework for Clause-Sharing SAT Solving}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {17:1--17:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.17},
URN = {urn:nbn:de:0030-drops-263239},
doi = {10.4230/LIPIcs.SAT.2026.17},
annote = {Keywords: Satisfiability, Proofs, Distributed computing}
}
Document
D-QBF with Few Existential Variables Revisited
Abstract
Quantified Boolean Formula (QBF) is a notoriously hard generalization of SAT, especially from the point of view of parameterized complexity, where the problem remains intractable for most standard parameters. A recent work by Eriksson et al. [IJCAI 24] addressed this by considering the case where the propositional part of the formula is in CNF and we parameterize by the number k of existentially quantified variables. One of their main results was that this natural (but so far overlooked) parameter does lead to fixed-parameter tractability, if we also bound the maximum arity d of the clauses of the given CNF. Unfortunately, their algorithm has a double-exponential dependence on k (2^{2^k}), even when d is an absolute constant. Since the work of Eriksson et al. only complemented this with a SETH-based lower bound implying that a 2^{O(k)} dependence is impossible, this left a large gap as an open question.
Our main result in this paper is to close this gap by showing that the double-exponential dependence is optimal, assuming the ETH: even for CNFs of arity 4, QBF with k existential variables cannot be solved in time 2^{2^o(k)} |φ|^O(1). Complementing this, we also consider the further restricted case of QBF with only two quantifier blocks (∀∃-QBF). We show that in this case the situation improves dramatically: for each d ≥ 3 we show an algorithm with running time k^O_d(k^{d-1}) |φ|^O(1) (where the notation O_d hides factors depending on d) and a lower bound under the ETH showing our algorithm is almost optimal.
Cite as
Andreas Grigorjew and Michael Lampis. D-QBF with Few Existential Variables Revisited. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 18:1-18:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{grigorjew_et_al:LIPIcs.SAT.2026.18,
author = {Grigorjew, Andreas and Lampis, Michael},
title = {{D-QBF with Few Existential Variables Revisited}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {18:1--18:13},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.18},
URN = {urn:nbn:de:0030-drops-263244},
doi = {10.4230/LIPIcs.SAT.2026.18},
annote = {Keywords: QBF, FPT algorithms, ETH}
}
Document
SMT with Uninterpreted Functions and Monotonicity Constraints in Systems Biology
Abstract
Uninterpreted functions are a key modeling tool for systems with unknown or abstracted components. Certain domains, such as systems biology, additionally impose monotonicity constraints on these components, requiring specific inputs to have a consistently positive or negative effect on the output. In this paper, we tackle the model inference problem for biological systems by applying the theory of uninterpreted functions with monotonicity constraints. We compare the performance of naive quantified encodings of the problem and the performance of the existing approach based on eager quantifier instantiation, which is based on the fact that a finite set of quantifier-free monotonicity lemmas is sufficient to encode the monotonicity of uninterpreted functions. Additionally, we consider a lazy variant of the approach that introduces the monotonicity lemmas on demand.
We evaluate the SMT-based approach to model inference using a large collection of systems biology benchmarks. The results demonstrate that the instantiation-based encodings significantly outperform quantified encodings, which typically struggle with large function arities and complex instances. As the key result, we show that our approach based on SMT with uninterpreted functions and monotonicity constraints significantly outperforms state-of-the-art domain-specific tools used in systems biology, such as the ASP-based Bonesis and the BDD-based AEON.
Cite as
Ondřej Huvar, Martin Jonáš, and Samuel Pastva. SMT with Uninterpreted Functions and Monotonicity Constraints in Systems Biology. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 19:1-19:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{huvar_et_al:LIPIcs.SAT.2026.19,
author = {Huvar, Ond\v{r}ej and Jon\'{a}\v{s}, Martin and Pastva, Samuel},
title = {{SMT with Uninterpreted Functions and Monotonicity Constraints in Systems Biology}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {19:1--19:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.19},
URN = {urn:nbn:de:0030-drops-263251},
doi = {10.4230/LIPIcs.SAT.2026.19},
annote = {Keywords: satisfiability modulo theories, uninterpreted function, monotonicity, boolean network, logic-based modeling}
}
Document
New Algorithms for Parity-SAT and Its Bounded-Occurrence Versions
Abstract
Parity-SAT is the problem of determining whether a given CNF formula has an odd number of satisfying assignments. As a canonical ⊕P-complete problem, it represents a fundamental variant of the exact model counting problem (#SAT). Under the Strong Exponential Time Hypothesis (SETH), Parity-SAT admits no O^*((2-ε)ⁿ)-time or O^*((2-ε)^m)-time algorithm for any constant ε > 0, where n and m denote the numbers of variables and clauses, respectively. Thus, breaking the 2ⁿ or 2^m barrier appears impossible in full generality.
In this work, we revisit this barrier through structural restrictions and a refined exploitation of parity. We study Parity-d-occ-SAT, where each variable appears in at most d clauses, and obtain three main results. First, we design {a randomized} O^*(2^{m(1-1/O(d))})-time algorithm, thereby breaking the 2^m barrier for every fixed d. Second, for the special case d = 2, we develop a significantly sharper branching algorithm running in O^*(1.1193ⁿ) time or O^*(1.3248^m) time. Third, leveraging the structural insights underlying the d = 2 case, we obtain an O^*(1.1052^L)-time algorithm for general Parity-SAT, where L denotes the formula length. All algorithms use only polynomial space. Notably, our running-time bounds are better than the best known bounds for the corresponding exact counting counterparts, highlighting a genuine algorithmic advantage of parity over counting. Conceptually, our results demonstrate that parity admits finer structural reductions and more efficient branching than exact model counting, and that bounded occurrence can be systematically leveraged to circumvent classical exponential barriers.
Cite as
Sanjay Jain, Junqiang Peng, Frank Stephan, Haoyun Tang, and Mingyu Xiao. New Algorithms for Parity-SAT and Its Bounded-Occurrence Versions. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 20:1-20:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{jain_et_al:LIPIcs.SAT.2026.20,
author = {Jain, Sanjay and Peng, Junqiang and Stephan, Frank and Tang, Haoyun and Xiao, Mingyu},
title = {{New Algorithms for Parity-SAT and Its Bounded-Occurrence Versions}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {20:1--20:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.20},
URN = {urn:nbn:de:0030-drops-263263},
doi = {10.4230/LIPIcs.SAT.2026.20},
annote = {Keywords: Parity-SAT, Exact Exponential Algorithms}
}
Document
PALSAT: Deep Cooperation of Unit Propagation and Local Search in Incomplete SAT Solving
Abstract
The Boolean Satisfiability (SAT) problem is a fundamental NP-complete problem. Algorithms for SAT include complete ones, typically based on Conflict-Driven Clause Learning (CDCL) methods, and incomplete ones, mostly following local search frameworks. CDCL solvers perform very well on complex structured instances. Local search (LS) algorithms cannot compete with CDCL solvers on structured instances, but show good performance on random and crafted instances, and also serve as an important component in top CDCL solvers. This raises a natural question: can techniques from complete SAT solving be used to improve incomplete solvers? This paper proposes the PALSAT (Progressive Activation Local Search for SAT) incomplete solver to answer it, which integrates the core techniques from both sides, Unit Propagation (UP) and LS. PALSAT starts from a subproblem, which relaxes many variables, and uses UP to progressively activate the search space (i.e., expand the subproblem). When a conflict is encountered, LS is invoked to repair it by searching all variables induced in the subproblem and the conflict. PALSAT ensures that the subproblem size increases monotonically and that the search process gradually approaches the full formula. In PALSAT, UP can guide growth direction based on the structure, and LS can efficiently repair conflicts. Their cooperation leads to some promising results. After a decade of evolution in CCAnr and probSAT variants, PALSAT represents a new incomplete algorithm framework with significantly better performance across various benchmarks.
Cite as
Mingming Jin, Zhijie Kuang, Jiongzhi Zheng, Kun Mao, and Kun He. PALSAT: Deep Cooperation of Unit Propagation and Local Search in Incomplete SAT Solving. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 21:1-21:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{jin_et_al:LIPIcs.SAT.2026.21,
author = {Jin, Mingming and Kuang, Zhijie and Zheng, Jiongzhi and Mao, Kun and He, Kun},
title = {{PALSAT: Deep Cooperation of Unit Propagation and Local Search in Incomplete SAT Solving}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {21:1--21:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.21},
URN = {urn:nbn:de:0030-drops-263277},
doi = {10.4230/LIPIcs.SAT.2026.21},
annote = {Keywords: Satisfiability Problem, Local Search Algorithm, Unit Propagation, Subproblem Expansion}
}
Document
Definition-Based Dependency Schemes
Abstract
A variable in a quantified Boolean formula (QBFs) is defined, if its value is uniquely determined by some other variables. Such definitions are widely exploited in various techniques for QBF solving. In this work, we formalize the concept of using definitions for reducing variable dependencies by introducing a novel dependency scheme and investigate its proof-theoretic impact.
Our analysis shows that a definition-based dependency scheme is able to detect independencies other established dependency schemes cannot and that this can lead to exponentially shorter refutations. We further demonstrate that our scheme can be combined with any other scheme and that such a combined use can exponentially outperform using either scheme alone. Moreover, we study the dynamic application of our definition-based dependency scheme, which leads to another exponential speedup compared to the static application. Finally, we analyze the computational complexity of our dependency scheme and introduce a family of tractable variants.
Cite as
David Kattermann, Clemens Hofstadler, and Martina Seidl. Definition-Based Dependency Schemes. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{kattermann_et_al:LIPIcs.SAT.2026.22,
author = {Kattermann, David and Hofstadler, Clemens and Seidl, Martina},
title = {{Definition-Based Dependency Schemes}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {22:1--22:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.22},
URN = {urn:nbn:de:0030-drops-263285},
doi = {10.4230/LIPIcs.SAT.2026.22},
annote = {Keywords: Quantified Boolean formulas, Dependency schemes, Proof calculi}
}
Document
Near-Optimal Encodings of Cardinality Constraints
Abstract
We present several novel encodings for cardinality constraints, which use fewer clauses than previous encodings and, more importantly, introduce new generally applicable techniques for constructing compact encodings. First, we present a CNF encoding for the AtMostOne(x_1,…,x_n) constraint using 2n + 2 √{2n} + O(∛n) clauses, thus refuting the conjectured optimality of Chen’s product encoding. Our construction also yields a smaller monotone circuit for the threshold-2 function, improving on a 50-year-old construction of Adleman and incidentally solving a long-standing open problem in circuit complexity. On the other hand, we show that any encoding for this constraint requires at least 2n + √{n+1} - 2 clauses, which is the first nontrivial unconditional lower bound for this constraint and answers a question of Kučera, Savický, and Vorel. We then turn our attention to encodings of AtMost_k(x_1,…,x_n), where we introduce grid compression, a technique inspired by hash tables, to give encodings using 2n + o(n) clauses as long as k = o(∛{n}) and 4n + o(n) clauses as long as k = o(n). Previously, the smallest known encodings were of size (k+1)n + o(n) for k ≤ 5 and 7n - o(n) for k ≥ 6.
Cite as
Andrew Krapivin, Benjamin Przybocki, and Bernardo Subercaseaux. Near-Optimal Encodings of Cardinality Constraints. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 23:1-23:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{krapivin_et_al:LIPIcs.SAT.2026.23,
author = {Krapivin, Andrew and Przybocki, Benjamin and Subercaseaux, Bernardo},
title = {{Near-Optimal Encodings of Cardinality Constraints}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {23:1--23:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.23},
URN = {urn:nbn:de:0030-drops-263294},
doi = {10.4230/LIPIcs.SAT.2026.23},
annote = {Keywords: CNF encodings, cardinality constraints, circuit complexity}
}
Document
Exact Symbolic Reasoning for Nonlinear Stochastic SMT via Cylindrical Algebraic Decomposition
Abstract
Stochastic Satisfiability Modulo Theories (SSMT) has traditionally focused on the interplay between existential and randomized quantifiers, typically relying on numerical sampling or approximations. We present a generalized SSMT framework that integrates universal quantification, lifting the formalism to a robust stochastic game-theoretic setting. By treating universal quantifiers as the adversarial infimum of satisfaction probabilities, our framework enables the exact modeling of competitive interactions under uncertainty.
Our approach leverages Cylindrical Algebraic Decomposition (CAD) to derive exact symbolic probability expressions for Nonlinear Real Arithmetic (NRA) formulas, moving beyond the limitations of linear constraints and point-value estimations. Central to our contribution is a recursive quantifier elimination algorithm designed to handle variable-dependent domains and non-algebraic expressions through a variable reparameterization technique.
Experimental evaluation across baseline synthetic formulas, strategic economic models, and probabilistic program verification benchmarks demonstrates that our framework consistently computes exact symbolic solutions. By achieving a degree of symbolic precision and expressiveness unattainable by traditional numerical solvers, this work establishes a new baseline for exact reasoning in stochastic adversarial environments.
Cite as
Jung-Cheng Lin, Chia-Hsuan Su, Jie-Hong R. Jiang, and Hiroshi Unno. Exact Symbolic Reasoning for Nonlinear Stochastic SMT via Cylindrical Algebraic Decomposition. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{lin_et_al:LIPIcs.SAT.2026.24,
author = {Lin, Jung-Cheng and Su, Chia-Hsuan and Jiang, Jie-Hong R. and Unno, Hiroshi},
title = {{Exact Symbolic Reasoning for Nonlinear Stochastic SMT via Cylindrical Algebraic Decomposition}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {24:1--24:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.24},
URN = {urn:nbn:de:0030-drops-263307},
doi = {10.4230/LIPIcs.SAT.2026.24},
annote = {Keywords: Stochastic Satisfiability Modulo Theories (SSMT), Cylindrical Algebraic Decomposition (CAD), Quantifier Elimination}
}
Document
d-DNNF Modulo Theories: A General Framework for Polytime SMT Queries
Abstract
In Knowledge Compilation (KC) a propositional knowledge base is compiled off-line into some target form, typically into deterministic decomposable negation normal form (d-DNNF) or one of its subcases, which is then used on-line to answer a large number of queries in polytime, such as clausal entailment, model counting, and others. The general idea is to push as much of the computational effort into the off-line compilation phase, which is amortized over all on-line polytime queries.
In this paper, we present for the first time a novel and general technique to leverage d-DNNF compilation and querying to SMT level. Intuitively, before d-DNNF compilation, the input SMT formula is combined with a list of pre-computed ad-hoc theory lemmas, so that the queries at SMT level reduce to those at propositional level. This approach has several features: (i) it works for every theory, or theory combination thereof; (ii) it works for all forms of d-DNNF; (iii) it is easy to implement on top of any d-DNNF compiler and any theory-lemma enumerator, which are used as black boxes; (iv) most importantly, these compiled SMT d-DNNFs can be queried in polytime by means of a standard propositional d-DNNF reasoner. As proof of concept, we have implemented a tool on top of state-of-the-art d-DNNF packages and of the MathSAT SMT solver. Some preliminary empirical evaluation supports the feasibility and effectiveness of the approach.
Cite as
Gabriele Masina, Emanuele Civini, Massimo Michelutti, Giuseppe Spallitta, and Roberto Sebastiani. d-DNNF Modulo Theories: A General Framework for Polytime SMT Queries. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 25:1-25:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{masina_et_al:LIPIcs.SAT.2026.25,
author = {Masina, Gabriele and Civini, Emanuele and Michelutti, Massimo and Spallitta, Giuseppe and Sebastiani, Roberto},
title = {{d-DNNF Modulo Theories: A General Framework for Polytime SMT Queries}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {25:1--25:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.25},
URN = {urn:nbn:de:0030-drops-263316},
doi = {10.4230/LIPIcs.SAT.2026.25},
annote = {Keywords: SMT, Knowledge Compilation, d-DNNF}
}
Document
On Knowledge Compilation for Two-Variable First-Order Logic
Abstract
Knowledge compilation transforms logical theories into circuit representations that support efficient reasoning. We study this problem for propositional groundings of FO², the two-variable fragment of first-order logic over finite domains. Given an FO² sentence and a domain of size n, its grounding yields a propositional theory over ground atoms. We ask whether such theories admit compact representations in DNNF-based and related knowledge compilation languages, and whether these can be constructed efficiently, both with respect to the domain size n for a fixed sentence. We show first that compact compilation is impossible in general: there exists an FO² sentence whose grounding over a domain of size n requires DNNF size 2^Ω(n). On the positive side, we develop a two-stage compiler that exploits the symmetries inherent in the propositional groundings of FO² sentences. It branches on unary and binary types rather than individual ground atoms, in a similar spirit to lifted inferences for probabilistic relational models. Moreover, it optimizes the compilation process by efficiently identifying and caching residual subproblems that are equivalent with respect to future extensions. Experiments show the practical efficiency of our approach, which often produces smaller circuits and compiles faster than straightforward grounding-based baselines.
Cite as
Qiaolan Meng, Juhua Pu, Hongting Niu, Yuyi Wang, Yuanhong Wang, and Ondřej Kuželka. On Knowledge Compilation for Two-Variable First-Order Logic. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 26:1-26:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{meng_et_al:LIPIcs.SAT.2026.26,
author = {Meng, Qiaolan and Pu, Juhua and Niu, Hongting and Wang, Yuyi and Wang, Yuanhong and Ku\v{z}elka, Ond\v{r}ej},
title = {{On Knowledge Compilation for Two-Variable First-Order Logic}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {26:1--26:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.26},
URN = {urn:nbn:de:0030-drops-263322},
doi = {10.4230/LIPIcs.SAT.2026.26},
annote = {Keywords: Knowledge Compilation, First-order Logic, SAT}
}
Document
Backtrackable Inprocessing
Abstract
We introduce Backtrackable Inprocessing (BI), a framework that enables applying inprocessing under the current trail at any decision level, at any point during incremental SAT solving. Our approach lifts the long-standing restriction that inprocessing must be performed only at the global decision level, thereby substantially increasing its potential effectiveness. We focus on three highly efficient core techniques: subsumption, self-subsuming resolution, and Bounded Variable Elimination (BVE). We show how to ensure sound backtracking in the presence of inprocessing, and demonstrate that applying BI for incremental preprocessing after propagating assumptions yields significant performance improvements on Bounded Model Checking (BMC) benchmarks from the Hardware Model Checking Competition 2017. Implemented in the Island SAT solver (IntelSAT’s fork), BI enables solving ∼1.5× as many difficult bounds as the baseline global-level incremental preprocessor.
Cite as
Alexander Nadel. Backtrackable Inprocessing. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 27:1-27:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{nadel:LIPIcs.SAT.2026.27,
author = {Nadel, Alexander},
title = {{Backtrackable Inprocessing}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {27:1--27:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.27},
URN = {urn:nbn:de:0030-drops-263330},
doi = {10.4230/LIPIcs.SAT.2026.27},
annote = {Keywords: SAT, Inprocessing, BVE, Bounded Variable Elimination, Subsumption, Incremental SAT}
}
Document
Factoring Learned Clauses
Abstract
Modern SAT solvers are based on the conflict-driven clause learning (CDCL) paradigm, which can be simulated by the resolution proof system. This limits solver effectiveness on instances known to be hard for resolution. Certain approaches, such as parity reasoning, have been shown to be effective in this context, but are hard to integrate with CDCL, in particular, with mainstream proof certificates. The powerful yet simple Extended Resolution (ER) proof system provides an alternative but is not widely used in SAT solving despite having proof certificates for decades and using it effectively remains an open challenge. 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. We further propose a new, less intrusive inprocessing approach based on factoring XOR and ITE gates from learned clauses globally. Previous work on bounded variable addition focused on AND gates and original clauses only. Our experimental evaluation shows substantial improvements on hard combinatorial benchmark families without performance degradation on the SAT Competition.
Cite as
Florian Pollitt, Zachary Battleman, Mathias Fleury, Yakir Vizel, Marijn J. H. Heule, Armin Biere, and Randal E. Bryant. Factoring Learned Clauses. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 28:1-28:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{pollitt_et_al:LIPIcs.SAT.2026.28,
author = {Pollitt, Florian and Battleman, Zachary and Fleury, Mathias and Vizel, Yakir and Heule, Marijn J. H. and Biere, Armin and Bryant, Randal E.},
title = {{Factoring Learned Clauses}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {28:1--28:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.28},
URN = {urn:nbn:de:0030-drops-263343},
doi = {10.4230/LIPIcs.SAT.2026.28},
annote = {Keywords: SAT solving, Extended Resolution, CDCL, Inprocessing}
}
Document
Automated Reencoding Meets Graph Theory
Abstract
Bounded Variable Addition (BVA) is a central preprocessing method in modern state-of-the-art SAT solvers. We provide a graph-theoretic characterization of which 2-CNF encodings can be constructed by an idealized BVA algorithm. Based on this insight, we prove new results about the behavior and limitations of BVA and its interaction with other preprocessing techniques. We show that idealized BVA, plus some minor additional preprocessing (e.g., equivalent literal substitution), can reencode any 2-CNF formula with n variables into an equivalent 2-CNF formula with (lg(3)/4 + o(1)) n²/(lg n) clauses. Furthermore, we show that without the additional preprocessing the constant factor worsens from lg(3)/4 ≈ 0.396 to 1, and that no reencoding method can achieve a constant below 0.25. On the other hand, for the at-most-one constraint on n variables, we prove that idealized BVA cannot reencode this constraint using fewer than 3n-6 clauses, a bound that we prove is achieved by actual implementations. In particular, this shows that the product encoding for at-most-one, which uses 2n+o(n) clauses, cannot be constructed by BVA regardless of the heuristics used. Finally, our graph-theoretic characterization of BVA allows us to leverage recent work in algorithmic graph theory to develop a drastically more efficient implementation of BVA that achieves a comparable clause reduction on random monotone 2-CNF formulas.
Cite as
Benjamin Przybocki, Bernardo Subercaseaux, and Marijn J. H. Heule. Automated Reencoding Meets Graph Theory. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 29:1-29:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{przybocki_et_al:LIPIcs.SAT.2026.29,
author = {Przybocki, Benjamin and Subercaseaux, Bernardo and Heule, Marijn J. H.},
title = {{Automated Reencoding Meets Graph Theory}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {29:1--29:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.29},
URN = {urn:nbn:de:0030-drops-263358},
doi = {10.4230/LIPIcs.SAT.2026.29},
annote = {Keywords: SAT solving, CNF encodings, BVA, Rectifier networks}
}
Document
An Exponential Separation Between Deterministic CDCL and DPLL Solvers
Abstract
We prove that there exists a deterministic configuration of Conflict-Driven Clause Learning (CDCL) SAT solvers using a variant of the VSIDS branching heuristic that solves instances of the Ordering Principle (OP) CNF formulas in time polynomial in n, where n is the number of variables in such formulas. Since tree-like resolution is known to have an exponential lower bound for proof size for OP formulas, it follows that CDCL under this configuration has an exponential separation with any solver that is polynomially equivalent to tree-like resolution and therefore any configuration of DPLL SAT solvers.
Cite as
Sahil Samar, Marc Vinyals, and Vijay Ganesh. An Exponential Separation Between Deterministic CDCL and DPLL Solvers. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 30:1-30:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{samar_et_al:LIPIcs.SAT.2026.30,
author = {Samar, Sahil and Vinyals, Marc and Ganesh, Vijay},
title = {{An Exponential Separation Between Deterministic CDCL and DPLL Solvers}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {30:1--30:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.30},
URN = {urn:nbn:de:0030-drops-263369},
doi = {10.4230/LIPIcs.SAT.2026.30},
annote = {Keywords: SAT solvers, CDCL, Proof Systems, VSIDS}
}
Document
Dsat: A Native SAT Solver for Discrete Logic
Abstract
Discrete variables are common in many applications, such as probabilistic reasoning, planning and explainable AI. When symbolic reasoning techniques are brought in to bear on these applications, a standard technique for handling discrete variables is to binarize them into Boolean variables to allow the use of Boolean computational machinery such as SAT solvers. This technique can face both computational and semantical challenges though. In this work, we develop a native SAT solver for discrete logic, which is a direct extension of Boolean logic in which variables can take arbitrary values. Our proposed solver has a similar design to Boolean SAT solvers, with ingredients such as unit resolution and clause learning but ones that operate natively on discrete variables. We illustrate the merits of the developed SAT solver by comparing it empirically to CSP solvers applied to discrete CNFs, to Boolean SAT solver applied to binarized CNFs, and to some hybrid solvers.
Cite as
Yaofang Zhang, Ken Zhou, and Adnan Darwiche. Dsat: A Native SAT Solver for Discrete Logic. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 31:1-31:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{zhang_et_al:LIPIcs.SAT.2026.31,
author = {Zhang, Yaofang and Zhou, Ken and Darwiche, Adnan},
title = {{Dsat: A Native SAT Solver for Discrete Logic}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {31:1--31:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.31},
URN = {urn:nbn:de:0030-drops-263372},
doi = {10.4230/LIPIcs.SAT.2026.31},
annote = {Keywords: Discrete Variables, CDCL SAT Solvers, Unit Resolution, Clause Learning}
}
Document
Short Paper
On Proof Systems for #QBF (Short Paper)
Abstract
For a quantified Boolean formula (QBF), the problem of computing the number of winning strategies is known as the #QBF problem. This problem is considered harder than the analogous #SAT problem. Recently, important proof systems for QBFs and #SAT have been studied. By extending the ideas from both fields, we show that it is possible to design proof systems for #QBF. Such proof systems are important not only for advancing the theory of #QBF but also for certifying and designing better #QBF solvers, an area that is still in its early stages.
In this paper, we explore #QBF proof systems to count the number of Skolem functions. In addition to a naive system, we study #QBF systems based on the ∀-expansion rule of QBFs. We observe that these systems have inherent structural weaknesses that lead to lower bounds. As an alternative, we propose a #QBF proof system that we call Q-MICE, which consists of sound inference rules for computing and certifying the #QBF solution, similar to the line-based #SAT proof system MICE. To demonstrate the strength of Q-MICE, we present various upper bounds, such as the quantified version of the propositional XOR-PAIRS formula, which are known to be hard for MICE. Consequently, we also separate Q-MICE from ∀-expansion based #QBF proof systems.
Cite as
Sravanthi Chede, Leroy Chew, Vaibhav Krishan, and Anil Shukla. On Proof Systems for #QBF (Short Paper). In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 32:1-32:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{chede_et_al:LIPIcs.SAT.2026.32,
author = {Chede, Sravanthi and Chew, Leroy and Krishan, Vaibhav and Shukla, Anil},
title = {{On Proof Systems for #QBF}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {32:1--32:12},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.32},
URN = {urn:nbn:de:0030-drops-263380},
doi = {10.4230/LIPIcs.SAT.2026.32},
annote = {Keywords: QBF, Model Counting, Proof Systems, #QBF}
}
Document
Short Paper
Shapley-Shubik Attribution from Minimal Subsets (Short Paper)
Abstract
We address the problem of attributing responsibility to individual clauses for the unsatisfiability of a propositional formula. Recent work adopted the Shapley-Shubik power index, proposing a probabilistic approximation algorithm. However, although polynomial, the required number of SAT solver calls becomes impractical when the input formula is not easy to solve. In such cases, it is often possible to enumerate a partial set of minimal unsatisfiable subsets (MUSes) and minimal correction subsets (MCSes). In this paper, we demonstrate that these subsets can be leveraged to efficiently bound and approximate the Shapley-Shubik index. We introduce a framework that exploits the structural information provided by the available sets to derive useful attribution explanations.
Cite as
Pablo Martínez-Naredo, Raúl Mencía, Joao Marques-Silva, and Carlos Mencía. Shapley-Shubik Attribution from Minimal Subsets (Short Paper). In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 33:1-33:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{martineznaredo_et_al:LIPIcs.SAT.2026.33,
author = {Mart{\'\i}nez-Naredo, Pablo and Menc{\'\i}a, Ra\'{u}l and Marques-Silva, Joao and Menc{\'\i}a, Carlos},
title = {{Shapley-Shubik Attribution from Minimal Subsets}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {33:1--33:13},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.33},
URN = {urn:nbn:de:0030-drops-263398},
doi = {10.4230/LIPIcs.SAT.2026.33},
annote = {Keywords: Unsatisfiability, Shapley-Shubik index, MUSes and MCSes}
}
Document
Tool Paper
HitPBO: An Implicit Hitting Set Solver for Pseudo-Boolean Optimization (Tool Paper)
Abstract
We describe HitPBO 1.0, a from-scratch open-source C++ implementation of the implicit hitting set (IHS) approach to pseudo-Boolean optimization. Compared to earlier implementations, HitPBO adds a range of functionalities and search techniques, certificates, and support for various alternative solvers within IHS. We give an overview of the solver’s architecture and its functionalities.
Cite as
Hannes Ihalainen, Dieter Vandesande, André Schidler, Jeremias Berg, and Matti Järvisalo. HitPBO: An Implicit Hitting Set Solver for Pseudo-Boolean Optimization (Tool Paper). In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 34:1-34:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{ihalainen_et_al:LIPIcs.SAT.2026.34,
author = {Ihalainen, Hannes and Vandesande, Dieter and Schidler, Andr\'{e} and Berg, Jeremias and J\"{a}rvisalo, Matti},
title = {{HitPBO: An Implicit Hitting Set Solver for Pseudo-Boolean Optimization}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {34:1--34:13},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.34},
URN = {urn:nbn:de:0030-drops-263401},
doi = {10.4230/LIPIcs.SAT.2026.34},
annote = {Keywords: Pseudo-Boolean optimization, implicit hitting set approach, solvers}
}
Document
Tool Paper
Efficient Identification of Isomorphic SAT Instances (Tool Paper)
Abstract
Many SAT benchmark datasets contain structurally identical instances arising from repeated shuffling, generators producing identical formulas under different seeds, or duplicate encodings from different tools. We present an efficient, open-source, isomorphism-invariant hashing algorithm for SAT instances, based on Weisfeiler-Leman (WL) label refinement. Each instance is represented as a bipartite clause-literal graph, and iterative label refinement computes a canonical signature, with instances having identical signatures treated as isomorphic. When integrated into our benchmark toolset Global Benchmark Database (GBD), the method substantially reduces false positives from naive degree-sequence hashing with minimal overhead.
Cite as
Ashlin Iser and Frederick Gehm. Efficient Identification of Isomorphic SAT Instances (Tool Paper). In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 35:1-35:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{iser_et_al:LIPIcs.SAT.2026.35,
author = {Iser, Ashlin and Gehm, Frederick},
title = {{Efficient Identification of Isomorphic SAT Instances}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {35:1--35:8},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.35},
URN = {urn:nbn:de:0030-drops-263418},
doi = {10.4230/LIPIcs.SAT.2026.35},
annote = {Keywords: Isomorphism, Benchmarking, Boolean Satisfiability}
}
Document
Tool Paper
Sustainable Benchmarking Tool (Tool Paper)
Abstract
Solvers for NP-hard problems from areas such as automated reasoning or optimisation are complex systems in which many different components interact. The performance of these solvers is the result of an intricate interplay between implementation details, algorithmic concepts and heuristics. This, alongside the complexity of the problem instances to be solved, makes it challenging to assess the effect of a single idea on the overall performance of a given solver. It is therefore not only crucial, but also challenging to evaluate the performance impact of new ideas. Existing reliable evaluation methods require large sets of diverse benchmark instances and considerable amounts of computing resources. This makes empirical evaluation a bottleneck for solver development, as it is time-consuming and energy-intensive, often requiring several CPU years of computation to evaluate the impact of a single idea. In recent years, this bottleneck has led to the development of data-driven approaches that can dynamically select a smaller number of instances that provide sufficient statistical evidence to evaluate the relative performance of a given set of solvers. However, these methods are typically not easily accessible. In this work, we present a tool that implements these methods and makes them readily accessible to solver developers, thus enabling them to obtain swifter feedback on their ideas.
Cite as
Ashlin Iser, Marie Anastacio, Théo Matricon, Laurent Simon, and Holger H. Hoos. Sustainable Benchmarking Tool (Tool Paper). In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 36:1-36:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{iser_et_al:LIPIcs.SAT.2026.36,
author = {Iser, Ashlin and Anastacio, Marie and Matricon, Th\'{e}o and Simon, Laurent and Hoos, Holger H.},
title = {{Sustainable Benchmarking Tool}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {36:1--36:12},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.36},
URN = {urn:nbn:de:0030-drops-263427},
doi = {10.4230/LIPIcs.SAT.2026.36},
annote = {Keywords: Sustainability, Empirical performance comparison, Benchmarking, Problem instance selection}
}
Document
Tool Paper
Scuttle: A System for Multi-Objective MaxSAT (Tool Paper)
Abstract
We describe the Scuttle system for multi-objective combinatorial optimization. Scuttle accepts multi-objective instances where the constraints are declared either as propositional clauses or pseudo-Boolean constraints, and implements a range of multi-objective maximum satisfiability algorithms (including ones for enumerating all Pareto-optimal and leximax-optimal solutions). Pseudo-Boolean constraints are translated to clauses, allowing for applying any of the implemented algorithms on both the clausal and the pseudo-Boolean level. Scuttle also includes tightly integrated preprocessing (both core boosting and liftings of SAT preprocessing techniques) for multi-objective instances and can provide proof certificates for selected algorithms.
Cite as
Christoph Jabs, Jeremias Berg, and Matti Järvisalo. Scuttle: A System for Multi-Objective MaxSAT (Tool Paper). In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 37:1-37:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{jabs_et_al:LIPIcs.SAT.2026.37,
author = {Jabs, Christoph and Berg, Jeremias and J\"{a}rvisalo, Matti},
title = {{Scuttle: A System for Multi-Objective MaxSAT}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {37:1--37:13},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.37},
URN = {urn:nbn:de:0030-drops-263431},
doi = {10.4230/LIPIcs.SAT.2026.37},
annote = {Keywords: Multi-objective combinatorial optimization, maximum satisfiability, pseudo-Boolean optimization}
}
Document
Tool Paper
decdnnf_rs: A Framework for Querying d-DNNF (Tool Paper)
Abstract
Industrial automated reasoning demands the rapid, repeated extraction of insights from complex formulas. Knowledge compilation into the Deterministic Decomposable Negation Normal Form (d-DNNF) addresses this by reducing natively intractable tasks to polynomial-time operations. We present decdnnf_rs, a performant framework for executing advanced reasoning queries directly on d-DNNF circuits. The library provides unified support for Satisfiability, Model Counting, Disjoint Model Enumeration, Direct Access, and Uniform Sampling. Crucially, decdnnf_rs handles dynamic contexts through implicit conditioning via weight propagation, avoiding the computational overhead of explicit graph modification. It also incorporates dynamic smoothness tracking to maintain a compact memory footprint. Bridging theoretical advancements with robust software engineering, decdnnf_rs offers an optimized toolset for exact and stochastic reasoning.
Cite as
Jean-Marie Lagniez and Emmanuel Lonca. decdnnf_rs: A Framework for Querying d-DNNF (Tool Paper). In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 38:1-38:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{lagniez_et_al:LIPIcs.SAT.2026.38,
author = {Lagniez, Jean-Marie and Lonca, Emmanuel},
title = {{decdnnf\underliners: A Framework for Querying d-DNNF}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {38:1--38:12},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.38},
URN = {urn:nbn:de:0030-drops-263442},
doi = {10.4230/LIPIcs.SAT.2026.38},
annote = {Keywords: Knowledge compilation, d-DNNF, Model counting, Model enumeration, Uniform sampling}
}
Document
Tool Paper
WhyUnsat: A Practical Explanation Tool (Tool Paper)
Abstract
Hard industrial planning, timetabling or scheduling instances for SAT typically have many high-level constraints, each expressed by a possibly large number of clauses. When a given instance is reported unsatisfiable by the SAT solver, the user normally needs an explanation why: a (hopefully small) subset of the constraints causing it. Our industrial applications require fast explanations, preferably faster than the original SAT run. For this, we leverage the original solver’s work through its unsatisfiability proof.
Here we introduce WhyUnsat, and explain why it is fast and robust. In WhyUnsat one can always plug in the best current SAT solver and proof trimmer, without any modification, by simply indicating the path to their executables. WhyUnsat is also fast because it exploits, via MPI, the -progressively cheaper- shared-memory and distributed computing resources. Another requirement we had is that the tool should be anytime and user-friendly; indeed, it quickly shows a human-readable presentation of (an over-approximation of) the explanation, which is then progressively reduced until minimality (unless interrupted by the user).
Finally, and not less importantly, here we explain how and why the WhyUnsat approach is now also directly applicable, at no implementation cost, to IPASIR-UP-based constraint programming by Lazy Clause Generation (LCG) as well as to SAT Modulo Theories (SMT).
Cite as
Robert Nieuwenhuis, Albert Oliveras, and Enric Rodríguez-Carbonell. WhyUnsat: A Practical Explanation Tool (Tool Paper). In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 39:1-39:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{nieuwenhuis_et_al:LIPIcs.SAT.2026.39,
author = {Nieuwenhuis, Robert and Oliveras, Albert and Rodr{\'\i}guez-Carbonell, Enric},
title = {{WhyUnsat: A Practical Explanation Tool}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {39:1--39:10},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.39},
URN = {urn:nbn:de:0030-drops-263456},
doi = {10.4230/LIPIcs.SAT.2026.39},
annote = {Keywords: SAT, SMT, Constraint Programming, Lazy Clause Generation}
}
Document
Tool Paper
CaDiCaL 3.0 (Tool Paper)
Abstract
The propositional satisfiability (SAT) solver Kissat supports a relatively narrow feature set in favor of bare-metal performance and targeted improvements to core solving techniques, which helped it dominate the International SAT Competition since 2024. However, many applications rely on advanced SAT solver features such as incremental interaction schemes, finding direct consequences of assumed literals, or expressive proof logging that allows for real-time checking. This system description reports on how we successfully adapted Kissat’s award-winning techniques to the full-featured incremental SAT solver CaDiCaL, including clausal congruence closure, clausal equivalence sweeping, and bounded variable addition. The main challenge was to support efficient linear proof production with hints. We further extended CaDiCaL’s API to extract implied literals under assumptions and applied advanced deterministic scheduling of inprocessing based on the ticks metric for approximating cache line accesses. Experiments confirm the benefits of these efforts.
Cite as
Florian Pollitt, Mathias Fleury, Katalin Fazekas, Nils Froleyks, André Schidler, Dominik Schreiber, and Armin Biere. CaDiCaL 3.0 (Tool Paper). In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 40:1-40:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{pollitt_et_al:LIPIcs.SAT.2026.40,
author = {Pollitt, Florian and Fleury, Mathias and Fazekas, Katalin and Froleyks, Nils and Schidler, Andr\'{e} and Schreiber, Dominik and Biere, Armin},
title = {{CaDiCaL 3.0}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {40:1--40:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.40},
URN = {urn:nbn:de:0030-drops-263465},
doi = {10.4230/LIPIcs.SAT.2026.40},
annote = {Keywords: Incremental SAT, CaDiCaL, SAT Solver}
}
Document
Tool Paper
Hermax: A Unified MaxSAT Library (Tool Paper)
Abstract
Despite the utility of Maximum Satisfiability (MaxSAT) in discrete optimization, developing iterative workflows remains cumbersome due to fragmented, low-level solver APIs. We present Hermax, a unified Python library and modelling compiler for MaxSAT. Hermax provides an IPAMIR interface that exposes incremental solving, assumptions, and weight updates through a single API across many incremental and non-incremental backends. Furthermore, it introduces a compiler with Constraint Programming primitives that translates high-level models directly into optimized CNF/WCNF through eager evaluation. This compiler allows automatic optimizations like integer ladder graph encoding that bypasses Pseudo-Boolean formulation when possible. Together, these features enable rapid prototyping and production grade optimization directly from Python across major platforms and hardware architectures.
Cite as
Josep Maria Salvia Hornos, Cèsar Fernández Camón, and Carles Mateu Piñol. Hermax: A Unified MaxSAT Library (Tool Paper). In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 41:1-41:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{salviahornos_et_al:LIPIcs.SAT.2026.41,
author = {Salvia Hornos, Josep Maria and Fern\'{a}ndez Cam\'{o}n, C\`{e}sar and Mateu Pi\~{n}ol, Carles},
title = {{Hermax: A Unified MaxSAT Library}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {41:1--41:13},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.41},
URN = {urn:nbn:de:0030-drops-263478},
doi = {10.4230/LIPIcs.SAT.2026.41},
annote = {Keywords: MaxSAT, Incremental Solving, IPAMIR, Python, Constraint modelling}
}
Document
Tool Paper
Unified Programmatic Access to CO Benchmarks, to Connect Constraint Solving Communities (Tool Paper)
Abstract
Many communities within Combinatorial Optimization (CO) maintain benchmark sets in heterogeneous formats, often tied to specific competitions and solver technologies. Whilst this diversity is of practical and historical importance, it also creates barriers to use and compare methods from different communities. Inspired by the more unified software ecosystem from the ML community, we propose a programmatic abstraction for CO benchmark sets. A unified programmatic interface for downloading, reading and converting datasets across formats. This includes solver-oriented benchmarks such as XCSP3, MIPLib, PB, MaxSATEval, SAT and application-oriented benchmarks such as Nurse rostering, PSPLib (RCSP), and JSPlib. To enable cross-formalism conversions, we provide loaders that bring these dataset instances into CPMpy, a modelling library for constraint programming. CPMpy provides a transformation stack; an extensive set of rewrite operations such as constraint decomposition, linearization, and Boolean encodings, that allow transforming between different constraint formalisms. Based on this, we implement file writers to multiple solver-oriented formats, including MiniZinc, LP file format (ILP), OPB, and DIMACS (W)CNF ((Max)SAT). We demonstrate that this unified abstraction facilitates cross-community access to benchmarks and systematic comparisons of solvers across paradigms.
Cite as
Thomas Sergeys, Ignace Bleukx, and Tias Guns. Unified Programmatic Access to CO Benchmarks, to Connect Constraint Solving Communities (Tool Paper). In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 42:1-42:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{sergeys_et_al:LIPIcs.SAT.2026.42,
author = {Sergeys, Thomas and Bleukx, Ignace and Guns, Tias},
title = {{Unified Programmatic Access to CO Benchmarks, to Connect Constraint Solving Communities}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {42:1--42:11},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.42},
URN = {urn:nbn:de:0030-drops-263485},
doi = {10.4230/LIPIcs.SAT.2026.42},
annote = {Keywords: CPMpy, datasets, benchmarking, constraint solving}
}
Document
Tool Paper
NLIPSat: Satisfiability-Based Nonlinear Integer Programming Encoding Toolkit (Tool Paper)
Abstract
While Maximum Satisfiability (MaxSAT) has been successfully applied to a wide range of combinatorial optimization problems, the encoding of Nonlinear Integer Programming (NLIP) with polynomial functions into MaxSAT has so far only been studied at a theoretical level. In this paper, we introduce NLIPSat, the first tool capable of encoding bounded polynomial NLIP instances directly into Maximum Satisfiability. Building upon recent MaxSAT formulations for polynomial NLIP proposed in [Zhifei Zheng et al., 2025], NLIPSat enables the encoding of polynomial nonlinear objective functions as weighted soft clauses and also supports the encoding of hard non-linear polynomial constraints within a polynomial setting. Extensive experiments on different benchmarks show that NLIPSat outperforms the state-of-the-art SMT solver Z3 by a wide margin.
Cite as
Zhengling Yangli, Zhifei Zheng, Sami Cherif, Rui Sá Shibasaki, and Chu-Min Li. NLIPSat: Satisfiability-Based Nonlinear Integer Programming Encoding Toolkit (Tool Paper). In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 43:1-43:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{yangli_et_al:LIPIcs.SAT.2026.43,
author = {Yangli, Zhengling and Zheng, Zhifei and Cherif, Sami and Shibasaki, Rui S\'{a} and Li, Chu-Min},
title = {{NLIPSat: Satisfiability-Based Nonlinear Integer Programming Encoding Toolkit}},
booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
pages = {43:1--43:13},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-431-4},
ISSN = {1868-8969},
year = {2026},
volume = {377},
editor = {Ignatiev, Alexey and Szeider, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.43},
URN = {urn:nbn:de:0030-drops-263492},
doi = {10.4230/LIPIcs.SAT.2026.43},
annote = {Keywords: Maximum Satisfiability, Nonlinear Integer Programming, Encodings, Tool}
}