LIPIcs, Volume 236
SAT 2022, August 2-5, 2022, Haifa, Israel
Editors: Kuldeep S. Meel and Ofer Strichman
Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)
Diptarka Chakraborty, Gunjan Kumar, and Kuldeep S. Meel. Support Size Estimation: The Power of Conditioning. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 33:1-33:13, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)
@InProceedings{chakraborty_et_al:LIPIcs.MFCS.2023.33, author = {Chakraborty, Diptarka and Kumar, Gunjan and Meel, Kuldeep S.}, title = {{Support Size Estimation: The Power of Conditioning}}, booktitle = {48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)}, pages = {33:1--33:13}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-292-1}, ISSN = {1868-8969}, year = {2023}, volume = {272}, editor = {Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.33}, URN = {urn:nbn:de:0030-drops-185675}, doi = {10.4230/LIPIcs.MFCS.2023.33}, annote = {Keywords: Support-size estimation, Distribution testing, Conditional sampling, Lower bound} }
Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)
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)
@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} }
Published in: LIPIcs, Volume 265, 21st International Symposium on Experimental Algorithms (SEA 2023)
Markus Anders, Pascal Schweitzer, and Julian Stieß. Engineering a Preprocessor for Symmetry Detection. In 21st International Symposium on Experimental Algorithms (SEA 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 265, pp. 1:1-1:21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)
@InProceedings{anders_et_al:LIPIcs.SEA.2023.1, author = {Anders, Markus and Schweitzer, Pascal and Stie{\ss}, Julian}, title = {{Engineering a Preprocessor for Symmetry Detection}}, booktitle = {21st International Symposium on Experimental Algorithms (SEA 2023)}, pages = {1:1--1:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-279-2}, ISSN = {1868-8969}, year = {2023}, volume = {265}, editor = {Georgiadis, Loukas}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SEA.2023.1}, URN = {urn:nbn:de:0030-drops-183511}, doi = {10.4230/LIPIcs.SEA.2023.1}, annote = {Keywords: graph isomorphism, automorphism groups, symmetry detection, preprocessors} }
Published in: LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)
Diptarka Chakraborty, Sourav Chakraborty, Gunjan Kumar, and Kuldeep S. Meel. Approximate Model Counting: Is SAT Oracle More Powerful Than NP Oracle?. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 123:1-123:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)
@InProceedings{chakraborty_et_al:LIPIcs.ICALP.2023.123, author = {Chakraborty, Diptarka and Chakraborty, Sourav and Kumar, Gunjan and Meel, Kuldeep S.}, title = {{Approximate Model Counting: Is SAT Oracle More Powerful Than NP Oracle?}}, booktitle = {50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)}, pages = {123:1--123:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-278-5}, ISSN = {1868-8969}, year = {2023}, volume = {261}, editor = {Etessami, Kousha and Feige, Uriel and Puppis, Gabriele}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.123}, URN = {urn:nbn:de:0030-drops-181750}, doi = {10.4230/LIPIcs.ICALP.2023.123}, annote = {Keywords: Model counting, Approximation, Satisfiability, NP oracle, SAT oracle} }
Published in: LIPIcs, Volume 244, 30th Annual European Symposium on Algorithms (ESA 2022)
Sourav Chakraborty, N. V. Vinodchandran¹, and Kuldeep S. Meel. Distinct Elements in Streams: An Algorithm for the (Text) Book. In 30th Annual European Symposium on Algorithms (ESA 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 244, pp. 34:1-34:6, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
@InProceedings{chakraborty_et_al:LIPIcs.ESA.2022.34, author = {Chakraborty, Sourav and Vinodchandran¹, N. V. and Meel, Kuldeep S.}, title = {{Distinct Elements in Streams: An Algorithm for the (Text) Book}}, booktitle = {30th Annual European Symposium on Algorithms (ESA 2022)}, pages = {34:1--34:6}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-247-1}, ISSN = {1868-8969}, year = {2022}, volume = {244}, editor = {Chechik, Shiri and Navarro, Gonzalo and Rotenberg, Eva and Herman, Grzegorz}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2022.34}, URN = {urn:nbn:de:0030-drops-169725}, doi = {10.4230/LIPIcs.ESA.2022.34}, annote = {Keywords: F₀ Estimation, Streaming, Sampling} }
Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)
Kuldeep S. Meel and Ofer Strichman. LIPIcs, Volume 236, SAT 2022, Complete Volume. In 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.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)
Kuldeep S. Meel and Ofer Strichman. Front Matter, Table of Contents, Preface, Conference Organization. In 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.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.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.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.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.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.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.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.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} }
Feedback for Dagstuhl Publishing