LIPIcs, Volume 271
SAT 2023, July 4-8, 2023, Alghero, Italy
Editors: Meena Mahajan and Friedrich Slivovsky
Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)
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)
@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-dev.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} }
Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)
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)
@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-dev.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} }
Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)
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)
@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-dev.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} }
Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)
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)
@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-dev.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} }
Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)
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)
@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-dev.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} }
Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)
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)
@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-dev.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} }
Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)
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)
@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-dev.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} }
Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)
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)
@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-dev.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} }
Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)
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)
@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-dev.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} }
Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)
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)
@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} }
Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)
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)
@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-dev.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} }
Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)
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)
@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-dev.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} }
Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)
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)
@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-dev.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} }
Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)
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)
@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-dev.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} }
Feedback for Dagstuhl Publishing