LIPIcs, Volume 305
SAT 2024, August 21-24, 2024, Pune, India
Editors: Supratik Chakraborty and Jie-Hong Roland Jiang
LIPIcs, Volume 13
FSTTCS 2011, December 12-14, 2011, Mumbai, India
Editors: Supratik Chakraborty and Amit Kumar
Published in: LIPIcs, Volume 307, 30th International Conference on Principles and Practice of Constraint Programming (CP 2024)
Alexandre Dubray, Pierre Schaus, and Siegfried Nijssen. Anytime Weighted Model Counting with Approximation Guarantees for Probabilistic Inference. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 10:1-10:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{dubray_et_al:LIPIcs.CP.2024.10, author = {Dubray, Alexandre and Schaus, Pierre and Nijssen, Siegfried}, title = {{Anytime Weighted Model Counting with Approximation Guarantees for Probabilistic Inference}}, booktitle = {30th International Conference on Principles and Practice of Constraint Programming (CP 2024)}, pages = {10:1--10:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-336-2}, ISSN = {1868-8969}, year = {2024}, volume = {307}, editor = {Shaw, Paul}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2024.10}, URN = {urn:nbn:de:0030-drops-206956}, doi = {10.4230/LIPIcs.CP.2024.10}, annote = {Keywords: Projected Weighted Model Counting, Limited Discrepancy Search, Approximate Method, Probabilistic Inference} }
Published in: LIPIcs, Volume 307, 30th International Conference on Principles and Practice of Constraint Programming (CP 2024)
Cunjing Ge and Armin Biere. Improved Bounds of Integer Solution Counts via Volume and Extending to Mixed-Integer Linear Constraints. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 13:1-13:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{ge_et_al:LIPIcs.CP.2024.13, author = {Ge, Cunjing and Biere, Armin}, title = {{Improved Bounds of Integer Solution Counts via Volume and Extending to Mixed-Integer Linear Constraints}}, booktitle = {30th International Conference on Principles and Practice of Constraint Programming (CP 2024)}, pages = {13:1--13:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-336-2}, ISSN = {1868-8969}, year = {2024}, volume = {307}, editor = {Shaw, Paul}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2024.13}, URN = {urn:nbn:de:0030-drops-206983}, doi = {10.4230/LIPIcs.CP.2024.13}, annote = {Keywords: Integer Solution Counting, Mixed-Integer Linear Constraints, #SMT(LA) Problems, Volume of Polytopes} }
Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)
27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 1-578, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@Proceedings{chakraborty_et_al:LIPIcs.SAT.2024, title = {{LIPIcs, Volume 305, SAT 2024, Complete Volume}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {1--578}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-334-8}, ISSN = {1868-8969}, year = {2024}, volume = {305}, editor = {Chakraborty, Supratik and Jiang, Jie-Hong Roland}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024}, URN = {urn:nbn:de:0030-drops-205211}, doi = {10.4230/LIPIcs.SAT.2024}, annote = {Keywords: LIPIcs, Volume 305, SAT 2024, Complete Volume} }
Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)
27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 0:i-0:xviii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{chakraborty_et_al:LIPIcs.SAT.2024.0, author = {Chakraborty, Supratik and Jiang, Jie-Hong Roland}, title = {{Front Matter, Table of Contents, Preface, Conference Organization}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {0:i--0:xviii}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-334-8}, ISSN = {1868-8969}, year = {2024}, volume = {305}, editor = {Chakraborty, Supratik and Jiang, Jie-Hong Roland}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.0}, URN = {urn:nbn:de:0030-drops-205222}, doi = {10.4230/LIPIcs.SAT.2024.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization} }
Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)
Martina Seidl. Models and Counter-Models of Quantified Boolean Formulas (Invited Talk). In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 1:1-1:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{seidl:LIPIcs.SAT.2024.1, author = {Seidl, Martina}, title = {{Models and Counter-Models of Quantified Boolean Formulas}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {1:1--1:7}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-334-8}, ISSN = {1868-8969}, year = {2024}, volume = {305}, editor = {Chakraborty, Supratik and Jiang, Jie-Hong Roland}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.1}, URN = {urn:nbn:de:0030-drops-205238}, doi = {10.4230/LIPIcs.SAT.2024.1}, annote = {Keywords: Quantified Boolean Formula, Solution Extraction, Solution Counting} }
Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)
Cesare Tinelli. Scalable Proof Production and Checking in SMT (Invited Talk). In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 2:1-2:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{tinelli:LIPIcs.SAT.2024.2, author = {Tinelli, Cesare}, title = {{Scalable Proof Production and Checking in SMT}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {2:1--2:2}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-334-8}, ISSN = {1868-8969}, year = {2024}, volume = {305}, editor = {Chakraborty, Supratik and Jiang, Jie-Hong Roland}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.2}, URN = {urn:nbn:de:0030-drops-205241}, doi = {10.4230/LIPIcs.SAT.2024.2}, annote = {Keywords: Satisfiability Modulo Theories, Proof generation and certification} }
Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)
Moshe Y. Vardi. Logical Algorithmics: From Relational Queries to Boolean Reasoning (Invited Talk). In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, p. 3:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{vardi:LIPIcs.SAT.2024.3, author = {Vardi, Moshe Y.}, title = {{Logical Algorithmics: From Relational Queries to Boolean Reasoning}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {3:1--3:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-334-8}, ISSN = {1868-8969}, year = {2024}, volume = {305}, editor = {Chakraborty, Supratik and Jiang, Jie-Hong Roland}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.3}, URN = {urn:nbn:de:0030-drops-205253}, doi = {10.4230/LIPIcs.SAT.2024.3}, annote = {Keywords: Logic, Algorithms} }
Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)
Markus Anders, Sofia Brenner, and Gaurav Rattan. Satsuma: Structure-Based Symmetry Breaking in SAT. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 4:1-4:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{anders_et_al:LIPIcs.SAT.2024.4, author = {Anders, Markus and Brenner, Sofia and Rattan, Gaurav}, title = {{Satsuma: Structure-Based Symmetry Breaking in SAT}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {4:1--4:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-334-8}, ISSN = {1868-8969}, year = {2024}, volume = {305}, editor = {Chakraborty, Supratik and Jiang, Jie-Hong Roland}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.4}, URN = {urn:nbn:de:0030-drops-205269}, doi = {10.4230/LIPIcs.SAT.2024.4}, annote = {Keywords: symmetry breaking, boolean satisfiability, graph isomorphism} }
Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)
Olaf Beyersdorff, Johannes K. Fichte, Markus Hecher, Tim Hoffmann, and Kaspar Kasche. The Relative Strength of #SAT Proof Systems. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{beyersdorff_et_al:LIPIcs.SAT.2024.5, author = {Beyersdorff, Olaf and Fichte, Johannes K. and Hecher, Markus and Hoffmann, Tim and Kasche, Kaspar}, title = {{The Relative Strength of #SAT Proof Systems}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {5:1--5:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-334-8}, ISSN = {1868-8969}, year = {2024}, volume = {305}, editor = {Chakraborty, Supratik and Jiang, Jie-Hong Roland}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.5}, URN = {urn:nbn:de:0030-drops-205276}, doi = {10.4230/LIPIcs.SAT.2024.5}, annote = {Keywords: Model Counting, #SAT, Proof Complexity, Proof Systems, Lower Bounds, Knowledge Compilation} }
Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)
Armin Biere, Katalin Fazekas, Mathias Fleury, and Nils Froleyks. Clausal Congruence Closure. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 6:1-6:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{biere_et_al:LIPIcs.SAT.2024.6, author = {Biere, Armin and Fazekas, Katalin and Fleury, Mathias and Froleyks, Nils}, title = {{Clausal Congruence Closure}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {6:1--6:25}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-334-8}, ISSN = {1868-8969}, year = {2024}, volume = {305}, editor = {Chakraborty, Supratik and Jiang, Jie-Hong Roland}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.6}, URN = {urn:nbn:de:0030-drops-205287}, doi = {10.4230/LIPIcs.SAT.2024.6}, annote = {Keywords: Satisfiability Solving, Congruence Closure, Structural Hashing, SAT Sweeping, Conjunctive Normal Form, Combinational Equivalence Checking, Hardware Equivalence Checking} }
Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)
Ilario Bonacina, Maria Luisa Bonet, and Massimo Lauria. MaxSAT Resolution with Inclusion Redundancy. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 7:1-7:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{bonacina_et_al:LIPIcs.SAT.2024.7, author = {Bonacina, Ilario and Bonet, Maria Luisa and Lauria, Massimo}, title = {{MaxSAT Resolution with Inclusion Redundancy}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {7:1--7:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-334-8}, ISSN = {1868-8969}, year = {2024}, volume = {305}, editor = {Chakraborty, Supratik and Jiang, Jie-Hong Roland}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.7}, URN = {urn:nbn:de:0030-drops-205298}, doi = {10.4230/LIPIcs.SAT.2024.7}, annote = {Keywords: MaxSAT, Redundancy, MaxSAT resolution, Branch-and-bound, Pigeonhole principle, Parity Principle} }
Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)
Yi Chu, Chu-Min Li, Furong Ye, and Shaowei Cai. Enhancing MaxSAT Local Search via a Unified Soft Clause Weighting Scheme. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{chu_et_al:LIPIcs.SAT.2024.8, author = {Chu, Yi and Li, Chu-Min and Ye, Furong and Cai, Shaowei}, title = {{Enhancing MaxSAT Local Search via a Unified Soft Clause Weighting Scheme}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {8:1--8:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-334-8}, ISSN = {1868-8969}, year = {2024}, volume = {305}, editor = {Chakraborty, Supratik and Jiang, Jie-Hong Roland}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.8}, URN = {urn:nbn:de:0030-drops-205301}, doi = {10.4230/LIPIcs.SAT.2024.8}, annote = {Keywords: Weighted Partial MaxSAT, Local Search Method, Weighting Scheme} }
Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)
Robin Coutelier, Mathias Fleury, and Laura Kovács. Lazy Reimplication in Chronological Backtracking. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 9:1-9:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{coutelier_et_al:LIPIcs.SAT.2024.9, author = {Coutelier, Robin and Fleury, Mathias and Kov\'{a}cs, Laura}, title = {{Lazy Reimplication in Chronological Backtracking}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {9:1--9:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-334-8}, ISSN = {1868-8969}, year = {2024}, volume = {305}, editor = {Chakraborty, Supratik and Jiang, Jie-Hong Roland}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.9}, URN = {urn:nbn:de:0030-drops-205313}, doi = {10.4230/LIPIcs.SAT.2024.9}, annote = {Keywords: Chronological Backtracking, CDCL, Invariants, Watcher Lists} }
Feedback for Dagstuhl Publishing