Volume
LIPIcs, Volume 341
28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)
Event
SAT 2025, August 12-15, 2025, Glasgow, ScotlandEditors
Publication Details
- published at: 2025-08-07
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-381-2
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 341, SAT 2025, Complete Volume
Abstract
LIPIcs, Volume 341, SAT 2025, Complete Volume
Cite as
28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 1-566, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@Proceedings{berg_et_al:LIPIcs.SAT.2025,
title = {{LIPIcs, Volume 341, SAT 2025, Complete Volume}},
booktitle = {28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
pages = {1--566},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-381-2},
ISSN = {1868-8969},
year = {2025},
volume = {341},
editor = {Berg, Jeremias and Nordstr\"{o}m, Jakob},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025},
URN = {urn:nbn:de:0030-drops-242300},
doi = {10.4230/LIPIcs.SAT.2025},
annote = {Keywords: LIPIcs, Volume 341, SAT 2025, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 0:i-0:xx, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{berg_et_al:LIPIcs.SAT.2025.0,
author = {Berg, Jeremias and Nordstr\"{o}m, Jakob},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
pages = {0:i--0:xx},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-381-2},
ISSN = {1868-8969},
year = {2025},
volume = {341},
editor = {Berg, Jeremias and Nordstr\"{o}m, Jakob},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.0},
URN = {urn:nbn:de:0030-drops-242297},
doi = {10.4230/LIPIcs.SAT.2025.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
Privacy-Preserving SAT Solving (Invited Talk)
Abstract
This is an extended abstract of the invited talk presented at the joint conferences "28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)" and "31st International Conference on Principles and Practice of Constraint Programming (CP 2025)". The talk is based on a series of three papers published previously, and it provides a unified overview of their key ideas and results.
Cite as
Ruzica Piskac. Privacy-Preserving SAT Solving (Invited Talk). In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{piskac:LIPIcs.SAT.2025.1,
author = {Piskac, Ruzica},
title = {{Privacy-Preserving SAT Solving}},
booktitle = {28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
pages = {1:1--1:2},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-381-2},
ISSN = {1868-8969},
year = {2025},
volume = {341},
editor = {Berg, Jeremias and Nordstr\"{o}m, Jakob},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.1},
URN = {urn:nbn:de:0030-drops-237356},
doi = {10.4230/LIPIcs.SAT.2025.1},
annote = {Keywords: SAT solving, Privacy-preserving reasoning, Zero-knowledge proofs, Propositional unsatisfiability}
}
Document
Invited Talk
Anytime and Exact Search for Planning Problems: How to Explore a DP-based State Transition Graph with A*, CP and LS? (Invited Talk)
Abstract
Many planning problems may be solved with Dynamic Programming (DP) by decomposing the problem into subproblems which are recursively solved. These decompositions induce state transition graphs which are closely related to decision diagrams [J. N. Hooker, 2013], and where optimal solutions correspond to best paths in these graphs. A* is a well known algorithm which extends Djikstra’s algorithm with heuristics for guiding the path search [Hart et al., 1968]. It is exact (provided that the heuristic function is admissible), but it is not anytime. In other words, it computes a best path but it does not output sub-optimal paths while computing it. Hence, when state transition graphs have exponential sizes, A* may run out of time or memory without producing any solution. Various anytime extensions of A* have been proposed to compute a sequence of paths of increasing quality until finding an optimal path and proving its optimality.
In this talk, we will provide an overview of these exact and anytime extensions of A*, with a more detailed focus on Anytime Column Search (ACS) [Vadlamudi et al., 2012], and Iterative Memory Bounded A* (IMBA*) [L. Libralesso and F. Fontan, 2021]. Both approaches iterate A* searches while bounding the number of states that are stored or expanded at each iteration. We will also show how to combine them with Local Search (LS) in order to find better paths faster, and with bounding and constraint propagation in order to prune the graph, as proposed in [R. Fontaine et al., 2023].
This will be illustrated using the Travelling Salesman Problem (TSP) as a running example. The DP formulation introduced by Bellman in [Bellman, 1962] for the TSP has been extended to handle Time Windows (TWs) in [Christofides et al., 1981], and Time Dependent (TD) cost functions in [Malandraki and Dial, 1996]. It has also been extended to {Vehicle Routing Problems} (VRPs) in [van Hoorn, 2016] and to TD-VRPs in [Rifki et al., 2020]. We will finish by presenting an experimental comparison with state-of-the-art approaches for solving the TSP with TWs on classical benchmarks and on a new benchmark which contains hard Euclidean instances located in the phase transition zone [O. Rifki and C. Solnon, 2025].
Cite as
Christine Solnon. Anytime and Exact Search for Planning Problems: How to Explore a DP-based State Transition Graph with A*, CP and LS? (Invited Talk). In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 2:1-2:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{solnon:LIPIcs.SAT.2025.2,
author = {Solnon, Christine},
title = {{Anytime and Exact Search for Planning Problems: How to Explore a DP-based State Transition Graph with A*, CP and LS?}},
booktitle = {28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
pages = {2:1--2:2},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-381-2},
ISSN = {1868-8969},
year = {2025},
volume = {341},
editor = {Berg, Jeremias and Nordstr\"{o}m, Jakob},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.2},
URN = {urn:nbn:de:0030-drops-237366},
doi = {10.4230/LIPIcs.SAT.2025.2},
annote = {Keywords: Dynamic Programming, A*, Anytime search, Time Dependent TSP-TW}
}
Document
Problem Partitioning via Proof Prefixes
Abstract
Satisfiability solvers have been instrumental in tackling hard problems, including mathematical challenges that require years of computation. A key obstacle in efficiently solving such problems lies in effectively partitioning them into many, frequently millions of subproblems. Existing automated partitioning techniques, primarily based on lookahead methods, perform well on some instances but fail to generate effective partitions for many others.
This paper introduces a powerful partitioning approach that leverages prefixes of proofs derived from conflict-driven clause-learning solvers. This method enables non-experts to harness the power of massively parallel SAT solving for their problems. We also propose a semantically-driven partitioning technique tailored for problems with large cardinality constraints, which frequently arise in optimization tasks. We evaluate our methods on diverse benchmarks, including combinatorial problems and formulas from SAT and MaxSAT competitions. Our results demonstrate that these techniques outperform existing partitioning strategies in many cases, offering improved scalability and efficiency.
Cite as
Zachary Battleman, Joseph E. Reeves, and Marijn J. H. Heule. Problem Partitioning via Proof Prefixes. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 3:1-3:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{battleman_et_al:LIPIcs.SAT.2025.3,
author = {Battleman, Zachary and Reeves, Joseph E. and Heule, Marijn J. H.},
title = {{Problem Partitioning via Proof Prefixes}},
booktitle = {28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
pages = {3:1--3:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-381-2},
ISSN = {1868-8969},
year = {2025},
volume = {341},
editor = {Berg, Jeremias and Nordstr\"{o}m, Jakob},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.3},
URN = {urn:nbn:de:0030-drops-237378},
doi = {10.4230/LIPIcs.SAT.2025.3},
annote = {Keywords: Satisfiability solving, parallel computing, problem partitioning}
}
Document
Bit-Precise Reasoning with Parametric Bit-Vectors
Abstract
The SMT-LIB theory of bit-vectors is restricted to bit-vectors of fixed width. However, several important applications can benefit from reasoning about bit-vectors of symbolic widths, i.e., parametric bit-vectors. Recent work has introduced an approach for solving formulas over parametric bit-vectors, via an eager translation to quantified integer arithmetic with uninterpreted functions. The approach was shown to be successful for several applications, including the bit-width independent verification of compiler optimizations, invertibility conditions, and rewrite rules. We extend and improve that approach in several aspects. Theoretically, we improve expressiveness by defining a new theory of parametric bit-vectors that supports more operators and allows reasoning about the bit-widths themselves. Algorithmically, we introduce a lazy algorithm that avoids the use of uninterpreted functions and quantified axioms for them. Empirically, we show a significant improvement by implementing and evaluating our approach, and comparing it experimentally to the previous one.
Cite as
Zvika Berger, Yoni Zohar, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli. Bit-Precise Reasoning with Parametric Bit-Vectors. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 4:1-4:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{berger_et_al:LIPIcs.SAT.2025.4,
author = {Berger, Zvika and Zohar, Yoni and Niemetz, Aina and Preiner, Mathias and Reynolds, Andrew and Barrett, Clark and Tinelli, Cesare},
title = {{Bit-Precise Reasoning with Parametric Bit-Vectors}},
booktitle = {28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
pages = {4:1--4:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-381-2},
ISSN = {1868-8969},
year = {2025},
volume = {341},
editor = {Berg, Jeremias and Nordstr\"{o}m, Jakob},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.4},
URN = {urn:nbn:de:0030-drops-237385},
doi = {10.4230/LIPIcs.SAT.2025.4},
annote = {Keywords: Satisfiability Modulo Theories, Bit-precise Reasoning, Parametric Bit-vectors}
}
Document
Semi-Algebraic Proof Systems for QBF
Abstract
We introduce new semi-algebraic proof systems for Quantified Boolean Formulas (QBF) analogous to the propositional systems Nullstellensatz, Sherali-Adams and Sum-of-Squares. We transfer to this setting techniques both from the QBF literature (strategy extraction) and from propositional proof complexity (size-degree relations and pseudo-expectation). We obtain a number of strong QBF lower bounds and separations between these systems, even when disregarding propositional hardness.
Cite as
Olaf Beyersdorff, Ilario Bonacina, Kaspar Kasche, Meena Mahajan, and Luc Nicolas Spachmann. Semi-Algebraic Proof Systems for QBF. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{beyersdorff_et_al:LIPIcs.SAT.2025.5,
author = {Beyersdorff, Olaf and Bonacina, Ilario and Kasche, Kaspar and Mahajan, Meena and Spachmann, Luc Nicolas},
title = {{Semi-Algebraic Proof Systems for QBF}},
booktitle = {28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
pages = {5:1--5:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-381-2},
ISSN = {1868-8969},
year = {2025},
volume = {341},
editor = {Berg, Jeremias and Nordstr\"{o}m, Jakob},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.5},
URN = {urn:nbn:de:0030-drops-237394},
doi = {10.4230/LIPIcs.SAT.2025.5},
annote = {Keywords: QBF, Proof Complexity, Sums-of-Squares, Nullstellensatz, Sherali-Adams, Semi-Algebraic Proof Systems}
}
Document
An Algebraic Approach to MaxCSP
Abstract
Recently, there have been some attempts to base SAT and MaxSAT solvers on calculi beyond Resolution, even trying to solve SAT using MaxSAT proof systems. One of these directions was to perform MaxSAT sound inferences using polynomials over finite fields, extending the proof system Polynomial Calculus, which is known to be more powerful than Resolution.
In this work, we extend the use of the Polynomial Calculus for optimization, showing its completeness over many-valued variables. This allows using a more direct and efficient encoding of CSP problems (e.g., k-Coloring) and solving the maximization version of the problem on such encoding (e.g., Max-k-Coloring).
Cite as
Ilario Bonacina and Jordi Levy. An Algebraic Approach to MaxCSP. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 6:1-6:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{bonacina_et_al:LIPIcs.SAT.2025.6,
author = {Bonacina, Ilario and Levy, Jordi},
title = {{An Algebraic Approach to MaxCSP}},
booktitle = {28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
pages = {6:1--6:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-381-2},
ISSN = {1868-8969},
year = {2025},
volume = {341},
editor = {Berg, Jeremias and Nordstr\"{o}m, Jakob},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.6},
URN = {urn:nbn:de:0030-drops-237407},
doi = {10.4230/LIPIcs.SAT.2025.6},
annote = {Keywords: MaxCSP, Polynomial Calculus, MaxSAT}
}
Document
Redundancy Rules for MaxSAT
Abstract
The concept of redundancy in SAT leads to more expressive and powerful proof search techniques, e.g., able to express various inprocessing techniques, and originates interesting hierarchies of proof systems [Heule et.al'20, Buss-Thapen'19]. Redundancy has also been integrated in MaxSAT [Ihalainen et.al'22, Berg et.al'23, Bonacina et.al'24].
In this paper, we define a structured hierarchy of redundancy proof systems for MaxSAT, with the goal of studying its proof complexity. We obtain MaxSAT variants of proof systems such as SPR, PR, SR, and others, previously defined for SAT.
All our rules are polynomially checkable, unlike [Ihalainen et.al'22]. Moreover, they are simpler and weaker than [Berg et.al'23], and possibly amenable to lower bounds. This work also complements the approach of [Bonacina et.al'24]. Their proof systems use different rule sets for soft and hard clauses, while here we propose a system using only hard clauses and blocking variables. This is easier to integrate with current solvers and proof checkers.
We discuss the strength of the systems introduced, we show some limitations of them, and we give a short cost-SR proof that any assignment for the weak pigeonhole principle PHP^m_n falsifies at least m-n clauses.
Cite as
Ilario Bonacina, Maria Luisa Bonet, Sam Buss, and Massimo Lauria. Redundancy Rules for MaxSAT. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 7:1-7:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{bonacina_et_al:LIPIcs.SAT.2025.7,
author = {Bonacina, Ilario and Bonet, Maria Luisa and Buss, Sam and Lauria, Massimo},
title = {{Redundancy Rules for MaxSAT}},
booktitle = {28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
pages = {7:1--7:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-381-2},
ISSN = {1868-8969},
year = {2025},
volume = {341},
editor = {Berg, Jeremias and Nordstr\"{o}m, Jakob},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.7},
URN = {urn:nbn:de:0030-drops-237411},
doi = {10.4230/LIPIcs.SAT.2025.7},
annote = {Keywords: MaxSAT, Redundancy Rules, Pigeonhole Principle}
}
Document
Certifying Projected Knowledge Compilation
Abstract
Knowledge compilers convert Boolean formulas, given in conjunctive normal form (CNF), into representations that enable efficient evaluation of unweighted and weighted model counts, as well as a variety of other useful properties. With projected knowledge compilation, the generated representation describes the restriction of the formula to a designated set of data variables, with the remaining ones eliminated by existential quantification. Projected knowledge compilation has applications in a variety of domains, including formal verification and synthesis.
This paper describes a formally verified proof framework for certifying the output of a projected knowledge compiler. It builds on an earlier clausal proof framework for certifying the output of a standard knowledge compiler. Extending the framework to projected compilation requires a method to represent Skolem assignments, describing how the quantified variables can be assigned, given an assignment for the data variables. We do so by extending the representation generated by the knowledge compiler to also encode Skolem assignments. We also refine the earlier framework, moving beyond purely clausal proofs to enable scaling certification to larger formulas.
We present experimental results obtained by making small modifications to the D4 projected knowledge compiler and extensions of our earlier proof generator. We detail a soundness argument stating that a compiler output that passes our certifier is logically equivalent to the quantified input formula; the soundness argument has been formally validated using the HOL4 proof assistant. The checker also ensures that the compiler output satisfies the properties required for efficient unweighted and weighted model counting. We have developed two proof checkers for the certification framework: one written in C and designed for high performance and one written in CakeML and formally verified in HOL4.
Cite as
Randal E. Bryant, Yong Kiam Tan, and Marijn J. H. Heule. Certifying Projected Knowledge Compilation. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 8:1-8:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{bryant_et_al:LIPIcs.SAT.2025.8,
author = {Bryant, Randal E. and Tan, Yong Kiam and Heule, Marijn J. H.},
title = {{Certifying Projected Knowledge Compilation}},
booktitle = {28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
pages = {8:1--8:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-381-2},
ISSN = {1868-8969},
year = {2025},
volume = {341},
editor = {Berg, Jeremias and Nordstr\"{o}m, Jakob},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.8},
URN = {urn:nbn:de:0030-drops-237422},
doi = {10.4230/LIPIcs.SAT.2025.8},
annote = {Keywords: Knowledge Compilation, Propositional model counting, Proof checking}
}
Document
CNFs and DNFs with Exactly k Solutions
Abstract
Model counting is a fundamental problem that consists of determining the number of satisfying assignments for a given Boolean formula. The weighted variant, which computes the weighted sum of satisfying assignments, has extensive applications in probabilistic reasoning, network reliability, statistical physics, and formal verification. A common approach for solving weighted model counting is to reduce it to unweighted model counting, which raises an important question: What is the minimum number of terms (or clauses) required to construct a DNF (or CNF) formula with exactly k satisfying assignments?
In this paper, we establish both upper and lower bounds on this question. We prove that for any natural number k, one can construct a monotone DNF formula with exactly k satisfying assignments using at most O(√{log k}log log k) terms. This construction represents the first o(log k) upper bound for this problem. We complement this result by showing that there exist infinitely many values of k for which any DNF or CNF representation requires at least Ω(log log k) terms or clauses. These results have significant implications for the efficiency of model counting algorithms based on formula transformations.
Cite as
L. Sunil Chandran, Rishikesh Gajjala, and Kuldeep S. Meel. CNFs and DNFs with Exactly k Solutions. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 9:1-9:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{chandran_et_al:LIPIcs.SAT.2025.9,
author = {Chandran, L. Sunil and Gajjala, Rishikesh and Meel, Kuldeep S.},
title = {{CNFs and DNFs with Exactly k Solutions}},
booktitle = {28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
pages = {9:1--9:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-381-2},
ISSN = {1868-8969},
year = {2025},
volume = {341},
editor = {Berg, Jeremias and Nordstr\"{o}m, Jakob},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.9},
URN = {urn:nbn:de:0030-drops-237433},
doi = {10.4230/LIPIcs.SAT.2025.9},
annote = {Keywords: Model counting, #SAT, Set Systems, Combinatorics}
}
Document
Fine-Grained Complexity Analysis of Dependency Quantified Boolean Formulas
Abstract
Dependency Quantified Boolean Formulas (DQBF) extend Quantified Boolean Formulas by allowing each existential variable to depend on an explicitly specified subset of the universal variables. The satisfiability problem for DQBF is NEXP-complete in general, with only a few tractable fragments known to date. We investigate the complexity of DQBF with k existential variables (k-DQBF) under structural restrictions on the matrix - specifically, when it is in Conjunctive Normal Form (CNF) or Disjunctive Normal Form (DNF) - as well as under constraints on the dependency sets. For DNF matrices, we obtain a clear classification: 2-DQBF is PSPACE-complete, while 3-DQBF is NEXP-hard, even with disjoint dependencies. For CNF matrices, the picture is more nuanced: we show that the complexity of k-DQBF ranges from NL-complete for 2-DQBF with disjoint dependencies to NEXP-complete for 6-DQBF with arbitrary dependencies.
Cite as
Che Cheng, Long-Hin Fung, Jie-Hong Roland Jiang, Friedrich Slivovsky, and Tony Tan. Fine-Grained Complexity Analysis of Dependency Quantified Boolean Formulas. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 10:1-10:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{cheng_et_al:LIPIcs.SAT.2025.10,
author = {Cheng, Che and Fung, Long-Hin and Jiang, Jie-Hong Roland and Slivovsky, Friedrich and Tan, Tony},
title = {{Fine-Grained Complexity Analysis of Dependency Quantified Boolean Formulas}},
booktitle = {28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
pages = {10:1--10:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-381-2},
ISSN = {1868-8969},
year = {2025},
volume = {341},
editor = {Berg, Jeremias and Nordstr\"{o}m, Jakob},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.10},
URN = {urn:nbn:de:0030-drops-237441},
doi = {10.4230/LIPIcs.SAT.2025.10},
annote = {Keywords: Dependency quantified Boolean formulas, complexity, completeness, conjunctive normal form, disjunctive normal form}
}
Document
Better Extension Variables in DQBF via Independence
Abstract
We show that extension variables in (D)QBF can be generalised by conditioning on universal assignments. The benefit of this is that the dependency sets of such conditioned extension variables can be made smaller to allow easier refutations. This simple modification instantly solves many challenges in p-simulating the QBF expansion rule, which cannot be p-simulated in proof systems that have strategy extraction [Leroy Chew and Judith Clymo, 2020]. Simulating expansion is even more crucial in DQBF, where other methods are incomplete. In this paper we provide an overview of the strength of this new independent extension rule. We find that a new version of Extended Frege called IndExtFrege + ∀red can p-simulate a multitude of difficult QBF and DQBF techniques, even techniques that are difficult to approach with eFrege + ∀red. We show five p-simulations, that IndExtFrege + ∀red p-simulates QRAT, DQBF-IR-calc, IR(𝒟^rrs)-calc, Fork-Resolution and DQRAT which together underpin most DQBF solving and preprocessing techniques. The p-simulations work despite these systems using complicated rules and our new extension rule being relatively simple. Moreover, unlike recent p-simulations by eFrege + ∀red we can simulate the proof rules line by line, which allows us to mix QBF rules more easily with other inference steps.
Cite as
Leroy Chew and Tomáš Peitl. Better Extension Variables in DQBF via Independence. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 11:1-11:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{chew_et_al:LIPIcs.SAT.2025.11,
author = {Chew, Leroy and Peitl, Tom\'{a}\v{s}},
title = {{Better Extension Variables in DQBF via Independence}},
booktitle = {28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
pages = {11:1--11:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-381-2},
ISSN = {1868-8969},
year = {2025},
volume = {341},
editor = {Berg, Jeremias and Nordstr\"{o}m, Jakob},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.11},
URN = {urn:nbn:de:0030-drops-237453},
doi = {10.4230/LIPIcs.SAT.2025.11},
annote = {Keywords: DQBF, QBF, Proof Systems, Dependency Schemes, RAT, Extended Frege, Skolem functions}
}
Document
SAT-Metropolis: Combining Markov Chain Monte Carlo with SAT/SMT Sampling
Abstract
Probabilistic inference via Markov Chain Monte Carlo (MCMC) is at the core of statistical analysis and has a myriad of applications. However, probabilistic inference in the presence of hard constraints, so constraints that must hold with probability one, remains a difficult task. The reason is that hard constraints make the state space of the target distribution sparse, and may even divide it into disjoint areas separated by probability-zero states. As a consequence, the random walk performed by MCMC algorithms fails to effectively sample from the complete set of states in the target distribution. In this paper, we propose the use of SAT/SMT sampling to adapt a classic and widely used MCMC algorithm, namely Metropolis sampling. We use SAT/SMT samplers as proposal distributions. In this way, the algorithm ignores probability-zero states. Our method, sat-metropolis, effectively works in problems with multivariate polynomial hard constraints where regular Metropolis fails. We evaluate the convergence and scalability of sat-metropolis using three different state-of-the-art SAT/SMT samplers: SPUR, CMSGen, and MegaSampler. The evaluation shows how different features of the SAT/SMT sampling tools affect the effectiveness of probabilistic inference. We conclude that SAT/SMT sampling is a viable and promising technology for probabilistic inference under hard constraints.
Cite as
Maja Aaslyng Dall, Raúl Pardo, Thomas Lumley, and Andrzej Wąsowski. SAT-Metropolis: Combining Markov Chain Monte Carlo with SAT/SMT Sampling. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 12:1-12:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{dall_et_al:LIPIcs.SAT.2025.12,
author = {Dall, Maja Aaslyng and Pardo, Ra\'{u}l and Lumley, Thomas and W\k{a}sowski, Andrzej},
title = {{SAT-Metropolis: Combining Markov Chain Monte Carlo with SAT/SMT Sampling}},
booktitle = {28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
pages = {12:1--12:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-381-2},
ISSN = {1868-8969},
year = {2025},
volume = {341},
editor = {Berg, Jeremias and Nordstr\"{o}m, Jakob},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.12},
URN = {urn:nbn:de:0030-drops-237462},
doi = {10.4230/LIPIcs.SAT.2025.12},
annote = {Keywords: SAT/SMT sampling, Probabilistic inference, Markov Chain Monte Carlo}
}
Document
Random Local Access for Sampling k-SAT Solutions
Abstract
We present a sublinear time algorithm that gives random local access to the uniform distribution over satisfying assignments to an arbitrary k-SAT formula Φ, at exponential clause density. Our algorithm provides memory-less query access to variable assignments, such that the output variable assignments consistently emulate a single global satisfying assignment whose law is close to the uniform distribution over satisfying assignments to Φ. Random local access and related models have been studied for a wide variety of natural Gibbs distributions and random graphical processes. Here, we establish feasibility of random local access models for one of the most canonical such sample spaces, the set of satisfying assignments to a k-SAT formula.
Our algorithm proceeds by leveraging the local uniformity of the uniform distribution over satisfying assignments to Φ. We randomly partition the variables into two subsets, so that each clause has sufficiently many variables from each set to preserve local uniformity. We then sample some variables by simulating a systematic scan Glauber dynamics backward in time, greedily constructing the necessary intermediate steps. We sample the other variables by first conducting a search for a polylogarithmic-sized local component, which we iteratively grow to identify a small subformula from which we can efficiently sample using the appropriate marginal distribution. This two-pronged approach enables us to sample individual variable assignments without constructing a full solution.
Cite as
Dingding Dong and Nitya Mani. Random Local Access for Sampling k-SAT Solutions. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 13:1-13:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{dong_et_al:LIPIcs.SAT.2025.13,
author = {Dong, Dingding and Mani, Nitya},
title = {{Random Local Access for Sampling k-SAT Solutions}},
booktitle = {28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
pages = {13:1--13:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-381-2},
ISSN = {1868-8969},
year = {2025},
volume = {341},
editor = {Berg, Jeremias and Nordstr\"{o}m, Jakob},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.13},
URN = {urn:nbn:de:0030-drops-237474},
doi = {10.4230/LIPIcs.SAT.2025.13},
annote = {Keywords: sublinear time algorithms, random generation, k-SAT, local computation}
}
Document
Learn to Unlearn
Abstract
Clause learning is a significant milestone in the development of SAT solving. However, keeping all learned clauses without discrimination gradually slows down the solver. Thus, selectively removing some learned clauses during routine database reduction is essential. In this paper, we reexamine and test several long-standing ideas for clause removal in the modern solver Kissat. Our experiments show that retaining all clauses alters performance in all instances. For satisfiable instances, periodically removing all learned clauses surprisingly yields near state-of-the-art performance. For unsatisfiable instances, it is vital to always keep some learned clauses. Building on the influential Glucose paper, we find that it is crucial to always retain the clauses most likely to help, regardless of whether they are ranked by size or LBD in practice. Another key factor is whether a clause was used recently during conflict resolution steps. Eagerly keeping used clauses improves all unlearning strategies.
Cite as
Bernhard Gstrein, Florian Pollitt, André Schidler, Mathias Fleury, and Armin Biere. Learn to Unlearn. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 14:1-14:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{gstrein_et_al:LIPIcs.SAT.2025.14,
author = {Gstrein, Bernhard and Pollitt, Florian and Schidler, Andr\'{e} and Fleury, Mathias and Biere, Armin},
title = {{Learn to Unlearn}},
booktitle = {28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
pages = {14:1--14:12},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-381-2},
ISSN = {1868-8969},
year = {2025},
volume = {341},
editor = {Berg, Jeremias and Nordstr\"{o}m, Jakob},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.14},
URN = {urn:nbn:de:0030-drops-237480},
doi = {10.4230/LIPIcs.SAT.2025.14},
annote = {Keywords: Satisfiability solving, learned clause recycling, LBD}
}
Document
RustSAT: A Library for SAT Solving in Rust
Abstract
State-of-the-art Boolean satisfiability (SAT) solvers constitute a practical and competitive approach for solving various real-world problems. To encourage their widespread adoption, the relatively high barrier of entry following from the low level syntax of SAT and the expert knowledge required to achieve tight integration with SAT solvers should be further reduced. We present RustSAT, a library with the aim of making SAT solving technology readily available in the Rust programming language. RustSAT provides functionality for helping with generating (Max)SAT instances, writing them to, or reading them from files. Furthermore, RustSAT includes interfaces to various state-of-the-art SAT solvers available with a unified Rust API. Lastly, RustSAT implements several encodings for higher level constraints (at-most-one, cardinality, and pseudo-Boolean), which are also available via a C and Python API.
Cite as
Christoph Jabs. RustSAT: A Library for SAT Solving in Rust. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 15:1-15:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{jabs:LIPIcs.SAT.2025.15,
author = {Jabs, Christoph},
title = {{RustSAT: A Library for SAT Solving in Rust}},
booktitle = {28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
pages = {15:1--15:13},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-381-2},
ISSN = {1868-8969},
year = {2025},
volume = {341},
editor = {Berg, Jeremias and Nordstr\"{o}m, Jakob},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.15},
URN = {urn:nbn:de:0030-drops-237498},
doi = {10.4230/LIPIcs.SAT.2025.15},
annote = {Keywords: Rust, library, SAT solvers, constraint encodings}
}
Document
Depth-Optimal Quantum Layout Synthesis as SAT
Abstract
Quantum circuits consist of gates applied to qubits. Current quantum hardware platforms impose connectivity restrictions on binary CX gates. Hence, Layout Synthesis is an important step to transpile quantum circuits before they can be executed. Since CX gates are noisy, it is important to reduce the CX count or CX depth of the mapped circuits.
We provide a new and efficient encoding of Quantum-circuit Layout Synthesis in SAT. Previous SAT encodings focused on gate count and CX-gate count. Our encoding instead guarantees that we find mapped circuits with minimal circuit depth or minimal CX-gate depth. We use incremental SAT solving and parallel plans for an efficient encoding. This results in speedups of more than 10-100x compared to OLSQ2, which guarantees depth-optimality. But minimizing depth still takes more time than minimizing gate count with Q-Synth.
We correlate the noise reduction achieved by simulating circuits after (CX)-count and (CX)-depth reduction. We find that minimizing for CX-count correlates better with reducing noise than minimizing for CX-depth. However, taking into account both CX-count and CX-depth provides the best noise reduction.
Cite as
Anna B. Jakobsen, Anders B. Clausen, Jaco van de Pol, and Irfansha Shaik. Depth-Optimal Quantum Layout Synthesis as SAT. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 16:1-16:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{jakobsen_et_al:LIPIcs.SAT.2025.16,
author = {Jakobsen, Anna B. and Clausen, Anders B. and van de Pol, Jaco and Shaik, Irfansha},
title = {{Depth-Optimal Quantum Layout Synthesis as SAT}},
booktitle = {28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
pages = {16:1--16:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-381-2},
ISSN = {1868-8969},
year = {2025},
volume = {341},
editor = {Berg, Jeremias and Nordstr\"{o}m, Jakob},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.16},
URN = {urn:nbn:de:0030-drops-237501},
doi = {10.4230/LIPIcs.SAT.2025.16},
annote = {Keywords: Quantum Layout Synthesis, Transpiling, Circuit Mapping, Incremental SAT, Parallel Plans}
}
Document
Core-Guided Linear Programming-Based Maximum Satisfiability
Abstract
The core-guided algorithm OLL is the basis of some of the most successful algorithms for MaxSAT in recent evaluations. It works by iteratively finding cores of the formula and transforming it so that it exhibits a higher lower bound. It has recently been shown to implicitly discover cores of the original formula, as well as a compact representation of its reasoning within a linear program. In this paper, we use and extend these results to design a practical MaxSAT solver. We show an explicit linear program which matches and usually exceeds the bound computed by OLL. We show that OLL can be restated as an algorithm that explicitly computes a feasible dual solution of this linear program. This restated algorithm naturally works with an arbitrary dual solution. It can in fact be used to improve any LP representation of the MaxSAT instance. This presents a large increase of the potential design space for such algorithms. We describe some potential improvements from this insight and show that an implementation outperforms the state of the art algorithms on the set of instances from the latest MaxSAT evaluation.
Cite as
George Katsirelos. Core-Guided Linear Programming-Based Maximum Satisfiability. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 17:1-17:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{katsirelos:LIPIcs.SAT.2025.17,
author = {Katsirelos, George},
title = {{Core-Guided Linear Programming-Based Maximum Satisfiability}},
booktitle = {28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
pages = {17:1--17:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-381-2},
ISSN = {1868-8969},
year = {2025},
volume = {341},
editor = {Berg, Jeremias and Nordstr\"{o}m, Jakob},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.17},
URN = {urn:nbn:de:0030-drops-237513},
doi = {10.4230/LIPIcs.SAT.2025.17},
annote = {Keywords: maximum satisfiability, core-guided solvers, linear programming}
}
Document
Towards Practical First-Order Model Counting
Abstract
First-order model counting (FOMC) is the problem of counting the number of models of a sentence in first-order logic. Since lifted inference techniques rely on reductions to variants of FOMC, the design of scalable methods for FOMC has attracted attention from both theoreticians and practitioners over the past decade. Recently, a new approach based on first-order knowledge compilation was proposed. This approach, called Crane, instead of simply providing the final count, generates definitions of (possibly recursive) functions that can be evaluated with different arguments to compute the model count for any domain size. However, this approach is not fully automated, as it requires manual evaluation of the constructed functions. The primary contribution of this work is a fully automated compilation algorithm, called Crane2, which transforms the function definitions into C++ code equipped with arbitrary-precision arithmetic. These additions allow the new FOMC algorithm to scale to domain sizes over 500,000 times larger than the current state of the art, as demonstrated through experimental results.
Cite as
Ananth K. Kidambi, Guramrit Singh, Paulius Dilkas, and Kuldeep S. Meel. Towards Practical First-Order Model Counting. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 18:1-18:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{kidambi_et_al:LIPIcs.SAT.2025.18,
author = {Kidambi, Ananth K. and Singh, Guramrit and Dilkas, Paulius and Meel, Kuldeep S.},
title = {{Towards Practical First-Order Model Counting}},
booktitle = {28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
pages = {18:1--18:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-381-2},
ISSN = {1868-8969},
year = {2025},
volume = {341},
editor = {Berg, Jeremias and Nordstr\"{o}m, Jakob},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.18},
URN = {urn:nbn:de:0030-drops-237527},
doi = {10.4230/LIPIcs.SAT.2025.18},
annote = {Keywords: First-order model counting, knowledge compilation, lifted inference}
}
Document
An Application of SAT Solvers in Integer Programming Games
Abstract
Integer programming games (IPGs) are a popular game-theoretic tool to model an array of games where each player has a discrete strategy set. These games arise in important domains such as economics, transportation, cybersecurity, etc., but solving them is non-trivial as it is known that checking for the existence of pure Nash equilibria in an IPG is Σ₂^p-complete. Recent works have proposed a class of relaxed solution concepts for IPGs called locally optimal integer solutions (LOIS) and shown it to be an efficient alternative for pure Nash equilibria. While LOIS are significantly simpler to compute, they still do not scale when solved using traditional mathematical solvers, especially when high-quality solutions are desired. In this paper, we apply commercially available SAT solvers to find LOIS in IPGs. We investigate efficient encodings for a cybersecurity game and compare solution times when using SAT solvers vs mathematical program solvers. We also investigate the application of SAT solvers in graph games using a graph interdiction example and compare against the obtained LOI solutions against existing heuristics-based solutions. Our results indicate that with appropriate encodings, large-scale IPGs can be solved much more efficiently using SAT solvers. We also show that SAT solvers can be applied to graph games in conjunction with LOIS for obtaining high-quality solutions. Our results emphasize the potential of SAT solvers combined with LOIS to solve significant game theory problems.
Cite as
Pravesh Koirala, Aditya Shrey, and Forrest Laine. An Application of SAT Solvers in Integer Programming Games. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 19:1-19:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{koirala_et_al:LIPIcs.SAT.2025.19,
author = {Koirala, Pravesh and Shrey, Aditya and Laine, Forrest},
title = {{An Application of SAT Solvers in Integer Programming Games}},
booktitle = {28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
pages = {19:1--19:12},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-381-2},
ISSN = {1868-8969},
year = {2025},
volume = {341},
editor = {Berg, Jeremias and Nordstr\"{o}m, Jakob},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.19},
URN = {urn:nbn:de:0030-drops-237534},
doi = {10.4230/LIPIcs.SAT.2025.19},
annote = {Keywords: Game Theory, Integer Programming Games, SAT Solvers, Local Solutions, Graph Games}
}
Document
Scalable Precise Computation of Shannon Entropy
Abstract
Quantitative information flow analyses (QIF) are a class of techniques for measuring the amount of confidential information leaked by a program to its public outputs. Shannon entropy is an important method to quantify the amount of leakage in QIF. This paper focuses on the programs modeled in Boolean constraints and optimizes the two stages of the Shannon entropy computation to implement a scalable precise tool PSE. In the first stage, we design a knowledge compilation language called ADD[∧] that combines Algebraic Decision Diagrams and conjunctive decomposition. ADD[∧] avoids enumerating possible outputs of a program and supports tractable entropy computation. In the second stage, we optimize the model counting queries that are used to compute the probabilities of outputs. We compare PSE with the state-of-the-art probabilistic approximately correct tool EntropyEstimation, which was shown to significantly outperform the previous precise tools. The experimental results demonstrate that PSE solved 56 more benchmarks compared to EntropyEstimation in a total of 459. For 98% of the benchmarks that both PSE and EntropyEstimation solved, PSE is at least 10× as efficient as EntropyEstimation.
Cite as
Yong Lai, Haolong Tong, Zhenghang Xu, and Minghao Yin. Scalable Precise Computation of Shannon Entropy. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 20:1-20:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{lai_et_al:LIPIcs.SAT.2025.20,
author = {Lai, Yong and Tong, Haolong and Xu, Zhenghang and Yin, Minghao},
title = {{Scalable Precise Computation of Shannon Entropy}},
booktitle = {28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
pages = {20:1--20:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-381-2},
ISSN = {1868-8969},
year = {2025},
volume = {341},
editor = {Berg, Jeremias and Nordstr\"{o}m, Jakob},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.20},
URN = {urn:nbn:de:0030-drops-237540},
doi = {10.4230/LIPIcs.SAT.2025.20},
annote = {Keywords: Knowledge Compilation, Algebraic Decision Diagrams, Quantitative Information Flow, Shannon Entropy}
}
Document
Improving Reduction Techniques in Pseudo-Boolean Conflict Analysis
Abstract
Recent pseudo-Boolean (PB) solvers leverage the cutting planes proof system to perform SAT-style conflict analysis during search. This process learns implied PB constraints, which can prune later parts of the search tree and is crucial to a PB solver’s performance. A key step in PB conflict analysis is the reduction of a reason constraint, which caused a variable propagation that contributed to the conflict. While necessary, reduction generally makes the reason constraint less strong. Consequently, different approaches to reduction have been proposed, broadly categorised as division- or saturation-based, with the aim of preserving the strength of the reason constraint as much as possible.
This paper proposes two novel techniques in each reduction category. We theoretically show how each technique yields reason constraints which are at least as strong as those obtained from existing reduction methods. We then evaluate the empirical effectiveness of the reduction techniques on hard knapsack instances and the most recent PB'24 competition benchmarks.
Cite as
Orestis Lomis, Jo Devriendt, Hendrik Bierlee, and Tias Guns. Improving Reduction Techniques in Pseudo-Boolean Conflict Analysis. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 21:1-21:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{lomis_et_al:LIPIcs.SAT.2025.21,
author = {Lomis, Orestis and Devriendt, Jo and Bierlee, Hendrik and Guns, Tias},
title = {{Improving Reduction Techniques in Pseudo-Boolean Conflict Analysis}},
booktitle = {28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
pages = {21:1--21:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-381-2},
ISSN = {1868-8969},
year = {2025},
volume = {341},
editor = {Berg, Jeremias and Nordstr\"{o}m, Jakob},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.21},
URN = {urn:nbn:de:0030-drops-237551},
doi = {10.4230/LIPIcs.SAT.2025.21},
annote = {Keywords: Constraint Programming, Pseudo-Boolean Reasoning, Conflict Analysis}
}
Document
Enumerating All Boolean Matches
Abstract
Boolean matching, a fundamental problem in circuit design, determines whether two Boolean circuits are equivalent under input/output permutations and negations. While most works focus on finding a single match or proving its absence, the problem of enumerating all matches remains largely unexplored, with BooM being a notable exception. Motivated by timing challenges in Intel’s library mapping flow, we introduce EBat - an open-source tool for enumerating all matches between single-output circuits. Built from scratch, EBat reuses BooM’s SAT encoding and introduces novel high-level algorithms and performance-critical subroutines to efficiently identify and block multiple mismatches and matches simultaneously. Experiments demonstrate that EBat substantially outperforms BooM’s baseline algorithm, solving 3 to 4 times more benchmarks within a given time limit. EBat has been productized as part of Intel’s library mapping flow, effectively addressing the timing challenges.
Cite as
Alexander Nadel and Yogev Shalmon. Enumerating All Boolean Matches. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 22:1-22:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{nadel_et_al:LIPIcs.SAT.2025.22,
author = {Nadel, Alexander and Shalmon, Yogev},
title = {{Enumerating All Boolean Matches}},
booktitle = {28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
pages = {22:1--22:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-381-2},
ISSN = {1868-8969},
year = {2025},
volume = {341},
editor = {Berg, Jeremias and Nordstr\"{o}m, Jakob},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.22},
URN = {urn:nbn:de:0030-drops-237568},
doi = {10.4230/LIPIcs.SAT.2025.22},
annote = {Keywords: Boolean Matching, All-Boolean-Matching, Enumeration, SAT, Generalization}
}
Document
Symbolic Conflict Analysis in Pseudo-Boolean Optimization
Abstract
In the the last two decades, a lot of effort has been devoted to the development of satisfiability-checking tools for a variety of SAT-related problems. However, most of these tools lack optimization capabilities. That is, instead of finding any solution, one is sometimes interested in a solution that is best according to some criterion.
Pseudo-Boolean solvers can be used to deal with optimization by successively solving a series of problems that contain an additional pseudo-Boolean constraint expressing that a better solution is required. A key point for the success of this simple approach is that lemmas that are learned for one problem can be reused for subsequent ones.
In this paper we go one step further and show how, by using a simple symbolic conflict analysis procedure, not only can lemmas be reused between problems but also strengthened, thus further pruning the search space traversal. In addition, we show how this technique automatically allows one to infer upper bounds in maximization problems, thus giving an estimation of how far the solver is from finding an optimal solution. Experimental results with our PB solver reveal that (i) this technique is indeed effective in practice, providing important speedups in problems where several solutions are found and (ii) on problems with very few solutions, where the impact of our technique is limited, its overhead is negligible.
Cite as
Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, and Rui Zhao. Symbolic Conflict Analysis in Pseudo-Boolean Optimization. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{nieuwenhuis_et_al:LIPIcs.SAT.2025.23,
author = {Nieuwenhuis, Robert and Oliveras, Albert and Rodr{\'\i}guez-Carbonell, Enric and Zhao, Rui},
title = {{Symbolic Conflict Analysis in Pseudo-Boolean Optimization}},
booktitle = {28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
pages = {23:1--23:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-381-2},
ISSN = {1868-8969},
year = {2025},
volume = {341},
editor = {Berg, Jeremias and Nordstr\"{o}m, Jakob},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.23},
URN = {urn:nbn:de:0030-drops-237579},
doi = {10.4230/LIPIcs.SAT.2025.23},
annote = {Keywords: SAT, Pseudo-Boolean Optimization, Conflict Analysis}
}
Document
SAT-Based CEGAR Method for the Hamiltonian Cycle Problem Enhanced by Cut-Set Constraints
Abstract
In this paper, we propose an enhancement to the SAT-based counterexample-guided abstraction refinement (CEGAR) approach for solving the Hamiltonian Cycle Problem (HCP). Many SAT-based methods for HCP have been proposed, including a CEGAR-based method that repeatedly solves a relaxed version of HCP strengthened by counterexamples. However, when the counterexample space - represented by the full set of subcycle partitions - is large, it becomes difficult to find a solution. To address this, we introduce cut-set constraints in the refinement step, replacing traditional subcycle blocking constraints. Our evaluation shows that these cut-set constraints achieve equal or better reduction in the counterexample space, making it easier to find valid solutions. We further assessed performance using all 1001 instances from the FHCP challenge set and confirmed that the proposed method solved 937 instances within 1800 seconds, outperforming both the existing eager and CEGAR encodings (which solved at most 666 instances). This demonstrates the effectiveness of incorporating cut-set constraints into SAT-based CEGAR approaches.
Cite as
Ryoga Ohashi, Takehide Soh, Daniel Le Berre, Hidetomo Nabeshima, Mutsunori Banbara, Katsumi Inoue, and Naoyuki Tamura. SAT-Based CEGAR Method for the Hamiltonian Cycle Problem Enhanced by Cut-Set Constraints. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 24:1-24:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{ohashi_et_al:LIPIcs.SAT.2025.24,
author = {Ohashi, Ryoga and Soh, Takehide and Le Berre, Daniel and Nabeshima, Hidetomo and Banbara, Mutsunori and Inoue, Katsumi and Tamura, Naoyuki},
title = {{SAT-Based CEGAR Method for the Hamiltonian Cycle Problem Enhanced by Cut-Set Constraints}},
booktitle = {28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
pages = {24:1--24:10},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-381-2},
ISSN = {1868-8969},
year = {2025},
volume = {341},
editor = {Berg, Jeremias and Nordstr\"{o}m, Jakob},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.24},
URN = {urn:nbn:de:0030-drops-237585},
doi = {10.4230/LIPIcs.SAT.2025.24},
annote = {Keywords: Hamiltonian Cycle Problem, SAT Encoding, CEGAR}
}
Document
QRP+Gen: A Framework for Checking Q-Resolution Proofs with Generalized Axioms
Abstract
Q-resolution is a proof system for quantified Boolean formulas (QBFs) that forms the foundation for search-based QBF solvers with clause and cube learning. To derive stronger clauses and cubes, Q-resolution was extended with so-called generalized axioms. The derivation of such generalized axioms relies on solving oracles that could be, for example, SAT solvers or even QBF solvers.
While the correctness of results obtained with classical QCDCL-based solving can be efficiently certified by an independent checker, until now, proof generation had to be turned off to benefit from generalized axioms. Consequently, the results obtained with reasoning under generalized axioms could not be certified independently. To overcome this restriction, we present QRP+Gen, a novel framework to automatically generate and check Q-resolution proofs that contain generalized axioms. To this end, we extended the Q-resolution format QRP such that all necessary information is included to verify the correctness of generalized axioms. Our extension allows to integrate certificates produced by any oracle which can produce automatically checkable proofs. Furthermore, we developed a proof checker that orchestrates the proof checking of the core Q-resolution proof and the proofs produced by the oracles. As a case study, we equipped the search-based QBF solver DepQBF with proof-producing oracles for the SAT-based techniques trivial truth and trivial falsity.
Cite as
Mark Peyrer and Martina Seidl. QRP+Gen: A Framework for Checking Q-Resolution Proofs with Generalized Axioms. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 25:1-25:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{peyrer_et_al:LIPIcs.SAT.2025.25,
author = {Peyrer, Mark and Seidl, Martina},
title = {{QRP+Gen: A Framework for Checking Q-Resolution Proofs with Generalized Axioms}},
booktitle = {28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
pages = {25:1--25:10},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-381-2},
ISSN = {1868-8969},
year = {2025},
volume = {341},
editor = {Berg, Jeremias and Nordstr\"{o}m, Jakob},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.25},
URN = {urn:nbn:de:0030-drops-237592},
doi = {10.4230/LIPIcs.SAT.2025.25},
annote = {Keywords: Automated Reasoning, Quantified Resolution Proof, Generalized Axioms}
}
Document
Analyzing Reformulation Performance in Core-Guided MaxSAT Solving
Abstract
Core-guided algorithms like OLL are among the best methods for solving the Maximum Satisfiability problem (MaxSAT). Although some performance characteristics of OLL have been studied, a comprehensive experimental analysis of its reformulation behavior is still missing. In this paper, we present a large-scale study on how different reformulations of a MaxSAT instance produced by OLL affect solver performance. By representing these reformulations as a directed acyclic graph (DAG), we isolate the impact of structural features - such as the size and interconnectivity of unsatisfiable cores - on solver runtime. Our extensive experimental evaluation of over 600k solver runs reveals clear correlations between DAG properties and performance outcomes. These results suggest a new avenue for designing heuristics that steer the solver toward more tractable reformulations. All OLL DAGs and performance data from our experiments are publicly available to foster further research.
Cite as
André Schidler and Stefan Szeider. Analyzing Reformulation Performance in Core-Guided MaxSAT Solving. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{schidler_et_al:LIPIcs.SAT.2025.26,
author = {Schidler, Andr\'{e} and Szeider, Stefan},
title = {{Analyzing Reformulation Performance in Core-Guided MaxSAT Solving}},
booktitle = {28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
pages = {26:1--26:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-381-2},
ISSN = {1868-8969},
year = {2025},
volume = {341},
editor = {Berg, Jeremias and Nordstr\"{o}m, Jakob},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.26},
URN = {urn:nbn:de:0030-drops-237605},
doi = {10.4230/LIPIcs.SAT.2025.26},
annote = {Keywords: maximum satisfiability, OLL, core-guided}
}
Document
Streamlining Distributed SAT Solver Design
Abstract
Distributed clause-sharing SAT solvers have recently been established as powerful automated reasoning tools that can conquer previously infeasible instances. A common design of distributed SAT solvers is to run many off-the-shelf sequential solvers in parallel, employ some diversification (e.g., restart intervals or decision orders), and share conflict clauses among the solver threads. This approach, naïvely, adopts all best practices of sequential solver design for distributed solving, where these practices may be less useful or even actively detrimental. In this work we diagnose such shortcomings in the state-of-the-art system MallobSat and propose first effective mitigations. In particular, we replace the redundant pre- and inprocessing at all threads with single-core preprocessing that runs next to the parallel search, remove LBD values from the clause-sharing operation, and slim down solver diversification to very few lightweight and uniform methods. Experimental evaluations on up to 3072 cores (64 nodes) confirm that our measures improve performance while also drastically simplifying the SAT solving program that is run in parallel.
Cite as
Dominik Schreiber, Niccolò Rigi-Luperti, and Armin Biere. Streamlining Distributed SAT Solver Design. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 27:1-27:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{schreiber_et_al:LIPIcs.SAT.2025.27,
author = {Schreiber, Dominik and Rigi-Luperti, Niccol\`{o} and Biere, Armin},
title = {{Streamlining Distributed SAT Solver Design}},
booktitle = {28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
pages = {27:1--27:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-381-2},
ISSN = {1868-8969},
year = {2025},
volume = {341},
editor = {Berg, Jeremias and Nordstr\"{o}m, Jakob},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.27},
URN = {urn:nbn:de:0030-drops-237615},
doi = {10.4230/LIPIcs.SAT.2025.27},
annote = {Keywords: Satisfiability, parallel SAT solving, distributed computing, preprocessing}
}
Document
CNOT-Optimal Clifford Synthesis as SAT
Abstract
Clifford circuit optimization is an important step in the quantum compilation pipeline. Major compilers employ heuristic approaches. While they are fast, their results are often suboptimal. Minimization of noisy gates, like 2-qubit CNOT gates, is crucial for practical computing. Exact approaches have been proposed to fill the gap left by heuristic approaches. Among these are SAT based approaches that optimize gate count or depth, but they suffer from scalability issues. Further, they do not guarantee optimality on more important metrics like CNOT count or CNOT depth. A recent work proposed an exhaustive search only on Clifford circuits in a certain normal form to guarantee CNOT count optimality. But an exhaustive approach cannot scale beyond 6 qubits.
In this paper, we incorporate search restricted to Clifford normal forms in a SAT encoding to guarantee CNOT count optimality. By allowing parallel plans, we propose a second SAT encoding that optimizes CNOT depth. By taking advantage of flexibility in SAT based approaches, we also handle connectivity restrictions in hardware platforms, and allow for qubit relabeling. We have implemented the above encodings and variations in our open source tool Q-Synth.
In experiments, our encodings significantly outperform existing SAT approaches on random Clifford circuits. We consider practical VQE and Feynman benchmarks to compare with TKET and Qiskit compilers. In all-to-all connectivity, we observe reductions up to 32.1% in CNOT count and 48.1% in CNOT depth. Overall, we observe better results than TKET in the CNOT count and depth. We also experiment with connectivity restrictions of major quantum platforms. Compared to Qiskit, we observe up to 30.3% CNOT count and 35.9% CNOT depth further reduction.
Cite as
Irfansha Shaik and Jaco van de Pol. CNOT-Optimal Clifford Synthesis as SAT. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 28:1-28:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{shaik_et_al:LIPIcs.SAT.2025.28,
author = {Shaik, Irfansha and van de Pol, Jaco},
title = {{CNOT-Optimal Clifford Synthesis as SAT}},
booktitle = {28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
pages = {28:1--28:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-381-2},
ISSN = {1868-8969},
year = {2025},
volume = {341},
editor = {Berg, Jeremias and Nordstr\"{o}m, Jakob},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.28},
URN = {urn:nbn:de:0030-drops-237621},
doi = {10.4230/LIPIcs.SAT.2025.28},
annote = {Keywords: Circuit Synthesis, Circuit Optimization, Quantum Circuits, Propositional Satisfiability, Parallel Plans, Clifford Circuits, Encodings}
}
Document
Reencoding Unique Literal Clauses
Abstract
We present a lightweight reencoding technique that augments propositional formulas containing implicit or explicit exactly-one constraints with auxiliary variables derived from the order encoding. Our approach is based on the observation that many formulas contain clauses where each literal appears only in that clause, and that these unique literal clauses can be replaced by the corresponding sequential counter encoding of exactly-one constraints, which introduces the same variables as the order encoding. We implemented the reencoding in the state-of-the-art SAT solver CaDiCaL with support for proof logging and solution reconstruction. Experiments on SAT Competition benchmarks demonstrate that our technique enables solving dozens of additional formulas. We found that shuffling a formula before reencoding harms performance. To mitigate this issue, we introduce a method that sorts literals within clauses based on the formula structure before applying our reencoding. The same technique also predicts whether reencoding is likely to yield improvements.
Cite as
Aeacus Sheng, Joseph E. Reeves, and Marijn J. H. Heule. Reencoding Unique Literal Clauses. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 29:1-29:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{sheng_et_al:LIPIcs.SAT.2025.29,
author = {Sheng, Aeacus and Reeves, Joseph E. and Heule, Marijn J. H.},
title = {{Reencoding Unique Literal Clauses}},
booktitle = {28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
pages = {29:1--29:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-381-2},
ISSN = {1868-8969},
year = {2025},
volume = {341},
editor = {Berg, Jeremias and Nordstr\"{o}m, Jakob},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.29},
URN = {urn:nbn:de:0030-drops-237635},
doi = {10.4230/LIPIcs.SAT.2025.29},
annote = {Keywords: Satisfiability solving, auxiliary variables, graph coloring}
}
Document
Bridging Language Models and Symbolic Solvers via the Model Context Protocol
Abstract
This paper presents the MCP Solver, a system that bridges large language models with symbolic solvers through the Model Context Protocol (MCP). The system includes a server and a client component. The server provides an interface to constraint programming (via MiniZinc Python), propositional satisfiability and maximum satisfiability (both via PySAT), and SAT modulo Theories (via Python Z3). The client contains an agent that connects to the server via MCP and uses a language model to autonomously translate problem statements (given in English) into encodings through an incremental editing process and runs the solver. Our experiments demonstrate that this neurosymbolic integration effectively combines the natural language understanding of language models with robust solving capabilities across multiple solving paradigms.
Cite as
Stefan Szeider. Bridging Language Models and Symbolic Solvers via the Model Context Protocol. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 30:1-30:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{szeider:LIPIcs.SAT.2025.30,
author = {Szeider, Stefan},
title = {{Bridging Language Models and Symbolic Solvers via the Model Context Protocol}},
booktitle = {28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
pages = {30:1--30:12},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-381-2},
ISSN = {1868-8969},
year = {2025},
volume = {341},
editor = {Berg, Jeremias and Nordstr\"{o}m, Jakob},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.30},
URN = {urn:nbn:de:0030-drops-237649},
doi = {10.4230/LIPIcs.SAT.2025.30},
annote = {Keywords: Large Language Models, Agents, Constraint Programming, Satisfiability Solvers, Maximum Satisfiability, SAT Modulo Theories, Model Context Protocol}
}
Document
On Top-Down Pseudo-Boolean Model Counting
Abstract
Pseudo-Boolean model counting involves computing the number of satisfying assignments of a given pseudo-Boolean (PB) formula. In recent years, PB model counting has seen increased interest partly owing to the succinctness of PB formulas over typical propositional Boolean formulas in conjunctive normal form (CNF) at describing problem constraints. In particular, the research community has developed tools to tackle exact PB model counting. These recently developed counters follow one of the two existing major designs for model counters, namely the bottom-up model counter design. A natural question would be whether the other major design, the top-down model counter paradigm, would be effective at PB model counting, especially when the top-down design offered superior performance in CNF model counting literature.
In this work, we investigate the aforementioned top-down design for PB model counting and introduce the first exact top-down PB model counter, PBMC. PBMC is a top-down search-based counter for PB formulas, with a new variable decision heuristic that considers variable coefficients. Through our evaluations, we highlight the superior performance of PBMC at PB model counting compared to the existing state-of-the-art counters PBCount, PBCounter, and Ganak. In particular, PBMC could count for 1849 instances while the next-best competing method, PBCount, could only count for 1773 instances, demonstrating the potential of a top-down PB counter design.
Cite as
Suwei Yang, Yong Lai, and Kuldeep S. Meel. On Top-Down Pseudo-Boolean Model Counting. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 31:1-31:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{yang_et_al:LIPIcs.SAT.2025.31,
author = {Yang, Suwei and Lai, Yong and Meel, Kuldeep S.},
title = {{On Top-Down Pseudo-Boolean Model Counting}},
booktitle = {28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
pages = {31:1--31:10},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-381-2},
ISSN = {1868-8969},
year = {2025},
volume = {341},
editor = {Berg, Jeremias and Nordstr\"{o}m, Jakob},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.31},
URN = {urn:nbn:de:0030-drops-237658},
doi = {10.4230/LIPIcs.SAT.2025.31},
annote = {Keywords: Pseudo-Boolean, Model Counting, Constraint Satisfiability}
}
Document
Efficient Certified Reasoning for Binarized Neural Networks
Abstract
Neural networks have emerged as essential components in safety-critical applications - these use cases demand complex, yet trustworthy computations. Binarized Neural Networks (BNNs) are a type of neural network where each neuron is constrained to a Boolean value; they are particularly well-suited for safety-critical tasks because they retain much of the computational capacities of full-scale (floating-point or quantized) deep neural networks, but remain compatible with satisfiability solvers for qualitative verification and with model counters for quantitative reasoning. However, existing methods for BNN analysis suffer from either limited scalability or susceptibility to soundness errors, which hinders their applicability in real-world scenarios.
In this work, we present a scalable and trustworthy approach for both qualitative and quantitative verification of BNNs. Our approach introduces a native representation of BNN constraints in a custom-designed solver for qualitative reasoning, and in an approximate model counter for quantitative reasoning. We further develop specialized proof generation and checking pipelines with native support for BNN constraint reasoning, ensuring trustworthiness for all of our verification results. Empirical evaluations on a BNN robustness verification benchmark suite demonstrate that our certified solving approach achieves a 9× speedup over prior certified CNF and PB-based approaches, and our certified counting approach achieves a 218× speedup over the existing CNF-based baseline. In terms of coverage, our pipeline produces fully certified results for 99% and 86% of the qualitative and quantitative reasoning queries on BNNs, respectively. This is in sharp contrast to the best existing baselines which can fully certify only 62% and 4% of the queries, respectively.
Cite as
Jiong Yang, Yong Kiam Tan, Mate Soos, Magnus O. Myreen, and Kuldeep S. Meel. Efficient Certified Reasoning for Binarized Neural Networks. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 32:1-32:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{yang_et_al:LIPIcs.SAT.2025.32,
author = {Yang, Jiong and Tan, Yong Kiam and Soos, Mate and Myreen, Magnus O. and Meel, Kuldeep S.},
title = {{Efficient Certified Reasoning for Binarized Neural Networks}},
booktitle = {28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
pages = {32:1--32:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-381-2},
ISSN = {1868-8969},
year = {2025},
volume = {341},
editor = {Berg, Jeremias and Nordstr\"{o}m, Jakob},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.32},
URN = {urn:nbn:de:0030-drops-237665},
doi = {10.4230/LIPIcs.SAT.2025.32},
annote = {Keywords: Neural network verification, proof certification, SAT solving, approximate model counting}
}