Volume
LIPIcs, Volume 271
26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)
Event
SAT 2023, July 4-8, 2023, Alghero, ItalyEditors
Publication Details
- published at: 2023-08-09
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-286-0
- DBLP: db/conf/sat/sat2023
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 271, SAT 2023, Complete Volume
Abstract
LIPIcs, Volume 271, SAT 2023, Complete Volume
Cite as
26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 1-522, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@Proceedings{mahajan_et_al:LIPIcs.SAT.2023,
title = {{LIPIcs, Volume 271, SAT 2023, Complete Volume}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {1--522},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-286-0},
ISSN = {1868-8969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023},
URN = {urn:nbn:de:0030-drops-184615},
doi = {10.4230/LIPIcs.SAT.2023},
annote = {Keywords: LIPIcs, Volume 271, SAT 2023, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 0:i-0:xviii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{mahajan_et_al:LIPIcs.SAT.2023.0,
author = {Mahajan, Meena and Slivovsky, Friedrich},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {0:i--0:xviii},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-286-0},
ISSN = {1868-8969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.0},
URN = {urn:nbn:de:0030-drops-184625},
doi = {10.4230/LIPIcs.SAT.2023.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Algorithms Transcending the SAT-Symmetry Interface
Abstract
Dedicated treatment of symmetries in satisfiability problems (SAT) is indispensable for solving various classes of instances arising in practice. However, the exploitation of symmetries usually takes a black box approach. Typically, off-the-shelf external, general-purpose symmetry detection tools are invoked to compute symmetry groups of a formula. The groups thus generated are a set of permutations passed to a separate tool to perform further analyzes to understand the structure of the groups. The result of this second computation is in turn used for tasks such as static symmetry breaking or dynamic pruning of the search space. Within this pipeline of tools, the detection and analysis of symmetries typically incurs the majority of the time overhead for symmetry exploitation.
In this paper we advocate for a more holistic view of what we call the SAT-symmetry interface. We formulate a computational setting, centered around a new concept of joint graph/group pairs, to analyze and improve the detection and analysis of symmetries. Using our methods, no information is lost performing computational tasks lying on the SAT-symmetry interface. Having access to the entire input allows for simpler, yet efficient algorithms.
Specifically, we devise algorithms and heuristics for computing finest direct disjoint decompositions, finding equivalent orbits, and finding natural symmetric group actions. Our algorithms run in what we call instance-quasi-linear time, i.e., almost linear time in terms of the input size of the original formula and the description length of the symmetry group returned by symmetry detection tools. Our algorithms improve over both heuristics used in state-of-the-art symmetry exploitation tools, as well as theoretical general-purpose algorithms.
Cite as
Markus Anders, Pascal Schweitzer, and Mate Soos. Algorithms Transcending the SAT-Symmetry Interface. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 1:1-1:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{anders_et_al:LIPIcs.SAT.2023.1,
author = {Anders, Markus and Schweitzer, Pascal and Soos, Mate},
title = {{Algorithms Transcending the SAT-Symmetry Interface}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {1:1--1:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-286-0},
ISSN = {1868-8969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.1},
URN = {urn:nbn:de:0030-drops-184635},
doi = {10.4230/LIPIcs.SAT.2023.1},
annote = {Keywords: boolean satisfiability, symmetry exploitation, computational group theory}
}
Document
Proof Complexity of Propositional Model Counting
Abstract
Recently, the proof system MICE for the model counting problem #SAT was introduced by Fichte, Hecher and Roland (SAT'22). As demonstrated by Fichte et al., the system MICE can be used for proof logging for state-of-the-art #SAT solvers.
We perform a proof-complexity study of MICE. For this we first simplify the rules of MICE and obtain a calculus MICE' that is polynomially equivalent to MICE. Our main result establishes an exponential lower bound for the number of proof steps in MICE' (and hence also in MICE) for a specific family of CNFs.
Cite as
Olaf Beyersdorff, Tim Hoffmann, and Luc Nicolas Spachmann. Proof Complexity of Propositional Model Counting. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 2:1-2:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{beyersdorff_et_al:LIPIcs.SAT.2023.2,
author = {Beyersdorff, Olaf and Hoffmann, Tim and Spachmann, Luc Nicolas},
title = {{Proof Complexity of Propositional Model Counting}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {2:1--2:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-286-0},
ISSN = {1868-8969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.2},
URN = {urn:nbn:de:0030-drops-184647},
doi = {10.4230/LIPIcs.SAT.2023.2},
annote = {Keywords: model counting, #SAT, proof complexity, proof systems, lower bounds}
}
Document
CadiBack: Extracting Backbones with CaDiCaL
Abstract
The backbone of a satisfiable formula is the set of literals that are true in all its satisfying assignments. Backbone computation can improve a wide range of SAT-based applications, such as verification, fault localization and product configuration. In this tool paper, we introduce a new backbone extraction tool called CadiBack. It takes advantage of unique features available in our state-of-the-art SAT solver CaDiCaL including transparent inprocessing and single clause assumptions, which have not been evaluated in this context before. In addition, CaDiCaL is enhanced with an improved algorithm to support model rotation by utilizing watched literal data structures. In our comprehensive experiments with a large number of benchmarks, CadiBack solves 60% more instances than the state-of-the-art backbone extraction tool MiniBones. Our tool is thoroughly tested with fuzzing, internal correctness checking and cross-checking on a large benchmark set. It is publicly available as open source, well documented and easy to extend.
Cite as
Armin Biere, Nils Froleyks, and Wenxi Wang. CadiBack: Extracting Backbones with CaDiCaL. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 3:1-3:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{biere_et_al:LIPIcs.SAT.2023.3,
author = {Biere, Armin and Froleyks, Nils and Wang, Wenxi},
title = {{CadiBack: Extracting Backbones with CaDiCaL}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {3:1--3:12},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-286-0},
ISSN = {1868-8969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.3},
URN = {urn:nbn:de:0030-drops-184655},
doi = {10.4230/LIPIcs.SAT.2023.3},
annote = {Keywords: Satisfiability, Backbone, Incremental Solving}
}
Document
QCDCL vs QBF Resolution: Further Insights
Abstract
We continue the investigation on the relations of QCDCL and QBF resolution systems. In particular, we introduce QCDCL versions that tightly characterise QU-Resolution and (a slight variant of) long-distance Q-Resolution. We show that most QCDCL variants - parameterised by different policies for decisions, unit propagations and reductions - lead to incomparable systems for almost all choices of these policies.
Cite as
Benjamin Böhm and Olaf Beyersdorff. QCDCL vs QBF Resolution: Further Insights. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 4:1-4:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{bohm_et_al:LIPIcs.SAT.2023.4,
author = {B\"{o}hm, Benjamin and Beyersdorff, Olaf},
title = {{QCDCL vs QBF Resolution: Further Insights}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {4:1--4:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-286-0},
ISSN = {1868-8969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.4},
URN = {urn:nbn:de:0030-drops-184660},
doi = {10.4230/LIPIcs.SAT.2023.4},
annote = {Keywords: QBF, CDCL, resolution, proof complexity, simulations, lower bounds}
}
Document
Polynomial Calculus for MaxSAT
Abstract
MaxSAT is the problem of finding an assignment satisfying the maximum number of clauses in a CNF formula. We consider a natural generalization of this problem to generic sets of polynomials and propose a weighted version of Polynomial Calculus to address this problem.
Weighted Polynomial Calculus is a natural generalization of MaxSAT-Resolution and weighted Resolution that manipulates polynomials with coefficients in a finite field and either weights in ℕ or ℤ. We show the soundness and completeness of these systems via an algorithmic procedure.
Weighted Polynomial Calculus, with weights in ℕ and coefficients in 𝔽₂, is able to prove efficiently that Tseitin formulas on a connected graph are minimally unsatisfiable. Using weights in ℤ, it also proves efficiently that the Pigeonhole Principle is minimally unsatisfiable.
Cite as
Ilario Bonacina, Maria Luisa Bonet, and Jordi Levy. Polynomial Calculus for MaxSAT. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 5:1-5:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{bonacina_et_al:LIPIcs.SAT.2023.5,
author = {Bonacina, Ilario and Bonet, Maria Luisa and Levy, Jordi},
title = {{Polynomial Calculus for MaxSAT}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {5:1--5:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-286-0},
ISSN = {1868-8969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.5},
URN = {urn:nbn:de:0030-drops-184670},
doi = {10.4230/LIPIcs.SAT.2023.5},
annote = {Keywords: Polynomial Calculus, MaxSAT, Proof systems, Algebraic reasoning}
}
Document
Certified Knowledge Compilation with Application to Verified Model Counting
Abstract
Computing many useful properties of Boolean formulas, such as their weighted or unweighted model count, is intractable on general representations. It can become tractable when formulas are expressed in a special form, such as the decision-decomposable, negation normal form (dec-DNNF) . Knowledge compilation is the process of converting a formula into such a form. Unfortunately existing knowledge compilers provide no guarantee that their output correctly represents the original formula, and therefore they cannot validate a model count, or any other computed value.
We present Partitioned-Operation Graphs (POGs), a form that can encode all of the representations used by existing knowledge compilers. We have designed CPOG, a framework that can express proofs of equivalence between a POG and a Boolean formula in conjunctive normal form (CNF).
We have developed a program that generates POG representations from dec-DNNF graphs produced by the state-of-the-art knowledge compiler D4, as well as checkable CPOG proofs certifying that the output POGs are equivalent to the input CNF formulas. Our toolchain for generating and verifying POGs scales to all but the largest graphs produced by D4 for formulas from a recent model counting competition. Additionally, we have developed a formally verified CPOG checker and model counter for POGs in the Lean 4 proof assistant. In doing so, we proved the soundness of our proof framework. These programs comprise the first formally verified toolchain for weighted and unweighted model counting.
Cite as
Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad, and Marijn J. H. Heule. Certified Knowledge Compilation with Application to Verified Model Counting. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 6:1-6:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{bryant_et_al:LIPIcs.SAT.2023.6,
author = {Bryant, Randal E. and Nawrocki, Wojciech and Avigad, Jeremy and Heule, Marijn J. H.},
title = {{Certified Knowledge Compilation with Application to Verified Model Counting}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {6:1--6:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-286-0},
ISSN = {1868-8969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.6},
URN = {urn:nbn:de:0030-drops-184685},
doi = {10.4230/LIPIcs.SAT.2023.6},
annote = {Keywords: Propositional model counting, Proof checking}
}
Document
Separating Incremental and Non-Incremental Bottom-Up Compilation
Abstract
The aim of a compiler is, given a function represented in some language, to generate an equivalent representation in a target language L. In bottom-up (BU) compilation of functions given as CNF formulas, constructing the new representation requires compiling several subformulas in L. The compiler starts by compiling the clauses in L and iteratively constructs representations for new subformulas using an "Apply" operator that performs conjunction in L, until all clauses are combined into one representation. In principle, BU compilation can generate representations for any subformulas and conjoin them in any way. But an attractive strategy from a practical point of view is to augment one main representation - which we call the core - by conjoining to it the clauses one at a time. We refer to this strategy as incremental BU compilation. We prove that, for known relevant languages L for BU compilation, there is a class of CNF formulas that admit BU compilations to L that generate only polynomial-size intermediate representations, while their incremental BU compilations all generate an exponential-size core.
Cite as
Alexis de Colnet. Separating Incremental and Non-Incremental Bottom-Up Compilation. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 7:1-7:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{decolnet:LIPIcs.SAT.2023.7,
author = {de Colnet, Alexis},
title = {{Separating Incremental and Non-Incremental Bottom-Up Compilation}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {7:1--7:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-286-0},
ISSN = {1868-8969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.7},
URN = {urn:nbn:de:0030-drops-184696},
doi = {10.4230/LIPIcs.SAT.2023.7},
annote = {Keywords: Knowledge Compilation, Bottom-up Compilation, DNNF, OBDD}
}
Document
IPASIR-UP: User Propagators for CDCL
Abstract
Modern SAT solvers are frequently embedded as sub-reasoning engines into more complex tools for addressing problems beyond the Boolean satisfiability problem. Examples include solvers for Satisfiability Modulo Theories (SMT), combinatorial optimization, model enumeration and counting. In such use cases, the SAT solver is often able to provide relevant information beyond the satisfiability answer. Further, domain knowledge of the embedding system (e.g., symmetry properties or theory axioms) can be beneficial for the CDCL search, but cannot be efficiently represented in clausal form. In this paper, we propose a general interface to inspect and influence the internal behaviour of CDCL SAT solvers. Our goal is to capture the most essential functionalities that are sufficient to simplify and improve use cases that require a more fine-grained interaction with the SAT solver than provided via the standard IPASIR interface. For our experiments, we extend CaDiCaL with our interface and evaluate it on two representative use cases: enumerating graphs within the SAT modulo Symmetries framework (SMS), and as the main CDCL(T) SAT engine of the SMT solver cvc5.
Cite as
Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, and Armin Biere. IPASIR-UP: User Propagators for CDCL. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 8:1-8:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{fazekas_et_al:LIPIcs.SAT.2023.8,
author = {Fazekas, Katalin and Niemetz, Aina and Preiner, Mathias and Kirchweger, Markus and Szeider, Stefan and Biere, Armin},
title = {{IPASIR-UP: User Propagators for CDCL}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {8:1--8:13},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-286-0},
ISSN = {1868-8969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.8},
URN = {urn:nbn:de:0030-drops-184709},
doi = {10.4230/LIPIcs.SAT.2023.8},
annote = {Keywords: SAT, CDCL, Satisfiability Modulo Theories, Satisfiability Modulo Symmetries}
}
Document
AllSAT for Combinational Circuits
Abstract
Motivated by the need to improve the scalability of Intel’s in-house Static Timing Analysis (STA) tool, we consider the problem of enumerating all the solutions of a single-output combinational Boolean circuit, called AllSAT-CT. While AllSAT-CT is immediately reducible to enumerating the solutions of a Boolean formula in Conjunctive Normal Form (AllSAT-CNF), our experiments had shown that such a reduction, followed by applying state-of-the-art AllSAT-CNF tools, does not scale well on neither our industrial AllSAT-CT instances nor generic circuits, both when the user requires the solutions to be disjoint or when they can be non-disjoint. We focused on understanding the reasons for this phenomenon for the well-known iterative blocking family of AllSAT-CNF algorithms. We realized that existing blocking AllSAT-CNF algorithms fail to generalize efficiently for AllSAT-CT, since they are restricted to Boolean logic. Consequently, we introduce three dedicated AllSAT-CT algorithms that are ternary-logic-aware: a ternary simulation-based algorithm TALE, a dual-rail&MaxSAT-based algorithm MARS, and their combination. Specifically, we introduce in MARS two novel blocking clause generation approaches for the disjoint and non-disjoint cases. We implemented our algorithms in our new tool HALL. We show that HALL scales substantially better than any reduction to existing AllSAT-CNF tools on our industrial STA instances as well as on publicly available families of combinational circuits for both the disjoint and the non-disjoint cases.
Cite as
Dror Fried, Alexander Nadel, and Yogev Shalmon. AllSAT for Combinational Circuits. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{fried_et_al:LIPIcs.SAT.2023.9,
author = {Fried, Dror and Nadel, Alexander and Shalmon, Yogev},
title = {{AllSAT for Combinational Circuits}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {9:1--9:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-286-0},
ISSN = {1868-8969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.9},
URN = {urn:nbn:de:0030-drops-184717},
doi = {10.4230/LIPIcs.SAT.2023.9},
annote = {Keywords: AllSAT, SAT, Circuits}
}
Document
On the Complexity of k-DQBF
Abstract
Recently Dependency Quantified Boolean Formula (DQBF) has attracted a lot of attention in the SAT community. Intuitively, a DQBF is a natural extension of quantified boolean formula where for each existential variable, one can specify the set of universal variables it depends on. It has been observed that a DQBF with k existential variables - henceforth denoted by k-DQBF - is essentially a k-CNF formula in succinct representation. However, beside this and the fact that the satisfiability problem is NEXP-complete, not much is known about DQBF.
In this paper we take a closer look at k-DQBF and show that a number of well known classical results on k-SAT can indeed be lifted to k-DQBF, which shows a strong resemblance between k-SAT and k-DQBF. More precisely, we show the following.
a) The satisfiability problem for 2- and 3-DQBF is PSPACE- and NEXP-complete, respectively.
b) There is a parsimonious polynomial time reduction from arbitrary DQBF to 3-DQBF.
c) Many polynomial time projections from SAT to languages in NP can be lifted to polynomial time reductions from the satisfiability of DQBF to languages in NEXP.
d) Languages in the class NSPACE[s(n)] can be reduced to the satisfiability of 2-DQBF with O(s(n)) universal variables.
e) Languages in the class NTIME[t(n)] can be reduced to the satisfiability of 3-DQBF with O(log t(n)) universal variables.
The first result parallels the well known classical results that 2-SAT and 3-SAT are NL- and NP-complete, respectively.
Cite as
Long-Hin Fung and Tony Tan. On the Complexity of k-DQBF. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 10:1-10:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{fung_et_al:LIPIcs.SAT.2023.10,
author = {Fung, Long-Hin and Tan, Tony},
title = {{On the Complexity of k-DQBF}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {10:1--10:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-286-0},
ISSN = {1868-8969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.10},
URN = {urn:nbn:de:0030-drops-184729},
doi = {10.4230/LIPIcs.SAT.2023.10},
annote = {Keywords: Dependency quantified boolean formulas, existential variables, complexity}
}
Document
Effective Auxiliary Variables via Structured Reencoding
Abstract
Extended resolution shows that auxiliary variables are very powerful in theory. However, attempts to exploit this potential in practice have had limited success. One reasonably effective method in this regard is bounded variable addition (BVA), which automatically reencodes formulas by introducing new variables and eliminating clauses, often significantly reducing formula size. We find motivating examples suggesting that the performance improvement caused by BVA stems not only from this size reduction but also from the introduction of effective auxiliary variables. Analyzing specific packing-coloring instances, we discover that BVA is fragile with respect to formula randomization, relying on variable order to break ties. With this understanding, we augment BVA with a heuristic for breaking ties in a structured way. We evaluate our new preprocessing technique, Structured BVA (SBVA), on more than 29 000 formulas from previous SAT competitions and show that it is robust to randomization. In a simulated competition setting, our implementation outperforms BVA on both randomized and original formulas, and appears to be well-suited for certain families of formulas.
Cite as
Andrew Haberlandt, Harrison Green, and Marijn J. H. Heule. Effective Auxiliary Variables via Structured Reencoding. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{haberlandt_et_al:LIPIcs.SAT.2023.11,
author = {Haberlandt, Andrew and Green, Harrison and Heule, Marijn J. H.},
title = {{Effective Auxiliary Variables via Structured Reencoding}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {11:1--11:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-286-0},
ISSN = {1868-8969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.11},
URN = {urn:nbn:de:0030-drops-184736},
doi = {10.4230/LIPIcs.SAT.2023.11},
annote = {Keywords: Reencoding, Auxiliary Variables, Extended Resolution}
}
Document
An Analysis of Core-Guided Maximum Satisfiability Solvers Using Linear Programming
Abstract
Many current complete MaxSAT algorithms fall into two categories: core-guided or implicit hitting set. The two kinds of algorithms seem to have complementary strengths in practice, so that each kind of solver is better able to handle different families of instances. This suggests that a hybrid might match and outperform either, but the techniques used seem incompatible. In this paper, we focus on PMRES and OLL, two core-guided algorithms based on max resolution and soft cardinality constraints, respectively. We show that these algorithms implicitly discover cores of the original formula, as has been previously shown for PM1. Moreover, we show that in some cases, including unweighted instances, they compute the optimum hitting set of these cores at each iteration. We also give compact integer linear programs for each which encode this hitting set problem. Importantly, their continuous relaxation has an optimum that matches the bound computed by the respective algorithms. This goes some way towards resolving the incompatibility of implicit hitting set and core-guided algorithms, since solvers based on the implicit hitting set algorithm typically solve the problem by encoding it as a linear program.
Cite as
George Katsirelos. An Analysis of Core-Guided Maximum Satisfiability Solvers Using Linear Programming. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 12:1-12:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{katsirelos:LIPIcs.SAT.2023.12,
author = {Katsirelos, George},
title = {{An Analysis of Core-Guided Maximum Satisfiability Solvers Using Linear Programming}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {12:1--12:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-286-0},
ISSN = {1868-8969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.12},
URN = {urn:nbn:de:0030-drops-184745},
doi = {10.4230/LIPIcs.SAT.2023.12},
annote = {Keywords: maximum satisfiability, core-guided solvers, minimum hitting set problem, linear programming}
}
Document
A SAT Solver’s Opinion on the Erdős-Faber-Lovász Conjecture
Abstract
In 1972, Paul Erdős, Vance Faber, and Lászlo Lovász asked whether every linear hypergraph with n vertices can be edge-colored with n colors, a statement that has come to be known as the EFL conjecture. Erdős himself considered the conjecture as one of his three favorite open problems, and offered increasing money prizes for its solution on several occasions. A proof of the conjecture was recently announced, for all but a finite number of hypergraphs. In this paper we look at some of the cases not covered by this proof.
We use SAT solvers, and in particular the SAT Modulo Symmetries (SMS) framework, to generate non-colorable linear hypergraphs with a fixed number of vertices and hyperedges modulo isomorphisms. Since hypergraph colorability is NP-hard, we cannot directly express in a propositional formula that we want only non-colorable hypergraphs. Instead, we use one SAT (SMS) solver to generate candidate hypergraphs modulo isomorphisms, and another to reject them by finding a coloring. Each successive candidate is required to defeat all previous colorings, whereby we avoid having to generate and test all linear hypergraphs.
Computational methods have previously been used to verify the EFL conjecture for small hypergraphs. We verify and extend these results to larger values and discuss challenges and directions. Ours is the first computational approach to the EFL conjecture that allows producing independently verifiable, DRAT proofs.
Cite as
Markus Kirchweger, Tomáš Peitl, and Stefan Szeider. A SAT Solver’s Opinion on the Erdős-Faber-Lovász Conjecture. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 13:1-13:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{kirchweger_et_al:LIPIcs.SAT.2023.13,
author = {Kirchweger, Markus and Peitl, Tom\'{a}\v{s} and Szeider, Stefan},
title = {{A SAT Solver’s Opinion on the Erd\H{o}s-Faber-Lov\'{a}sz Conjecture}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {13:1--13:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-286-0},
ISSN = {1868-8969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.13},
URN = {urn:nbn:de:0030-drops-184752},
doi = {10.4230/LIPIcs.SAT.2023.13},
annote = {Keywords: hypergraphs, graph coloring, SAT modulo symmetries}
}
Document
SAT-Based Generation of Planar Graphs
Abstract
To test a graph’s planarity in SAT-based graph generation we develop SAT encodings with dynamic symmetry breaking as facilitated in the SAT modulo Symmetry (SMS) framework. We implement and compare encodings based on three planarity criteria. In particular, we consider two eager encodings utilizing order-based and universal-set-based planarity criteria, and a lazy encoding based on Kuratowski’s theorem. The performance and scalability of these encodings are compared on two prominent problems from combinatorics: the computation of planar Turán numbers and the Earth-Moon problem. We further showcase the power of SMS equipped with a planarity encoding by verifying and extending several integer sequences from the Online Encyclopedia of Integer Sequences (OEIS) related to planar graph enumeration. Furthermore, we extend the SMS framework to directed graphs which might be of independent interest.
Cite as
Markus Kirchweger, Manfred Scheucher, and Stefan Szeider. SAT-Based Generation of Planar Graphs. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{kirchweger_et_al:LIPIcs.SAT.2023.14,
author = {Kirchweger, Markus and Scheucher, Manfred and Szeider, Stefan},
title = {{SAT-Based Generation of Planar Graphs}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {14:1--14:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-286-0},
ISSN = {1868-8969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.14},
URN = {urn:nbn:de:0030-drops-184767},
doi = {10.4230/LIPIcs.SAT.2023.14},
annote = {Keywords: SAT modulo Symmetry (SMS), dynamic symmetry breaking, planarity test, universal point set, order dimension, Schnyder’s theorem, Kuratowski’s theorem, Tur\'{a}n’s theorem, Earth-Moon problem}
}
Document
On CNF Conversion for Disjoint SAT Enumeration
Abstract
Modern SAT solvers are designed to handle problems expressed in Conjunctive Normal Form (CNF) so that non-CNF problems must be CNF-ized upfront, typically by using variants of either Tseitin or Plaisted and Greenbaum transformations. When passing from solving to enumeration, however, the capability of producing partial satisfying assignments that are as small as possible becomes crucial, which raises the question of whether such CNF encodings are also effective for enumeration.
In this paper, we investigate both theoretically and empirically the effectiveness of CNF conversions for disjoint SAT enumeration. On the negative side, we show that: (i) Tseitin transformation prevents the solver from producing short partial assignments, thus seriously affecting the effectiveness of enumeration; (ii) Plaisted and Greenbaum transformation overcomes this problem only in part. On the positive side, we show that combining Plaisted and Greenbaum transformation with NNF preprocessing upfront - which is typically not used in solving - can fully overcome the problem and can drastically reduce both the number of partial assignments and the execution time.
Cite as
Gabriele Masina, Giuseppe Spallitta, and Roberto Sebastiani. On CNF Conversion for Disjoint SAT Enumeration. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 15:1-15:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{masina_et_al:LIPIcs.SAT.2023.15,
author = {Masina, Gabriele and Spallitta, Giuseppe and Sebastiani, Roberto},
title = {{On CNF Conversion for Disjoint SAT Enumeration}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {15:1--15:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-286-0},
ISSN = {1868-8969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.15},
URN = {urn:nbn:de:0030-drops-184775},
doi = {10.4230/LIPIcs.SAT.2023.15},
annote = {Keywords: CNF conversion, AllSAT, AllSMT}
}
Document
Bounds on BDD-Based Bucket Elimination
Abstract
We study BDD-based bucket elimination, an approach to satisfiability testing using variable elimination which has seen several practical implementations in the past. We prove that it allows solving the standard pigeonhole principle formulas efficiently, when allowing different orders for variable elimination and BDD-representations, a variant of bucket elimination that was recently introduced. Furthermore, we show that this upper bound is somewhat brittle as for formulas which we get from the pigeonhole principle by restriction, i.e., fixing some of the variables, the same approach with the same variable orders has exponential runtime. We also show that the more common implementation of bucket elimination using the same order for variable elimination and the BDDs has exponential runtime for the pigeonhole principle when using either of the two orders from our upper bound, which suggests that the combination of both is the key to efficiency in the setting.
Cite as
Stefan Mengel. Bounds on BDD-Based Bucket Elimination. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 16:1-16:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{mengel:LIPIcs.SAT.2023.16,
author = {Mengel, Stefan},
title = {{Bounds on BDD-Based Bucket Elimination}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {16:1--16:11},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-286-0},
ISSN = {1868-8969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.16},
URN = {urn:nbn:de:0030-drops-184789},
doi = {10.4230/LIPIcs.SAT.2023.16},
annote = {Keywords: Bucket Elimination, Binary Decision Diagrams, Satisfiability, Complexity}
}
Document
Solving Huge Instances with Intel(R) SAT Solver
Abstract
We introduce a new release of our SAT solver Intelregistered SAT Solver. The new release, called IS23, is targeted to solve huge instances beyond the capacity of other solvers. IS23 can use 64-bit clause-indices and store clauses compressedly using bit-arrays, where each literal is normally allocated fewer than 32 bits. As a preliminary result, we show that only IS23 can handle a gigantic trivially satisfiable instance with over 8.5 billion clauses. Then, we demonstrate that IS23 enables a significant improvement in the capacity of our industrial tool for cell placement in physical design, since only IS23 can solve placement instances with up to 4.3 billion clauses. Finally, we show that IS23 is substantially more efficient than other solvers for finding many (10⁶) placements on instances with up to 170 million clauses. We use the latter application to demonstrate that variable succession, that is, the order in which the variables are provided to the solver, might have a significant impact on IS23’s performance, thereby providing a new dimension to SAT encoding considerations.
Cite as
Alexander Nadel. Solving Huge Instances with Intel(R) SAT Solver. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 17:1-17:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{nadel:LIPIcs.SAT.2023.17,
author = {Nadel, Alexander},
title = {{Solving Huge Instances with Intel(R) SAT Solver}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {17:1--17:12},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-286-0},
ISSN = {1868-8969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.17},
URN = {urn:nbn:de:0030-drops-184790},
doi = {10.4230/LIPIcs.SAT.2023.17},
annote = {Keywords: SAT, CDCL}
}
Document
Learning Shorter Redundant Clauses in SDCL Using MaxSAT
Abstract
In this paper we present the design and implementation of a Satisfaction-Driven Clause Learning (SDCL) SAT solver, MapleSDCL, which uses a MaxSAT-based technique that enables it to learn shorter, and hence better, redundant clauses. We also perform a thorough empirical evaluation of our method and show that our SDCL solver solves Mutilated Chess Board (MCB) problems significantly faster than CDCL solvers, without requiring any alteration to the branching heuristic used by the underlying CDCL SAT solver.
Cite as
Albert Oliveras, Chunxiao Li, Darryl Wu, Jonathan Chung, and Vijay Ganesh. Learning Shorter Redundant Clauses in SDCL Using MaxSAT. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{oliveras_et_al:LIPIcs.SAT.2023.18,
author = {Oliveras, Albert and Li, Chunxiao and Wu, Darryl and Chung, Jonathan and Ganesh, Vijay},
title = {{Learning Shorter Redundant Clauses in SDCL Using MaxSAT}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {18:1--18:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-286-0},
ISSN = {1868-8969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.18},
URN = {urn:nbn:de:0030-drops-184803},
doi = {10.4230/LIPIcs.SAT.2023.18},
annote = {Keywords: SAT, SDCL, MaxSAT}
}
Document
UpMax: User Partitioning for MaxSAT
Abstract
It has been shown that Maximum Satisfiability (MaxSAT) problem instances can be effectively solved by partitioning the set of soft clauses into several disjoint sets. The partitioning methods can be based on clause weights (e.g., stratification) or based on graph representations of the formula. Afterwards, a merge procedure is applied to guarantee that an optimal solution is found.
This paper proposes a new framework called UpMax that decouples the partitioning procedure from the MaxSAT solving algorithms. As a result, new partitioning procedures can be defined independently of the MaxSAT algorithm to be used. Moreover, this decoupling also allows users that build new MaxSAT formulas to propose partition schemes based on knowledge of the problem to be solved. We illustrate this approach using several problems and show that partitioning has a large impact on the performance of unsatisfiability-based MaxSAT algorithms.
Cite as
Pedro Orvalho, Vasco Manquinho, and Ruben Martins. UpMax: User Partitioning for MaxSAT. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 19:1-19:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{orvalho_et_al:LIPIcs.SAT.2023.19,
author = {Orvalho, Pedro and Manquinho, Vasco and Martins, Ruben},
title = {{UpMax: User Partitioning for MaxSAT}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {19:1--19:13},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-286-0},
ISSN = {1868-8969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.19},
URN = {urn:nbn:de:0030-drops-184819},
doi = {10.4230/LIPIcs.SAT.2023.19},
annote = {Keywords: Maximum Satisfiability, Formula partitioning, Graph-based methods}
}
Document
QMusExt: A Minimal (Un)satisfiable Core Extractor for Quantified Boolean Formulas
Abstract
In this paper, we present QMusExt, a tool for the extraction of minimal unsatisfiable sets (MUS) from quantified Boolean formulas (QBFs) in prenex conjunctive normal form (PCNF). Our tool generalizes an efficient algorithm for MUS extraction from propositional formulas that analyses and rewrites resolution proofs generated by SAT solvers.
In addition to extracting unsatisfiable cores from false formulas in PCNF, we apply QMusExt also to obtain satisfiable cores from Q-resolution proofs of true formulas in prenex disjunctive normal form (PDNF).
Cite as
Andreas Plank and Martina Seidl. QMusExt: A Minimal (Un)satisfiable Core Extractor for Quantified Boolean Formulas. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 20:1-20:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{plank_et_al:LIPIcs.SAT.2023.20,
author = {Plank, Andreas and Seidl, Martina},
title = {{QMusExt: A Minimal (Un)satisfiable Core Extractor for Quantified Boolean Formulas}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {20:1--20:10},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-286-0},
ISSN = {1868-8969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.20},
URN = {urn:nbn:de:0030-drops-184824},
doi = {10.4230/LIPIcs.SAT.2023.20},
annote = {Keywords: Minimal Unsatisfiable Core, Quantified Boolean Formula}
}
Document
Faster LRAT Checking Than Solving with CaDiCaL
Abstract
DRAT is the standard proof format used in the SAT Competition. It is easy to generate but checking proofs often takes even more time than solving the problem. An alternative is to use the LRAT proof system. While LRAT is easier and way more efficient to check, it is more complex to generate directly. Due to this complexity LRAT is not supported natively by any state-of-the-art SAT solver. Therefore Carneiro and Heule proposed the mixed proof format FRAT which still suffers from costly intermediate translation. We present an extension to the state-of-the-art solver CaDiCaL which is able to generate LRAT natively for all procedures implemented in CaDiCaL. We further present Lrat-Trim, a tool which not only trims and checks LRAT proofs in both ASCII and binary format but also produces clausal cores and has been tested thoroughly. Our experiments on recent competition benchmarks show that our approach reduces time of proof generation and certification substantially compared to competing approaches using intermediate DRAT or FRAT proofs.
Cite as
Florian Pollitt, Mathias Fleury, and Armin Biere. Faster LRAT Checking Than Solving with CaDiCaL. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 21:1-21:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{pollitt_et_al:LIPIcs.SAT.2023.21,
author = {Pollitt, Florian and Fleury, Mathias and Biere, Armin},
title = {{Faster LRAT Checking Than Solving with CaDiCaL}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {21:1--21:12},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-286-0},
ISSN = {1868-8969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.21},
URN = {urn:nbn:de:0030-drops-184837},
doi = {10.4230/LIPIcs.SAT.2023.21},
annote = {Keywords: SAT solving, Proof Checking, DRAT, LRAT, FRAT}
}
Document
Even Shorter Proofs Without New Variables
Abstract
Proof formats for SAT solvers have diversified over the last decade, enabling new features such as extended resolution-like capabilities, very general extension-free rules, inclusion of proof hints, and pseudo-boolean reasoning. Interference-based methods have been proven effective, and some theoretical work has been undertaken to better explain their limits and semantics. In this work, we combine the subsumption redundancy notion from [Sam Buss and Neil Thapen, 2019] and the overwrite logic framework from [Adrián Rebola{-}Pardo and Martin Suda, 2018]. Natural generalizations then become apparent, enabling even shorter proofs of the pigeonhole principle (compared to those from [Marijn J. H. Heule et al., 2017]) and smaller unsatisfiable core generation.
Cite as
Adrián Rebola-Pardo. Even Shorter Proofs Without New Variables. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 22:1-22:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{rebolapardo:LIPIcs.SAT.2023.22,
author = {Rebola-Pardo, Adri\'{a}n},
title = {{Even Shorter Proofs Without New Variables}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {22:1--22:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-286-0},
ISSN = {1868-8969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.22},
URN = {urn:nbn:de:0030-drops-184844},
doi = {10.4230/LIPIcs.SAT.2023.22},
annote = {Keywords: Interference, SAT solving, Unsatisfiability proofs, Unsatisfiable cores}
}
Document
Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving
Abstract
This paper presents a novel application of QBF solving to automata reduction. We focus on Transition-based Emerson-Lei automata (TELA), which is a popular formalism that generalizes many traditional kinds of automata over infinite words including Büchi, co-Büchi, Rabin, Streett, and parity automata. Transitions in a TELA are labelled with acceptance marks and its accepting formula is a positive Boolean combination of atoms saying that a particular mark has to be visited infinitely or finitely often. Algorithms processing these automata are often very sensitive to the number of acceptance marks. We introduce a new technique for reducing the number of acceptance marks in TELA based on satisfiability of quantified Boolean formulas (QBF). We evaluated our reduction technique on TELA produced by state-of-the-art tools of the libraries Owl and Spot and by the tool ltl3tela. The technique reduced some acceptance marks in automata produced by all the tools. On automata with more than one acceptance mark obtained by translation of LTL formulas from literature with tools Delag and Rabinizer 4, our technique reduced 27.7% and 39.3% of acceptance marks, respectively. The reduction was even higher on automata from random formulas.
Cite as
Tereza Schwarzová, Jan Strejček, and Juraj Major. Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 23:1-23:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{schwarzova_et_al:LIPIcs.SAT.2023.23,
author = {Schwarzov\'{a}, Tereza and Strej\v{c}ek, Jan and Major, Juraj},
title = {{Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {23:1--23:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-286-0},
ISSN = {1868-8969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.23},
URN = {urn:nbn:de:0030-drops-184859},
doi = {10.4230/LIPIcs.SAT.2023.23},
annote = {Keywords: Emerson-Lei automata, TELA, automata reduction, QBF, telatko}
}
Document
Validation of QBF Encodings with Winning Strategies
Abstract
When using a QBF solver for solving application problems encoded to quantified Boolean formulas (QBFs), mainly two things can potentially go wrong: (1) the solver could be buggy and return a wrong result or (2) the encoding could be incorrect. To ensure the correctness of solvers, sophisticated fuzzing and testing techniques have been presented. To ultimately trust a solving result, solvers have to provide a proof certificate that can be independently checked. Much less attention, however, has been paid to the question how to ensure the correctness of encodings.
The validation of QBF encodings is particularly challenging because of the variable dependencies introduced by the quantifiers. In contrast to SAT, the solution of a true QBF is not simply a variable assignment, but a winning strategy. For each existential variable x, a winning strategy provides a function that defines how to set x based on the values of the universal variables that precede x in the quantifier prefix. Winning strategies for false formulas are defined dually.
In this paper, we provide a tool for validating encodings using winning strategies and interactive game play with a QBF solver. As the representation of winning strategies can get huge, we also introduce validation based on partial winning strategies. Finally, we employ winning strategies for testing if two different encodings of one problem have the same solutions.
Cite as
Irfansha Shaik, Maximilian Heisinger, Martina Seidl, and Jaco van de Pol. Validation of QBF Encodings with Winning Strategies. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 24:1-24:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{shaik_et_al:LIPIcs.SAT.2023.24,
author = {Shaik, Irfansha and Heisinger, Maximilian and Seidl, Martina and van de Pol, Jaco},
title = {{Validation of QBF Encodings with Winning Strategies}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {24:1--24:10},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-286-0},
ISSN = {1868-8969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.24},
URN = {urn:nbn:de:0030-drops-184863},
doi = {10.4230/LIPIcs.SAT.2023.24},
annote = {Keywords: QBF, Validation, Winning Strategy, Equivalence, Certificates}
}
Document
Combining Cubic Dynamical Solvers with Make/Break Heuristics to Solve SAT
Abstract
Dynamical solvers for combinatorial optimization are usually based on 2superscript{nd} degree polynomial interactions, such as the Ising model. These exhibit high success for problems that map naturally to their formulation. However, SAT requires higher degree of interactions. As such, these quadratic dynamical solvers (QDS) have shown poor solution quality due to excessive auxiliary variables and the resulting increase in search-space complexity. Thus recently, a series of cubic dynamical solver (CDS) models have been proposed for SAT and other problems. We show that such problem-agnostic CDS models still perform poorly on moderate to large problems, thus motivating the need to utilize SAT-specific heuristics. With this insight, our contributions can be summarized into three points. First, we demonstrate that existing make-only heuristics perform poorly on scale-free, industrial-like problems when integrated into CDS. This motivates us to utilize break counts as well. Second, we derive a relationship between make/break and the CDS formulation to efficiently recover break counts. Finally, we utilize this relationship to propose a new make/break heuristic and combine it with a state-of-the-art CDS which is projected to solve SAT problems several orders of magnitude faster than existing software solvers.
Cite as
Anshujit Sharma, Matthew Burns, and Michael C. Huang. Combining Cubic Dynamical Solvers with Make/Break Heuristics to Solve SAT. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 25:1-25:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{sharma_et_al:LIPIcs.SAT.2023.25,
author = {Sharma, Anshujit and Burns, Matthew and Huang, Michael C.},
title = {{Combining Cubic Dynamical Solvers with Make/Break Heuristics to Solve SAT}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {25:1--25:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-286-0},
ISSN = {1868-8969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.25},
URN = {urn:nbn:de:0030-drops-184871},
doi = {10.4230/LIPIcs.SAT.2023.25},
annote = {Keywords: Satisfiability, Ising machines, Stochastic Heuristics, Natural Computation}
}
Document
Cutting Planes Width and the Complexity of Graph Isomorphism Refutations
Abstract
The width complexity measure plays a central role in Resolution and other propositional proof systems like Polynomial Calculus (under the name of degree). The study of width lower bounds is the most extended method for proving size lower bounds, and it is known that for these systems, proofs with small width also imply the existence of proofs with small size. Not much has been studied, however, about the width parameter in the Cutting Planes (CP) proof system, a measure that was introduced by Dantchev and Martin in 2011 under the name of CP cutwidth.
In this paper, we study the width complexity of CP refutations of graph isomorphism formulas. For a pair of non-isomorphic graphs G and H, we show a direct connection between the Weisfeiler-Leman differentiation number WL(G, H) of the graphs and the width of a CP refutation for the corresponding isomorphism formula Iso(G, H). In particular, we show that if WL(G, H) ≤ k, then there is a CP refutation of Iso(G, H) with width k, and if WL(G, H) > k, then there are no CP refutations of Iso(G, H) with width k-2. Similar results are known for other proof systems, like Resolution, Sherali-Adams, or Polynomial Calculus. We also obtain polynomial-size CP refutations from our width bound for isomorphism formulas for graphs with constant WL-dimension.
Cite as
Jacobo Torán and Florian Wörz. Cutting Planes Width and the Complexity of Graph Isomorphism Refutations. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 26:1-26:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{toran_et_al:LIPIcs.SAT.2023.26,
author = {Tor\'{a}n, Jacobo and W\"{o}rz, Florian},
title = {{Cutting Planes Width and the Complexity of Graph Isomorphism Refutations}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {26:1--26:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-286-0},
ISSN = {1868-8969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.26},
URN = {urn:nbn:de:0030-drops-184884},
doi = {10.4230/LIPIcs.SAT.2023.26},
annote = {Keywords: Cutting Planes, Proof Complexity, Linear Programming, Combinatorial Optimization, Weisfeiler-Leman Algorithm, Graph Isomorphism}
}
Document
Limits of CDCL Learning via Merge Resolution
Abstract
In their seminal work, Atserias et al. and independently Pipatsrisawat and Darwiche in 2009 showed that CDCL solvers can simulate resolution proofs with polynomial overhead. However, previous work does not address the tightness of the simulation, i.e., the question of how large this overhead needs to be. In this paper, we address this question by focusing on an important property of proofs generated by CDCL solvers that employ standard learning schemes, namely that the derivation of a learned clause has at least one inference where a literal appears in both premises (aka, a merge literal). Specifically, we show that proofs of this kind can simulate resolution proofs with at most a linear overhead, but there also exist formulas where such overhead is necessary or, more precisely, that there exist formulas with resolution proofs of linear length that require quadratic CDCL proofs.
Cite as
Marc Vinyals, Chunxiao Li, Noah Fleming, Antonina Kolokolova, and Vijay Ganesh. Limits of CDCL Learning via Merge Resolution. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 27:1-27:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{vinyals_et_al:LIPIcs.SAT.2023.27,
author = {Vinyals, Marc and Li, Chunxiao and Fleming, Noah and Kolokolova, Antonina and Ganesh, Vijay},
title = {{Limits of CDCL Learning via Merge Resolution}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {27:1--27:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-286-0},
ISSN = {1868-8969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.27},
URN = {urn:nbn:de:0030-drops-184894},
doi = {10.4230/LIPIcs.SAT.2023.27},
annote = {Keywords: proof complexity, resolution, merge resolution, CDCL, learning scheme}
}
Document
Explaining SAT Solving Using Causal Reasoning
Abstract
The past three decades have witnessed notable success in designing efficient SAT solvers, with modern solvers capable of solving industrial benchmarks containing millions of variables in just a few seconds. The success of modern SAT solvers owes to the widely-used CDCL algorithm, which lacks comprehensive theoretical investigation. Furthermore, it has been observed that CDCL solvers still struggle to deal with specific classes of benchmarks comprising only hundreds of variables, which contrasts with their widespread use in real-world applications. Consequently, there is an urgent need to uncover the inner workings of these seemingly weak yet powerful black boxes.
In this paper, we present a first step towards this goal by introducing an approach called {CausalSAT}, which employs causal reasoning to gain insights into the functioning of modern SAT solvers. {CausalSAT} initially generates observational data from the execution of SAT solvers and learns a structured graph representing the causal relationships between the components of a SAT solver. Subsequently, given a query such as whether a clause with low literals blocks distance (LBD) has a higher clause utility, {CausalSAT} calculates the causal effect of LBD on clause utility and provides an answer to the question. We use {CausalSAT} to quantitatively verify hypotheses previously regarded as "rules of thumb" or empirical findings, such as the query above or the notion that clauses with high LBD experience a rapid drop in utility over time. Moreover, {CausalSAT} can address previously unexplored questions, like which branching heuristic leads to greater clause utility in order to study the relationship between branching and clause management. Experimental evaluations using practical benchmarks demonstrate that {CausalSAT} effectively fits the data, verifies four "rules of thumb", and provides answers to three questions closely related to implementing modern solvers.
Cite as
Jiong Yang, Arijit Shaw, Teodora Baluta, Mate Soos, and Kuldeep S. Meel. Explaining SAT Solving Using Causal Reasoning. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 28:1-28:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{yang_et_al:LIPIcs.SAT.2023.28,
author = {Yang, Jiong and Shaw, Arijit and Baluta, Teodora and Soos, Mate and Meel, Kuldeep S.},
title = {{Explaining SAT Solving Using Causal Reasoning}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {28:1--28:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-286-0},
ISSN = {1868-8969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.28},
URN = {urn:nbn:de:0030-drops-184909},
doi = {10.4230/LIPIcs.SAT.2023.28},
annote = {Keywords: Satisfiability, Causality, SAT solver, Clause management}
}
Document
LS-DTKMS: A Local Search Algorithm for Diversified Top-k MaxSAT Problem
Abstract
The Maximum Satisfiability (MaxSAT), an important optimization problem, has a range of applications, including network routing, planning and scheduling, and combinatorial auctions. Among these applications, one usually benefits from having not just one single solution, but k diverse solutions. Motivated by this, we study an extension of MaxSAT, named Diversified Top-k MaxSAT (DTKMS) problem, which is to find k feasible assignments of a given formula such that each assignment satisfies all hard clauses and all of them together satisfy the maximum number of soft clauses. This paper presents a local search algorithm, LS-DTKMS, for DTKMS problem, which exploits novel scoring functions to select variables and assignments. Experiments demonstrate that LS-DTKMS outperforms the top-k MaxSAT based DTKMS solvers and state-of-the-art solvers for diversified top-k clique problem.
Cite as
Junping Zhou, Jiaxin Liang, Minghao Yin, and Bo He. LS-DTKMS: A Local Search Algorithm for Diversified Top-k MaxSAT Problem. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 29:1-29:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{zhou_et_al:LIPIcs.SAT.2023.29,
author = {Zhou, Junping and Liang, Jiaxin and Yin, Minghao and He, Bo},
title = {{LS-DTKMS: A Local Search Algorithm for Diversified Top-k MaxSAT Problem}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {29:1--29:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-286-0},
ISSN = {1868-8969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.29},
URN = {urn:nbn:de:0030-drops-184912},
doi = {10.4230/LIPIcs.SAT.2023.29},
annote = {Keywords: Top-k, MaxSAT, local search}
}
Document
A Comparison of SAT Encodings for Acyclicity of Directed Graphs
Abstract
Many practical applications require synthesizing directed graphs that satisfy the acyclic constraint along with some side constraints. Several methods have been devised for encoding acyclicity of directed graphs into SAT, each of which is based on a cycle-detecting algorithm. The leaf-elimination encoding (LEE) repeatedly eliminates leaves from the graph, and judges the graph to be acyclic if the graph becomes empty at a certain time. The vertex-elimination encoding (VEE) exploits the property that the cyclicity of the resulting graph produced by the vertex-elimination operation entails the cyclicity of the original graph. While VEE is significantly smaller than the transitive-closure encoding for sparse graphs, it generates prohibitively large encodings for large dense graphs. This paper reports on a comparison study of four SAT encodings for acyclicity of directed graphs, namely, LEE using unary encoding for time variables (LEE-u), LEE using binary encoding for time variables (LEE-b), VEE, and a hybrid encoding which combines LEE-b and VEE. The results show that the hybrid encoding significantly outperforms the others.
Cite as
Neng-Fa Zhou, Ruiwei Wang, and Roland H. C. Yap. A Comparison of SAT Encodings for Acyclicity of Directed Graphs. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 30:1-30:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{zhou_et_al:LIPIcs.SAT.2023.30,
author = {Zhou, Neng-Fa and Wang, Ruiwei and Yap, Roland H. C.},
title = {{A Comparison of SAT Encodings for Acyclicity of Directed Graphs}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {30:1--30:9},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-286-0},
ISSN = {1868-8969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.30},
URN = {urn:nbn:de:0030-drops-184927},
doi = {10.4230/LIPIcs.SAT.2023.30},
annote = {Keywords: Graph constraints, Acyclic constraint, SAT encoding, Graph Synthesis}
}