Volume
LIPIcs, Volume 236
25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)
Event
SAT 2022, August 2-5, 2022, Haifa, IsraelEditors
Publication Details
- published at: 2022-07-28
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-242-6
- DBLP: db/conf/sat/sat2022
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 236, SAT 2022, Complete Volume
Abstract
LIPIcs, Volume 236, SAT 2022, Complete Volume
Cite as
25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 1-618, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Proceedings{meel_et_al:LIPIcs.SAT.2022,
title = {{LIPIcs, Volume 236, SAT 2022, Complete Volume}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {1--618},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022},
URN = {urn:nbn:de:0030-drops-166736},
doi = {10.4230/LIPIcs.SAT.2022},
annote = {Keywords: LIPIcs, Volume 236, SAT 2022, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 0:i-0:xviii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{meel_et_al:LIPIcs.SAT.2022.0,
author = {Meel, Kuldeep S. and Strichman, Ofer},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {0:i--0:xviii},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.0},
URN = {urn:nbn:de:0030-drops-166746},
doi = {10.4230/LIPIcs.SAT.2022.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
SAT Preprocessors and Symmetry
Abstract
Exploitation of symmetries is an indispensable approach to solve certain classes of difficult SAT instances. Numerous techniques for the use of symmetry in SAT have evolved over the past few decades. But no matter how symmetries are used precisely, they have to be detected first. We investigate how to detect more symmetry, faster. The initial idea is to reap the benefits of SAT preprocessing for symmetry detection. As it turns out, applying an off-the-shelf preprocessor before handling symmetry runs into problems: the preprocessor can haphazardly remove symmetry from formulas, severely impeding symmetry exploitation.
Our main contribution is a theoretical framework that captures the relationship of SAT preprocessing techniques and symmetry. Based on this, we create a symmetry-aware preprocessor that can be applied safely before handling symmetry. We then demonstrate that applying the preprocessor does not only substantially decrease symmetry detection and breaking times, but also uncovers hidden symmetry not detectable in the original instances. Overall, we depart the conventional view of treating symmetry detection as a black-box, presenting a new application-specific approach to symmetry detection in SAT.
Cite as
Markus Anders. SAT Preprocessors and Symmetry. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 1:1-1:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{anders:LIPIcs.SAT.2022.1,
author = {Anders, Markus},
title = {{SAT Preprocessors and Symmetry}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {1:1--1:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.1},
URN = {urn:nbn:de:0030-drops-166752},
doi = {10.4230/LIPIcs.SAT.2022.1},
annote = {Keywords: boolean satisfiability, symmetry exploitation, graph isomorphism}
}
Document
A Comprehensive Study of k-Portfolios of Recent SAT Solvers
Abstract
Hard combinatorial problems such as propositional satisfiability are ubiquitous. The holy grail are solution methods that show good performance on all problem instances. However, new approaches emerge regularly, some of which are complementary to existing solvers in that they only run faster on some instances but not on many others. While portfolios, i.e., sets of solvers, have been touted as useful, putting together such portfolios also needs to be efficient. In particular, it remains an open question how well portfolios can exploit the complementarity of solvers. This paper features a comprehensive analysis of portfolios of recent SAT solvers, the ones from the SAT Competitions 2020 and 2021. We determine optimal portfolios with exact and approximate approaches and study the impact of portfolio size k on performance. We also investigate how effective off-the-shelf prediction models are for instance-specific solver recommendations. One result is that the portfolios found with an approximate approach are as good as the optimal solution in practice. We also observe that marginal returns decrease very quickly with larger k, and our prediction models do not give way to better performance beyond very small portfolio sizes.
Cite as
Jakob Bach, Markus Iser, and Klemens Böhm. A Comprehensive Study of k-Portfolios of Recent SAT Solvers. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 2:1-2:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{bach_et_al:LIPIcs.SAT.2022.2,
author = {Bach, Jakob and Iser, Markus and B\"{o}hm, Klemens},
title = {{A Comprehensive Study of k-Portfolios of Recent SAT Solvers}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {2:1--2:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.2},
URN = {urn:nbn:de:0030-drops-166767},
doi = {10.4230/LIPIcs.SAT.2022.2},
annote = {Keywords: Propositional satisfiability, solver portfolios, runtime prediction, machine learning, integer programming}
}
Document
On the Performance of Deep Generative Models of Realistic SAT Instances
Abstract
Generating realistic random SAT instances - random SAT formulas with computational characteristics similar to the ones of application SAT benchmarks - is a challenging problem in order to understand the success of modern SAT solvers solving this kind of problems. Traditional approaches are based on probabilistic models, where a probability distribution characterizes the occurrences of variables into clauses in order to mimic a certain feature exhibited in most application formulas (e.g., community structure), but they may be unable to reproduce others. Alternatively, deep generative models have been recently proposed to address this problem. The goal of these models is to learn the whole structure of the formula without focusing on any predefined feature, in order to reproduce all its computational characteristics at once. In this work, we propose two new deep generative models of realistic SAT instances, and carry out an exhaustive experimental evaluation of these and other existing models in order to analyze their performances. Our results show that models based on graph convolutional networks, possibly enhanced with edge features, return the best results in terms of structural properties and SAT solver performance.
Cite as
Iván Garzón, Pablo Mesejo, and Jesús Giráldez-Cru. On the Performance of Deep Generative Models of Realistic SAT Instances. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 3:1-3:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{garzon_et_al:LIPIcs.SAT.2022.3,
author = {Garz\'{o}n, Iv\'{a}n and Mesejo, Pablo and Gir\'{a}ldez-Cru, Jes\'{u}s},
title = {{On the Performance of Deep Generative Models of Realistic SAT Instances}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {3:1--3:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.3},
URN = {urn:nbn:de:0030-drops-166775},
doi = {10.4230/LIPIcs.SAT.2022.3},
annote = {Keywords: Realistic SAT generators, pseudo-industrial random SAT, deep generative models, deep learning}
}
Document
A SAT Attack on Rota’s Basis Conjecture
Abstract
The SAT modulo Symmetries (SMS) is a recently introduced framework for dynamic symmetry breaking in SAT instances. It combines a CDCL SAT solver with an external lexicographic minimality checking algorithm.
We extend SMS from graphs to matroids and use it to progress on Rota’s Basis Conjecture (1989), which states that one can always decompose a collection of r disjoint bases of a rank r matroid into r disjoint rainbow bases. Through SMS, we establish that the conjecture holds for all matroids of rank 4 and certain special cases of matroids of rank 5. Furthermore, we extend SMS with the facility to produce DRAT proofs. External tools can then be used to verify the validity of additional axioms produced by the lexicographic minimality check.
As a byproduct, we have utilized our framework to enumerate matroids modulo isomorphism and to support the investigation of various other problems on matroids.
Cite as
Markus Kirchweger, Manfred Scheucher, and Stefan Szeider. A SAT Attack on Rota’s Basis Conjecture. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 4:1-4:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{kirchweger_et_al:LIPIcs.SAT.2022.4,
author = {Kirchweger, Markus and Scheucher, Manfred and Szeider, Stefan},
title = {{A SAT Attack on Rota’s Basis Conjecture}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {4:1--4:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.4},
URN = {urn:nbn:de:0030-drops-166780},
doi = {10.4230/LIPIcs.SAT.2022.4},
annote = {Keywords: SAT modulo Symmetry (SMS), dynamic symmetry breaking, Rota’s basis conjecture, matroid}
}
Document
Classes of Hard Formulas for QBF Resolution
Abstract
To date, we know only a few handcrafted quantified Boolean formulas (QBFs) that are hard for central QBF resolution systems such as Q-Res and QU-Res, and only one specific QBF family to separate Q-Res and QU-Res.
Here we provide a general method to construct hard formulas for Q-Res and QU-Res. The construction uses simple propositional formulas (e.g. minimally unsatisfiable formulas) in combination with easy QBF gadgets (Σ₂^b formulas without constant winning strategies). This leads to a host of new hard formulas, including new classes of hard random QBFs.
We further present generic constructions for formulas separating Q-Res and QU-Res, and for separating Q-Res and LD-Q-Res.
Cite as
Agnes Schleitzer and Olaf Beyersdorff. Classes of Hard Formulas for QBF Resolution. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 5:1-5:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{schleitzer_et_al:LIPIcs.SAT.2022.5,
author = {Schleitzer, Agnes and Beyersdorff, Olaf},
title = {{Classes of Hard Formulas for QBF Resolution}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {5:1--5:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.5},
URN = {urn:nbn:de:0030-drops-166792},
doi = {10.4230/LIPIcs.SAT.2022.5},
annote = {Keywords: QBF, proof complexity, resolution, separations}
}
Document
Tight Bounds for Tseitin Formulas
Abstract
We show that for any connected graph G the size of any regular resolution or OBDD(∧, reordering) refutation of a Tseitin formula based on G is at least 2^Ω(tw(G)), where tw(G) is the treewidth of G. These lower bounds improve upon the previously known bounds and, moreover, they are tight.
For both of the proof systems, there are constructive upper bounds that almost match the obtained lower bounds, hence the class of Tseitin formulas is almost automatable for regular resolution and for OBDD(∧, reordering).
Cite as
Dmitry Itsykson, Artur Riazanov, and Petr Smirnov. Tight Bounds for Tseitin Formulas. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 6:1-6:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{itsykson_et_al:LIPIcs.SAT.2022.6,
author = {Itsykson, Dmitry and Riazanov, Artur and Smirnov, Petr},
title = {{Tight Bounds for Tseitin Formulas}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {6:1--6:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.6},
URN = {urn:nbn:de:0030-drops-166805},
doi = {10.4230/LIPIcs.SAT.2022.6},
annote = {Keywords: Proof complexity, Tseitin formulas, treewidth, resolution, OBDD-based proof systems}
}
Document
Towards Learning Quantifier Instantiation in SMT
Abstract
This paper applies machine learning (ML) to solve quantified satisfiability modulo theories (SMT) problems more efficiently. The motivating idea is that the solver should learn from already solved formulas to solve new ones. This is especially relevant in classes of similar formulas.
We focus on the enumerative instantiation - a well-established approach to solving quantified formulas anchored in the Herbrand’s theorem. The task is to select the right ground terms to be instantiated. In ML parlance, this means learning to rank ground terms. We devise a series of features of the considered terms and train on them using boosted decision trees. In particular, we integrate the LightGBM library into the SMT solver cvc5. The experimental results demonstrate that the ML-guided solver enables us to solve more formulas than the base solver and reduce the number of quantifier instantiations. We also do an ablation study on the features used in the machine learning component, showing the contributions of the various additions.
Cite as
Mikoláš Janota, Jelle Piepenbrock, and Bartosz Piotrowski. Towards Learning Quantifier Instantiation in SMT. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{janota_et_al:LIPIcs.SAT.2022.7,
author = {Janota, Mikol\'{a}\v{s} and Piepenbrock, Jelle and Piotrowski, Bartosz},
title = {{Towards Learning Quantifier Instantiation in SMT}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {7:1--7:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.7},
URN = {urn:nbn:de:0030-drops-166810},
doi = {10.4230/LIPIcs.SAT.2022.7},
annote = {Keywords: satisfiability modulo theories, quantifier instantiation, machine learning}
}
Document
Introducing Intel(R) SAT Solver
Abstract
We introduce Intel(R) SAT Solver (IntelSAT) - a new open-source CDCL SAT solver, written from scratch. IntelSAT is optimized for applications which generate many mostly satisfiable incremental SAT queries. We apply the following Incremental Lazy Backtracking (ILB) principle: in-between incremental queries, backtrack only when necessary and to the highest possible decision level. ILB is enabled by a novel reimplication procedure, which can reimply an assigned literal at a lower level without backtracking. Reimplication also helped us to restore the following two properties, lost in the modern solvers with the introduction of chronological backtracking: no assigned literal can be implied at a lower level, conflict analysis always starts with a clause falsified at the lowest possible level. In addition, we apply some new heuristics. Integrating IntelSAT into the MaxSAT solver TT-Open-WBO-Inc resulted in a significant performance boost on incomplete unweighted MaxSAT Evaluation benchmarks and improved the state-of-the-art in anytime unweighted MaxSAT solving.
Cite as
Alexander Nadel. Introducing Intel(R) SAT Solver. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 8:1-8:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{nadel:LIPIcs.SAT.2022.8,
author = {Nadel, Alexander},
title = {{Introducing Intel(R) SAT Solver}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {8:1--8:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.8},
URN = {urn:nbn:de:0030-drops-166825},
doi = {10.4230/LIPIcs.SAT.2022.8},
annote = {Keywords: SAT, CDCL, MaxSAT}
}
Document
A Generalization of the Satisfiability Coding Lemma and Its Applications
Abstract
The seminal Satisfiability Coding Lemma of Paturi, Pudlák, and Zane is a coding scheme for satisfying assignments of k-CNF formulas. We generalize it to give a coding scheme for implicants and use this generalized scheme to establish new structural and algorithmic properties of prime implicants of k-CNF formulas.
Our first application is a near-optimal bound of n⋅ 3^{n(1-Ω(1/k))} on the number of prime implicants of any n-variable k-CNF formula. This resolves an open problem from the Ph.D. thesis of Talebanfard, who proved such a bound for the special case of constant-read k-CNF formulas. Our proof is algorithmic in nature, yielding an algorithm for computing the set of all prime implicants - the Blake Canonical Form - of a given k-CNF formula. The problem of computing the Blake Canonical Form of a given function is a classic one, dating back to Quine, and our work gives the first non-trivial algorithm for k-CNF formulas.
Cite as
Milan Mossé, Harry Sha, and Li-Yang Tan. A Generalization of the Satisfiability Coding Lemma and Its Applications. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{mosse_et_al:LIPIcs.SAT.2022.9,
author = {Moss\'{e}, Milan and Sha, Harry and Tan, Li-Yang},
title = {{A Generalization of the Satisfiability Coding Lemma and Its Applications}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {9:1--9:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.9},
URN = {urn:nbn:de:0030-drops-166837},
doi = {10.4230/LIPIcs.SAT.2022.9},
annote = {Keywords: Prime Implicants, Satisfiability Coding Lemma, Blake Canonical Form, k-SAT}
}
Document
Relating Existing Powerful Proof Systems for QBF
Abstract
We advance the theory of QBF proof systems by showing the first simulation of the universal checking format QRAT by a theory-friendly system. We show that the sequent system G fully p-simulates QRAT, including the Extended Universal Reduction (EUR) rule which was recently used to show QRAT does not have strategy extraction. Because EUR heavily uses resolution paths our technique also brings resolution path dependency and sequent systems closer together. While we do not recommend G for practical applications this work can potentially show what features are needed for a new QBF checking format stronger than QRAT.
Cite as
Leroy Chew and Marijn J. H. Heule. Relating Existing Powerful Proof Systems for QBF. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 10:1-10:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{chew_et_al:LIPIcs.SAT.2022.10,
author = {Chew, Leroy and Heule, Marijn J. H.},
title = {{Relating Existing Powerful Proof Systems for QBF}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {10:1--10:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.10},
URN = {urn:nbn:de:0030-drops-166845},
doi = {10.4230/LIPIcs.SAT.2022.10},
annote = {Keywords: QBF, Proof Complexity, Verification, Strategy Extraction, Sequent Calculus}
}
Document
Should Decisions in QCDCL Follow Prefix Order?
Abstract
Quantified conflict-driven clause learning (QCDCL) is one of the main solving approaches for quantified Boolean formulas (QBF). One of the differences between QCDCL and propositional CDCL is that QCDCL typically follows the prefix order of the QBF for making decisions.
We investigate an alternative model for QCDCL solving where decisions can be made in arbitrary order. The resulting system QCDCL^ANY is still sound and terminating, but does not necessarily allow to always learn asserting clauses or cubes. To address this potential drawback, we additionally introduce two subsystems that guarantee to always learn asserting clauses (QCDCL^UNI-ANI) and asserting cubes (QCDCL^EXI-ANY), respectively.
We model all four approaches by formal proof systems and show that QCDCL^UNI-ANY is exponentially better than QCDCL on false formulas, whereas QCDCL^EXI-ANY is exponentially better than QCDCL on true QBFs. Technically, this involves constructing specific QBF families and showing lower and upper bounds in the respective proof systems.
We complement our theoretical study with some initial experiments that confirm our theoretical findings.
Cite as
Benjamin Böhm, Tomáš Peitl, and Olaf Beyersdorff. Should Decisions in QCDCL Follow Prefix Order?. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{bohm_et_al:LIPIcs.SAT.2022.11,
author = {B\"{o}hm, Benjamin and Peitl, Tom\'{a}\v{s} and Beyersdorff, Olaf},
title = {{Should Decisions in QCDCL Follow Prefix Order?}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {11:1--11:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.11},
URN = {urn:nbn:de:0030-drops-166850},
doi = {10.4230/LIPIcs.SAT.2022.11},
annote = {Keywords: QBF, CDCL, proof complexity, lower bounds}
}
Document
MaxSAT-Based Bi-Objective Boolean Optimization
Abstract
We explore a maximum satisfiability (MaxSAT) based approach to bi-objective optimization. Bi-objective optimization refers to the task of finding so-called Pareto-optimal solutions in terms of two objective functions. Bi-objective optimization problems naturally arise in various real-world settings. For example, in the context of learning interpretable representations, such as decision rules, from data, one wishes to balance between two objectives, the classification error and the size of the representation. Our approach is generally applicable to bi-objective optimizations which allow for propositional encodings. The approach makes heavy use of incremental Boolean satisfiability (SAT) solving and draws inspiration from modern MaxSAT solving approaches. In particular, we describe several variants of the approach which arise from different approaches to MaxSAT solving. In addition to computing a single representative solution per each point of the Pareto front, the approach allows for enumerating all Pareto-optimal solutions. We empirically compare the efficiency of the approach to recent competing approaches, showing practical benefits of our approach in the contexts of learning interpretable classification rules and bi-objective set covering.
Cite as
Christoph Jabs, Jeremias Berg, Andreas Niskanen, and Matti Järvisalo. MaxSAT-Based Bi-Objective Boolean Optimization. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 12:1-12:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{jabs_et_al:LIPIcs.SAT.2022.12,
author = {Jabs, Christoph and Berg, Jeremias and Niskanen, Andreas and J\"{a}rvisalo, Matti},
title = {{MaxSAT-Based Bi-Objective Boolean Optimization}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {12:1--12:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.12},
URN = {urn:nbn:de:0030-drops-166863},
doi = {10.4230/LIPIcs.SAT.2022.12},
annote = {Keywords: Multi-objective optimization, Pareto front enumeration, bi-objective optimization, maximum satisfiability, incremental SAT}
}
Document
Improvements to the Implicit Hitting Set Approach to Pseudo-Boolean Optimization
Abstract
The development of practical approaches to efficiently reasoning over pseudo-Boolean constraints has recently increasing attention as a natural generalization of Boolean satisfiability (SAT) solving. Analogously, solvers for pseudo-Boolean optimization draw inspiration from techniques developed for maximum satisfiability (MaxSAT) solving. Recently, the first practical solver lifting the implicit hitting set (IHS) approach - one of the most efficient approaches in modern MaxSAT solving - to the realm of PBO was developed, employing a PB solver as a core extractor together with an integer programming solver as a hitting set solver. In this work, we make practical improvements to the IHS approach to PBO. We propose the integration of solution-improving search to the PBO-IHS approach, resulting in a hybrid approach to PBO which makes use of both types of search towards an optimal solution. Furthermore, we explore the potential of different variants of core extraction within PBO-IHS - including recent advances in PB core extraction, allowing for extracting more general PB constraints compared to the at-least-one constraints typically relied on in IHS - in speeding up PBO-IHS search. We show that the empirical efficiency of PBO-IHS - recently shown to outperform other specialized PBO solvers - is further improved by the integration of these techniques.
Cite as
Pavel Smirnov, Jeremias Berg, and Matti Järvisalo. Improvements to the Implicit Hitting Set Approach to Pseudo-Boolean Optimization. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 13:1-13:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{smirnov_et_al:LIPIcs.SAT.2022.13,
author = {Smirnov, Pavel and Berg, Jeremias and J\"{a}rvisalo, Matti},
title = {{Improvements to the Implicit Hitting Set Approach to Pseudo-Boolean Optimization}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {13:1--13:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.13},
URN = {urn:nbn:de:0030-drops-166871},
doi = {10.4230/LIPIcs.SAT.2022.13},
annote = {Keywords: constraint optimization, pseudo-Boolean optimization, implicit hitting sets, solution-improving search, unsatisfiable cores}
}
Document
Incremental Maximum Satisfiability
Abstract
Boolean satisfiability (SAT) solvers allow for incremental computations, which is key to efficient employment of SAT solvers iteratively for developing complex decision and optimization procedures, including maximum satisfiability (MaxSAT) solvers. However, enabling incremental computations on the level of constraint optimization remains a noticeable challenge. While incremental computations have been identified to have great potential in speeding up MaxSAT-based approaches for solving various real-world optimization problems, enabling incremental computations in MaxSAT remains to most extent unexplored. In this work, we contribute towards making incremental MaxSAT solving a reality. Firstly, building on the IPASIR interface for incremental SAT solving, we propose the IPAMIR interface for implementing incremental MaxSAT solvers and for developing applications making use of incremental MaxSAT. Secondly, we expand our recent adaptation of the implicit hitting set based MaxHS MaxSAT solver to a fully-fledged incremental MaxSAT solver in terms of implementing the IPAMIR specification in full, and detail in particular how, in addition to weight changes, assumptions are enabled without losing incrementality. Thirdly, we provide further empirical evidence on the benefits of incremental MaxSAT solving under assumptions.
Cite as
Andreas Niskanen, Jeremias Berg, and Matti Järvisalo. Incremental Maximum Satisfiability. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 14:1-14:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{niskanen_et_al:LIPIcs.SAT.2022.14,
author = {Niskanen, Andreas and Berg, Jeremias and J\"{a}rvisalo, Matti},
title = {{Incremental Maximum Satisfiability}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {14:1--14:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.14},
URN = {urn:nbn:de:0030-drops-166885},
doi = {10.4230/LIPIcs.SAT.2022.14},
annote = {Keywords: maximum satisfiability, MaxSAT, incremental optimization, API, implicit hitting set approach}
}
Document
Weighted Model Counting with Twin-Width
Abstract
Bonnet et al. (FOCS 2020) introduced the graph invariant twin-width and showed that many NP-hard problems are tractable for graphs of bounded twin-width, generalizing similar results for other width measures, including treewidth and clique-width. In this paper, we investigate the use of twin-width for solving the propositional satisfiability problem (SAT) and propositional model counting. We particularly focus on Bounded-ones Weighted Model Counting (BWMC), which takes as input a CNF formula F along with a bound k and asks for the weighted sum of all models with at most k positive literals. BWMC generalizes not only SAT but also (weighted) model counting.
We develop the notion of "signed" twin-width of CNF formulas and establish that BWMC is fixed-parameter tractable when parameterized by the certified signed twin-width of F plus k. We show that this result is tight: it is neither possible to drop the bound k nor use the vanilla twin-width instead if one wishes to retain fixed-parameter tractability, even for the easier problem SAT. Our theoretical results are complemented with an empirical evaluation and comparison of signed twin-width on various classes of CNF formulas.
Cite as
Robert Ganian, Filip Pokrývka, André Schidler, Kirill Simonov, and Stefan Szeider. Weighted Model Counting with Twin-Width. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{ganian_et_al:LIPIcs.SAT.2022.15,
author = {Ganian, Robert and Pokr\'{y}vka, Filip and Schidler, Andr\'{e} and Simonov, Kirill and Szeider, Stefan},
title = {{Weighted Model Counting with Twin-Width}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {15:1--15:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.15},
URN = {urn:nbn:de:0030-drops-166896},
doi = {10.4230/LIPIcs.SAT.2022.15},
annote = {Keywords: Weighted model counting, twin-width, parameterized complexity, SAT}
}
Document
Certified CNF Translations for Pseudo-Boolean Solving
Abstract
The dramatic improvements in Boolean satisfiability (SAT) solving since the turn of the millennium have made it possible to leverage state-of-the-art conflict-driven clause learning (CDCL) solvers for many combinatorial problems in academia and industry, and the use of proof logging has played a crucial role in increasing the confidence that the results these solvers produce are correct. However, the fact that SAT proof logging is performed in conjunctive normal form (CNF) clausal format means that it has not been possible to extend guarantees of correctness to the use of SAT solvers for more expressive combinatorial paradigms, where the first step is an unverified translation of the input to CNF.
In this work, we show how cutting-planes-based reasoning can provide proof logging for solvers that translate pseudo-Boolean (a.k.a. 0-1 integer linear) decision problems to CNF and then run CDCL. To support a wide range of encodings, we provide a uniform and easily extensible framework for proof logging of CNF translations. We are hopeful that this is just a first step towards providing a unified proof logging approach that will also extend to maximum satisfiability (MaxSAT) solving and pseudo-Boolean optimization in general.
Cite as
Stephan Gocht, Ruben Martins, Jakob Nordström, and Andy Oertel. Certified CNF Translations for Pseudo-Boolean Solving. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 16:1-16:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{gocht_et_al:LIPIcs.SAT.2022.16,
author = {Gocht, Stephan and Martins, Ruben and Nordstr\"{o}m, Jakob and Oertel, Andy},
title = {{Certified CNF Translations for Pseudo-Boolean Solving}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {16:1--16:25},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.16},
URN = {urn:nbn:de:0030-drops-166901},
doi = {10.4230/LIPIcs.SAT.2022.16},
annote = {Keywords: pseudo-Boolean solving, 0-1 integer linear program, proof logging, certifying algorithms, certified translation, CNF encoding, cutting planes}
}
Document
Changing Partitions in Rectangle Decision Lists
Abstract
Rectangle decision lists are a form of decision lists that were recently shown to have applications in the proof complexity of certain OBDD-based QBF-solvers. We consider a version of rectangle decision lists with changing partitions, which corresponds to QBF-solvers that may change the variable order of the OBDDs they produce. We show that even allowing one single partition change generally leads to exponentially more succinct decision lists. More generally, we show that there is a succinctness hierarchy: for every k ∈ ℕ, when going from k partition changes to k+1, there are functions that can be represented exponentially more succinctly. As an application, we show a similar hierarchy for OBDD-based QBF-solvers.
Cite as
Stefan Mengel. Changing Partitions in Rectangle Decision Lists. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 17:1-17:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{mengel:LIPIcs.SAT.2022.17,
author = {Mengel, Stefan},
title = {{Changing Partitions in Rectangle Decision Lists}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {17:1--17:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.17},
URN = {urn:nbn:de:0030-drops-166913},
doi = {10.4230/LIPIcs.SAT.2022.17},
annote = {Keywords: rectangle decision lists, QBF proof complexity, OBDD}
}
Document
Towards a SAT Encoding for Quantum Circuits: A Journey From Classical Circuits to Clifford Circuits and Beyond
Abstract
Boolean Satisfiability (SAT) techniques are well-established in classical computing where they are used to solve a broad variety of problems, e.g., in the design of classical circuits and systems. Analogous to the classical realm, quantum algorithms are usually modelled as circuits and similar design tasks need to be tackled. Thus, it is natural to pose the question whether these design tasks in the quantum realm can also be approached using SAT techniques. To the best of our knowledge, no SAT formulation for arbitrary quantum circuits exists and it is unknown whether such an approach is feasible at all. In this work, we define a propositional SAT encoding that, in principle, can be applied to arbitrary quantum circuits. However, we show that, due to the inherent complexity of representing quantum states, constructing such an encoding is not feasible in general. Therefore, we establish general criteria for determining the feasibility of the proposed encoding and identify classes of quantum circuits fulfilling these criteria. We explicitly demonstrate how the proposed encoding can be applied to the class of Clifford circuits as a representative. Finally, we empirically demonstrate the applicability and efficiency of the proposed encoding for Clifford circuits. With these results, we lay the foundation for continuing the ongoing success of SAT in classical circuit and systems design for quantum circuits.
Cite as
Lucas Berent, Lukas Burgholzer, and Robert Wille. Towards a SAT Encoding for Quantum Circuits: A Journey From Classical Circuits to Clifford Circuits and Beyond. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{berent_et_al:LIPIcs.SAT.2022.18,
author = {Berent, Lucas and Burgholzer, Lukas and Wille, Robert},
title = {{Towards a SAT Encoding for Quantum Circuits: A Journey From Classical Circuits to Clifford Circuits and Beyond}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {18:1--18:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.18},
URN = {urn:nbn:de:0030-drops-166927},
doi = {10.4230/LIPIcs.SAT.2022.18},
annote = {Keywords: Satisfiability, Quantum Computing, Design Automation, Clifford Circuits}
}
Document
On the Parallel Parameterized Complexity of MaxSAT Variants
Abstract
In the maximum satisfiability problem (max-sat) we are given a propositional formula in conjunctive normal form and have to find an assignment that satisfies as many clauses as possible. We study the parallel parameterized complexity of various versions of max-sat and provide the first constant-time algorithms parameterized either by the solution size or by the allowed excess relative to some guarantee ("above guarantee" versions). For the dual parameterized version where the parameter is the number of clauses we are allowed to leave unsatisfied, we present the first parallel algorithm for max-2sat (known as almost-2sat). The difficulty in solving almost-2sat in parallel comes from the fact that the iterative compression method, originally developed to prove that the problem is fixed-parameter tractable at all, is inherently sequential. We observe that a graph flow whose value is a parameter can be computed in parallel and use this fact to develop a parallel algorithm for the vertex cover problem parameterized above the size of a given matching. Finally, we study the parallel complexity of max-sat parameterized by the vertex cover number, the treedepth, the feedback vertex set number, and the treewidth of the input’s incidence graph. While max-sat is fixed-parameter tractable for all of these parameters, we show that they allow different degrees of possible parallelization. For all four we develop dedicated parallel algorithms that are constructive, meaning that they output an optimal assignment - in contrast to results that can be obtained by parallel meta-theorems, which often only solve the decision version.
Cite as
Max Bannach, Malte Skambath, and Till Tantau. On the Parallel Parameterized Complexity of MaxSAT Variants. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 19:1-19:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{bannach_et_al:LIPIcs.SAT.2022.19,
author = {Bannach, Max and Skambath, Malte and Tantau, Till},
title = {{On the Parallel Parameterized Complexity of MaxSAT Variants}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {19:1--19:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.19},
URN = {urn:nbn:de:0030-drops-166934},
doi = {10.4230/LIPIcs.SAT.2022.19},
annote = {Keywords: max-sat, almost-sat, parallel algorithms, fixed-parameter tractability}
}
Document
Pedant: A Certifying DQBF Solver
Abstract
Pedant is a solver for Dependency Quantified Boolean Formulas (DQBF) that combines propositional definition extraction with Counterexample-Guided Inductive Synthesis (CEGIS) to compute a model of a given formula. Pedant 2 improves upon an earlier version in several ways. We extend the notion of dependencies by allowing existential variables to depend on other existential variables. This leads to more and smaller definitions, as well as more concise repairs for counterexamples. Additionally, we reduce counterexamples by determining minimal separators in a conflict graph, and use decision tree learning to obtain default functions for undetermined variables. An experimental evaluation on standard benchmarks showed a significant increase in the number of solved instances compared to the previous version of our solver.
Cite as
Franz-Xaver Reichl and Friedrich Slivovsky. Pedant: A Certifying DQBF Solver. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 20:1-20:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{reichl_et_al:LIPIcs.SAT.2022.20,
author = {Reichl, Franz-Xaver and Slivovsky, Friedrich},
title = {{Pedant: A Certifying DQBF Solver}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {20:1--20:10},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.20},
URN = {urn:nbn:de:0030-drops-166941},
doi = {10.4230/LIPIcs.SAT.2022.20},
annote = {Keywords: DQBF, DQBF Solver, Decision Procedure, Certificates}
}
Document
The Packing Chromatic Number of the Infinite Square Grid Is at Least 14
Abstract
A packing k-coloring of a graph G = (V, E) is a mapping from V to {1, ..., k} such that any pair of vertices u, v that receive the same color c must be at distance greater than c in G. Arguably the most fundamental problem regarding packing colorings is to determine the packing chromatic number of the infinite square grid. A sequence of previous works has proved this number to be between 13 and 15. Our work improves the lower bound to 14. Moreover, we present a new encoding that is asymptotically more compact than the previously used ones.
Cite as
Bernardo Subercaseaux and Marijn J.H. Heule. The Packing Chromatic Number of the Infinite Square Grid Is at Least 14. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 21:1-21:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{subercaseaux_et_al:LIPIcs.SAT.2022.21,
author = {Subercaseaux, Bernardo and Heule, Marijn J.H.},
title = {{The Packing Chromatic Number of the Infinite Square Grid Is at Least 14}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {21:1--21:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.21},
URN = {urn:nbn:de:0030-drops-166951},
doi = {10.4230/LIPIcs.SAT.2022.21},
annote = {Keywords: packing coloring, SAT solvers, encodings}
}
Document
QBF Merge Resolution Is Powerful but Unnatural
Abstract
The Merge Resolution proof system (M-Res) for QBFs, proposed by Beyersdorff et al. in 2019, explicitly builds partial strategies inside refutations. The original motivation for this approach was to overcome the limitations encountered in long-distance Q-Resolution proof system (LD-Q-Res), where the syntactic side-conditions, while prohibiting all unsound resolutions, also end up prohibiting some sound resolutions. However, while the advantage of M-Res over many other resolution-based QBF proof systems was already demonstrated, a comparison with LD-Q-Res itself had remained open. In this paper, we settle this question. We show that M-Res has an exponential advantage over not only LD-Q-Res, but even over LQU^+-Res and IRM, the most powerful among currently known resolution-based QBF proof systems. Combining this with results from Beyersdorff et al. 2020, we conclude that M-Res is incomparable with LQU-Res and LQU^+-Res.
Our proof method reveals two additional and curious features about MRes: (i) M-Res is not closed under restrictions, and is hence not a natural proof system, and (ii) weakening axiom clauses with existential variables provably yields an exponential advantage over MRes without weakening. We further show that in the context of regular derivations, weakening axiom clauses with universal variables provably yields an exponential advantage over M-Res without weakening. These results suggest that M-Res is better used with weakening, though whether M-Res with weakening is closed under restrictions remains open. We note that even with weakening, M-Res continues to be simulated by eFrege+∀red (the simulation of ordinary M-Res was shown recently by Chew and Slivovsky).
Cite as
Meena Mahajan and Gaurav Sood. QBF Merge Resolution Is Powerful but Unnatural. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 22:1-22:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{mahajan_et_al:LIPIcs.SAT.2022.22,
author = {Mahajan, Meena and Sood, Gaurav},
title = {{QBF Merge Resolution Is Powerful but Unnatural}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {22:1--22:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.22},
URN = {urn:nbn:de:0030-drops-166969},
doi = {10.4230/LIPIcs.SAT.2022.22},
annote = {Keywords: QBF, proof complexity, resolution, weakening, restrictions}
}
Document
Quantifier Elimination in Stochastic Boolean Satisfiability
Abstract
Stochastic Boolean Satisfiability (SSAT) generalizes quantified Boolean formulas (QBFs) by allowing quantification over random variables. Its generality makes SSAT powerful to model decision or optimization problems under uncertainty. On the other hand, the generalization complicates the computation in its counting nature. In this work, we address the following two questions: 1) Is there an analogy of quantifier elimination in SSAT, similar to QBF? 2) If quantifier elimination is possible for SSAT, can it be effective for SSAT solving? We answer them affirmatively, and develop an SSAT decision procedure based on quantifier elimination. Experimental results demonstrate the unique benefits of the new method compared to the state-of-the-art solvers.
Cite as
Hao-Ren Wang, Kuan-Hua Tu, Jie-Hong Roland Jiang, and Christoph Scholl. Quantifier Elimination in Stochastic Boolean Satisfiability. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 23:1-23:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{wang_et_al:LIPIcs.SAT.2022.23,
author = {Wang, Hao-Ren and Tu, Kuan-Hua and Jiang, Jie-Hong Roland and Scholl, Christoph},
title = {{Quantifier Elimination in Stochastic Boolean Satisfiability}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {23:1--23:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.23},
URN = {urn:nbn:de:0030-drops-166970},
doi = {10.4230/LIPIcs.SAT.2022.23},
annote = {Keywords: Stochastic Boolean Satisfiability, Quantifier Elimination, Decision Procedure}
}
Document
Quantified CDCL with Universal Resolution
Abstract
Quantified Conflict-Driven Clause Learning (QCDCL) solvers for QBF generate Q-resolution proofs. Pivot variables in Q-resolution must be existentially quantified. Allowing resolution on universally quantified variables leads to a more powerful proof system called QU-resolution, but so far, QBF solvers have used QU-resolution only in very limited ways. We present a new version of QCDCL that generates proofs in QU-resolution by leveraging propositional unit propagation. We detail how conflict analysis must be adapted to handle universal variables assigned by propagation, and show that the procedure is still sound and terminating. We further describe how dependency learning can be incorporated in the algorithm to increase the flexibility of decision heuristics. Experiments with crafted instances and benchmarks from recent QBF evaluations demonstrate the viability of the resulting version of QCDCL.
Cite as
Friedrich Slivovsky. Quantified CDCL with Universal Resolution. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 24:1-24:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{slivovsky:LIPIcs.SAT.2022.24,
author = {Slivovsky, Friedrich},
title = {{Quantified CDCL with Universal Resolution}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {24:1--24:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.24},
URN = {urn:nbn:de:0030-drops-166986},
doi = {10.4230/LIPIcs.SAT.2022.24},
annote = {Keywords: QBF, Q-Resolution, QU-Resolution, CDCL}
}
Document
OptiLog V2: Model, Solve, Tune and Run
Abstract
We present an extension of the OptiLog Python framework. We fully redesign the solvers module to support the dynamic loading of incremental SAT solvers with support for external libraries. We introduce new modules for modelling problems into Non-CNF format with support for Pseudo Boolean constraints, for evaluating and parsing the results of applications, and we add support for constrained execution of blackbox programs and SAT-heritage integration. All these enhancements allow OptiLog to become a swiss knife for SAT-based applications in academic and industrial environments.
Cite as
Josep Alòs, Carlos Ansótegui, Josep M. Salvia, and Eduard Torres. OptiLog V2: Model, Solve, Tune and Run. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 25:1-25:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{alos_et_al:LIPIcs.SAT.2022.25,
author = {Al\`{o}s, Josep and Ans\'{o}tegui, Carlos and Salvia, Josep M. and Torres, Eduard},
title = {{OptiLog V2: Model, Solve, Tune and Run}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {25:1--25:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.25},
URN = {urn:nbn:de:0030-drops-166996},
doi = {10.4230/LIPIcs.SAT.2022.25},
annote = {Keywords: Tool framework, Satisfiability, Modelling, Solving}
}
Document
Analysis of Core-Guided MaxSat Using Cores and Correction Sets
Abstract
Core-guided solvers are among the best performing algorithms for solving maximum satisfiability problems. These solvers perform a sequence of relaxations of the formula to increase the lower bound on the optimal solution at each relaxation step. In addition, the relaxations allow generating a large set of minimal cores (MUSes) of the original formula. However, properties of these cores in relation to the optimization objective have not been investigated. In contrast, minimum hitting set based solvers (MaxHS) extract a set of cores that are known to have properties related to the optimization objective, e.g., the size of the minimum hitting set of the discovered cores equals the optimum when the solver terminates. In this work we analyze minimal cores and minimum correction sets (MinCSes) of the input formula and its sub-formulas that core-guided solvers produce. We demonstrate that a set of MUSes that a core-guided algorithm discovers possess the same key properties as cores extracted by MaxHS solvers. For instance, we prove the size of a minimum hitting set of these cores equals the optimal cost. We also show that it discovers all MinCSes of special subformulas of the input formula. We discuss theoretical and practical implications of our results.
Cite as
Nina Narodytska and Nikolaj Bjørner. Analysis of Core-Guided MaxSat Using Cores and Correction Sets. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 26:1-26:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{narodytska_et_al:LIPIcs.SAT.2022.26,
author = {Narodytska, Nina and Bj{\o}rner, Nikolaj},
title = {{Analysis of Core-Guided MaxSat Using Cores and Correction Sets}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {26:1--26:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.26},
URN = {urn:nbn:de:0030-drops-167006},
doi = {10.4230/LIPIcs.SAT.2022.26},
annote = {Keywords: maximum satisfiability, unsatisfiable cores, correction sets}
}
Document
Migrating Solver State
Abstract
We present approaches to store and restore the state of a SAT solver, allowing us to migrate the state between different compute resources, or even between different solvers. This can be used in many ways, e.g., to improve the fault tolerance of solvers, to schedule SAT problems on a restricted number of cores, or to use dedicated preprocessing tools for inprocessing. We identify a minimum viable subset of the solver state to migrate such that the loss of performance is small. We then present and implement two different approaches to state migration: one approach stores the state at the end of a solver run whereas the other approach stores the state continuously as part of the proof trace. We show that our approaches enable the generation of correct models and valid unsatisfiability proofs. Experimental results confirm that the overhead is reasonable and that in several cases solver performance actually improves.
Cite as
Armin Biere, Md Solimul Chowdhury, Marijn J. H. Heule, Benjamin Kiesl, and Michael W. Whalen. Migrating Solver State. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 27:1-27:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{biere_et_al:LIPIcs.SAT.2022.27,
author = {Biere, Armin and Chowdhury, Md Solimul and Heule, Marijn J. H. and Kiesl, Benjamin and Whalen, Michael W.},
title = {{Migrating Solver State}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {27:1--27:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.27},
URN = {urn:nbn:de:0030-drops-167015},
doi = {10.4230/LIPIcs.SAT.2022.27},
annote = {Keywords: SAT, SMT, Cloud Computing, Serverless Computing}
}
Document
A New Exact Solver for (Weighted) Max#SAT
Abstract
We present and evaluate d4Max, an exact approach for solving the Weighted Max#SAT problem. The Max#SAT problem extends the model counting problem (#SAT) by considering a tripartition of the variables {X, Y, Z}, and consists in maximizing over X the number of assignments to Y that can be extended to a solution with some assignment to Z. The Weighted Max#SAT problem is an extension of the Max#SAT problem with weights associated on each interpretation. We test and compare our approach with other state-of-the-art solvers on the challenging task in probabilistic inference of finding the marginal maximum a posteriori probability (MMAP) of a given subset of the variables in a Bayesian network and on exist-random quantified SSAT benchmarks. The results clearly show the overall superiority of d4Max in term of speed and number of instances solved. Moreover, we experimentally show that, in general, d4Max is able to quickly spot a solution that is close to optimal, thereby opening the door to an efficient anytime approach.
Cite as
Gilles Audemard, Jean-Marie Lagniez, and Marie Miceli. A New Exact Solver for (Weighted) Max#SAT. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 28:1-28:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{audemard_et_al:LIPIcs.SAT.2022.28,
author = {Audemard, Gilles and Lagniez, Jean-Marie and Miceli, Marie},
title = {{A New Exact Solver for (Weighted) Max#SAT}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {28:1--28:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.28},
URN = {urn:nbn:de:0030-drops-167022},
doi = {10.4230/LIPIcs.SAT.2022.28},
annote = {Keywords: Max#SAT, EMaj-SAT, Weighted Projected Model Counting, SSAT}
}
Document
SAT-Based Leximax Optimisation Algorithms
Abstract
In several real-world problems, it is often the case that the goal is to optimise several objective functions. However, usually there is not a single optimal objective vector. Instead, there are many optimal objective vectors known as Pareto-optima. Finding all Pareto-optima is computationally expensive and the number of Pareto-optima can be too large for a user to analyse. A compromise can be made by defining an optimisation criterion that integrates all objective functions.
In this paper we propose several SAT-based algorithms to solve multi-objective optimisation problems using the leximax criterion. The leximax criterion is used to obtain a Pareto-optimal solution with a small trade-off between the objective functions, which is suitable in problems where there is an absence of priorities between the objective functions. Experimental results on the Multi-Objective Package Upgradeability Optimisation problem show that the SAT-based algorithms are able to outperform the Integer Linear Programming (ILP) approach when using non-commercial ILP solvers. Additionally, experimental results on selected instances from the MaxSAT evaluation adapted to the multi-objective domain show that our approach outperforms the ILP approach using commercial solvers.
Cite as
Miguel Cabral, Mikoláš Janota, and Vasco Manquinho. SAT-Based Leximax Optimisation Algorithms. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 29:1-29:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{cabral_et_al:LIPIcs.SAT.2022.29,
author = {Cabral, Miguel and Janota, Mikol\'{a}\v{s} and Manquinho, Vasco},
title = {{SAT-Based Leximax Optimisation Algorithms}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {29:1--29:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.29},
URN = {urn:nbn:de:0030-drops-167030},
doi = {10.4230/LIPIcs.SAT.2022.29},
annote = {Keywords: Multi-Objective Optimisation, Leximax, Sorting Networks}
}
Document
Proofs for Propositional Model Counting
Abstract
Although propositional model counting (#SAT) was long considered too hard to be practical, today’s highly efficient solvers facilitate applications in probabilistic reasoning, reliability estimation, quantitative design space exploration, and more. The current trend of solvers growing more capable every year is likely to continue as a diverse range of algorithms are explored in the field. However, to establish model counters as reliable tools like SAT-solvers, correctness is as critical as speed.
As in the nature of complex systems, bugs emerge as soon as the tools are widely used. To identify and avoid bugs, explain decisions, and provide trustworthy results, we need verifiable results. We propose a novel system for certifying model counts. We show how proof traces can be generated for exact model counters based on dynamic programming, counting CDCL with component caching, and knowledge compilation to Decision-DNNF, which are the predominant techniques in today’s exact implementations. We provide proof-of-concepts for emitting proofs and a parallel trace checker. Based on this, we show the feasibility of using certified model counting in an empirical experiment.
Cite as
Johannes K. Fichte, Markus Hecher, and Valentin Roland. Proofs for Propositional Model Counting. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 30:1-30:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{fichte_et_al:LIPIcs.SAT.2022.30,
author = {Fichte, Johannes K. and Hecher, Markus and Roland, Valentin},
title = {{Proofs for Propositional Model Counting}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {30:1--30:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.30},
URN = {urn:nbn:de:0030-drops-167043},
doi = {10.4230/LIPIcs.SAT.2022.30},
annote = {Keywords: Model Counting, Verification, Certified Counting}
}
Document
QBF Programming with the Modeling Language Bule
Abstract
We introduce Bule, a modeling language for problems from the complexity class PSPACE via quantified Boolean formulas (QBF) - that is, propositional formulas in which the variables are existentially or universally quantified. Bule allows the user to write a high-level representation of the problem in a natural, rule-based language, that is inspired by stratified Datalog. We implemented a tool of the same name that converts the high-level representation into DIMACS format and thus provides an interface to aribtrary QBF solvers, so that the modeled problems can also be solved. We analyze the complexity-theoretic properties of our modeling language, provide a library for common modeling patterns, and evaluate our language and tool on several examples.
Cite as
Jean Christoph Jung, Valentin Mayer-Eichberger, and Abdallah Saffidine. QBF Programming with the Modeling Language Bule. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 31:1-31:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{jung_et_al:LIPIcs.SAT.2022.31,
author = {Jung, Jean Christoph and Mayer-Eichberger, Valentin and Saffidine, Abdallah},
title = {{QBF Programming with the Modeling Language Bule}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {31:1--31:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.31},
URN = {urn:nbn:de:0030-drops-167058},
doi = {10.4230/LIPIcs.SAT.2022.31},
annote = {Keywords: Modeling, QBF Programming, CNF Encodings}
}