LIPIcs, Volume 236
SAT 2022, August 2-5, 2022, Haifa, Israel
Editors: Kuldeep S. Meel and Ofer Strichman
Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)
25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 1-618, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@Proceedings{meel_et_al:LIPIcs.SAT.2022, title = {{LIPIcs, Volume 236, SAT 2022, Complete Volume}}, booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)}, pages = {1--618}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-242-6}, ISSN = {1868-8969}, year = {2022}, volume = {236}, editor = {Meel, Kuldeep S. and Strichman, Ofer}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022}, URN = {urn:nbn:de:0030-drops-166736}, doi = {10.4230/LIPIcs.SAT.2022}, annote = {Keywords: LIPIcs, Volume 236, SAT 2022, Complete Volume} }
Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)
25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 0:i-0:xviii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{meel_et_al:LIPIcs.SAT.2022.0, author = {Meel, Kuldeep S. and Strichman, Ofer}, title = {{Front Matter, Table of Contents, Preface, Conference Organization}}, booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)}, pages = {0:i--0:xviii}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-242-6}, ISSN = {1868-8969}, year = {2022}, volume = {236}, editor = {Meel, Kuldeep S. and Strichman, Ofer}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.0}, URN = {urn:nbn:de:0030-drops-166746}, doi = {10.4230/LIPIcs.SAT.2022.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization} }
Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)
Markus Anders. SAT Preprocessors and Symmetry. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 1:1-1:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{anders:LIPIcs.SAT.2022.1, author = {Anders, Markus}, title = {{SAT Preprocessors and Symmetry}}, booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)}, pages = {1:1--1:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-242-6}, ISSN = {1868-8969}, year = {2022}, volume = {236}, editor = {Meel, Kuldeep S. and Strichman, Ofer}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.1}, URN = {urn:nbn:de:0030-drops-166752}, doi = {10.4230/LIPIcs.SAT.2022.1}, annote = {Keywords: boolean satisfiability, symmetry exploitation, graph isomorphism} }
Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)
Jakob Bach, Markus Iser, and Klemens Böhm. A Comprehensive Study of k-Portfolios of Recent SAT Solvers. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 2:1-2:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{bach_et_al:LIPIcs.SAT.2022.2, author = {Bach, Jakob and Iser, Markus and B\"{o}hm, Klemens}, title = {{A Comprehensive Study of k-Portfolios of Recent SAT Solvers}}, booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)}, pages = {2:1--2:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-242-6}, ISSN = {1868-8969}, year = {2022}, volume = {236}, editor = {Meel, Kuldeep S. and Strichman, Ofer}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.2}, URN = {urn:nbn:de:0030-drops-166767}, doi = {10.4230/LIPIcs.SAT.2022.2}, annote = {Keywords: Propositional satisfiability, solver portfolios, runtime prediction, machine learning, integer programming} }
Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)
Iván Garzón, Pablo Mesejo, and Jesús Giráldez-Cru. On the Performance of Deep Generative Models of Realistic SAT Instances. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 3:1-3:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{garzon_et_al:LIPIcs.SAT.2022.3, author = {Garz\'{o}n, Iv\'{a}n and Mesejo, Pablo and Gir\'{a}ldez-Cru, Jes\'{u}s}, title = {{On the Performance of Deep Generative Models of Realistic SAT Instances}}, booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)}, pages = {3:1--3:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-242-6}, ISSN = {1868-8969}, year = {2022}, volume = {236}, editor = {Meel, Kuldeep S. and Strichman, Ofer}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.3}, URN = {urn:nbn:de:0030-drops-166775}, doi = {10.4230/LIPIcs.SAT.2022.3}, annote = {Keywords: Realistic SAT generators, pseudo-industrial random SAT, deep generative models, deep learning} }
Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)
Markus Kirchweger, Manfred Scheucher, and Stefan Szeider. A SAT Attack on Rota’s Basis Conjecture. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 4:1-4:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{kirchweger_et_al:LIPIcs.SAT.2022.4, author = {Kirchweger, Markus and Scheucher, Manfred and Szeider, Stefan}, title = {{A SAT Attack on Rota’s Basis Conjecture}}, booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)}, pages = {4:1--4:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-242-6}, ISSN = {1868-8969}, year = {2022}, volume = {236}, editor = {Meel, Kuldeep S. and Strichman, Ofer}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.4}, URN = {urn:nbn:de:0030-drops-166780}, doi = {10.4230/LIPIcs.SAT.2022.4}, annote = {Keywords: SAT modulo Symmetry (SMS), dynamic symmetry breaking, Rota’s basis conjecture, matroid} }
Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)
Agnes Schleitzer and Olaf Beyersdorff. Classes of Hard Formulas for QBF Resolution. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 5:1-5:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{schleitzer_et_al:LIPIcs.SAT.2022.5, author = {Schleitzer, Agnes and Beyersdorff, Olaf}, title = {{Classes of Hard Formulas for QBF Resolution}}, booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)}, pages = {5:1--5:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-242-6}, ISSN = {1868-8969}, year = {2022}, volume = {236}, editor = {Meel, Kuldeep S. and Strichman, Ofer}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.5}, URN = {urn:nbn:de:0030-drops-166792}, doi = {10.4230/LIPIcs.SAT.2022.5}, annote = {Keywords: QBF, proof complexity, resolution, separations} }
Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)
Dmitry Itsykson, Artur Riazanov, and Petr Smirnov. Tight Bounds for Tseitin Formulas. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 6:1-6:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{itsykson_et_al:LIPIcs.SAT.2022.6, author = {Itsykson, Dmitry and Riazanov, Artur and Smirnov, Petr}, title = {{Tight Bounds for Tseitin Formulas}}, booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)}, pages = {6:1--6:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-242-6}, ISSN = {1868-8969}, year = {2022}, volume = {236}, editor = {Meel, Kuldeep S. and Strichman, Ofer}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.6}, URN = {urn:nbn:de:0030-drops-166805}, doi = {10.4230/LIPIcs.SAT.2022.6}, annote = {Keywords: Proof complexity, Tseitin formulas, treewidth, resolution, OBDD-based proof systems} }
Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)
Mikoláš Janota, Jelle Piepenbrock, and Bartosz Piotrowski. Towards Learning Quantifier Instantiation in SMT. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{janota_et_al:LIPIcs.SAT.2022.7, author = {Janota, Mikol\'{a}\v{s} and Piepenbrock, Jelle and Piotrowski, Bartosz}, title = {{Towards Learning Quantifier Instantiation in SMT}}, booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)}, pages = {7:1--7:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-242-6}, ISSN = {1868-8969}, year = {2022}, volume = {236}, editor = {Meel, Kuldeep S. and Strichman, Ofer}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.7}, URN = {urn:nbn:de:0030-drops-166810}, doi = {10.4230/LIPIcs.SAT.2022.7}, annote = {Keywords: satisfiability modulo theories, quantifier instantiation, machine learning} }
Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)
Alexander Nadel. Introducing Intel(R) SAT Solver. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 8:1-8:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{nadel:LIPIcs.SAT.2022.8, author = {Nadel, Alexander}, title = {{Introducing Intel(R) SAT Solver}}, booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)}, pages = {8:1--8:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-242-6}, ISSN = {1868-8969}, year = {2022}, volume = {236}, editor = {Meel, Kuldeep S. and Strichman, Ofer}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.8}, URN = {urn:nbn:de:0030-drops-166825}, doi = {10.4230/LIPIcs.SAT.2022.8}, annote = {Keywords: SAT, CDCL, MaxSAT} }
Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)
Milan Mossé, Harry Sha, and Li-Yang Tan. A Generalization of the Satisfiability Coding Lemma and Its Applications. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{mosse_et_al:LIPIcs.SAT.2022.9, author = {Moss\'{e}, Milan and Sha, Harry and Tan, Li-Yang}, title = {{A Generalization of the Satisfiability Coding Lemma and Its Applications}}, booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)}, pages = {9:1--9:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-242-6}, ISSN = {1868-8969}, year = {2022}, volume = {236}, editor = {Meel, Kuldeep S. and Strichman, Ofer}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.9}, URN = {urn:nbn:de:0030-drops-166837}, doi = {10.4230/LIPIcs.SAT.2022.9}, annote = {Keywords: Prime Implicants, Satisfiability Coding Lemma, Blake Canonical Form, k-SAT} }
Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)
Leroy Chew and Marijn J. H. Heule. Relating Existing Powerful Proof Systems for QBF. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 10:1-10:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{chew_et_al:LIPIcs.SAT.2022.10, author = {Chew, Leroy and Heule, Marijn J. H.}, title = {{Relating Existing Powerful Proof Systems for QBF}}, booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)}, pages = {10:1--10:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-242-6}, ISSN = {1868-8969}, year = {2022}, volume = {236}, editor = {Meel, Kuldeep S. and Strichman, Ofer}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.10}, URN = {urn:nbn:de:0030-drops-166845}, doi = {10.4230/LIPIcs.SAT.2022.10}, annote = {Keywords: QBF, Proof Complexity, Verification, Strategy Extraction, Sequent Calculus} }
Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)
Benjamin Böhm, Tomáš Peitl, and Olaf Beyersdorff. Should Decisions in QCDCL Follow Prefix Order?. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{bohm_et_al:LIPIcs.SAT.2022.11, author = {B\"{o}hm, Benjamin and Peitl, Tom\'{a}\v{s} and Beyersdorff, Olaf}, title = {{Should Decisions in QCDCL Follow Prefix Order?}}, booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)}, pages = {11:1--11:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-242-6}, ISSN = {1868-8969}, year = {2022}, volume = {236}, editor = {Meel, Kuldeep S. and Strichman, Ofer}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.11}, URN = {urn:nbn:de:0030-drops-166850}, doi = {10.4230/LIPIcs.SAT.2022.11}, annote = {Keywords: QBF, CDCL, proof complexity, lower bounds} }
Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)
Christoph Jabs, Jeremias Berg, Andreas Niskanen, and Matti Järvisalo. MaxSAT-Based Bi-Objective Boolean Optimization. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 12:1-12:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{jabs_et_al:LIPIcs.SAT.2022.12, author = {Jabs, Christoph and Berg, Jeremias and Niskanen, Andreas and J\"{a}rvisalo, Matti}, title = {{MaxSAT-Based Bi-Objective Boolean Optimization}}, booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)}, pages = {12:1--12:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-242-6}, ISSN = {1868-8969}, year = {2022}, volume = {236}, editor = {Meel, Kuldeep S. and Strichman, Ofer}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.12}, URN = {urn:nbn:de:0030-drops-166863}, doi = {10.4230/LIPIcs.SAT.2022.12}, annote = {Keywords: Multi-objective optimization, Pareto front enumeration, bi-objective optimization, maximum satisfiability, incremental SAT} }
Feedback for Dagstuhl Publishing