@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} } @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} } @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} } @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} } @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} } @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} } @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} } @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} } @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} } @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} } @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} } @InProceedings{dahiya_et_al:LIPIcs.SAT.2024.10, author = {Dahiya, Yogesh and Mahajan, Meena and Mouli, Sasank}, title = {{New Lower Bounds for Polynomial Calculus over Non-Boolean Bases}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {10:1--10:20}, 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.10}, URN = {urn:nbn:de:0030-drops-205327}, doi = {10.4230/LIPIcs.SAT.2024.10}, annote = {Keywords: Proof Complexity, Polynomial Calculus, degree, Fourier basis, extension variables} } @InProceedings{decolnet:LIPIcs.SAT.2024.11, author = {de Colnet, Alexis}, title = {{On the Relative Efficiency of Dynamic and Static Top-Down Compilation to Decision-DNNF}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {11:1--11:21}, 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.11}, URN = {urn:nbn:de:0030-drops-205339}, doi = {10.4230/LIPIcs.SAT.2024.11}, annote = {Keywords: Knowledge compilation, top-down compilation, decision-DNNF Circuits} } @InProceedings{faber_et_al:LIPIcs.SAT.2024.12, author = {Faber, Daniel and Jabrayilov, Adalat and Mutzel, Petra}, title = {{SAT Encoding of Partial Ordering Models for Graph Coloring Problems}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {12:1--12:20}, 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.12}, URN = {urn:nbn:de:0030-drops-205340}, doi = {10.4230/LIPIcs.SAT.2024.12}, annote = {Keywords: Graph coloring, bandwidth coloring, SAT encodings, ILP formulations} } @InProceedings{fried_et_al:LIPIcs.SAT.2024.13, author = {Fried, Dror and Nadel, Alexander and Sebastiani, Roberto and Shalmon, Yogev}, title = {{Entailing Generalization Boosts Enumeration}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {13:1--13:14}, 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.13}, URN = {urn:nbn:de:0030-drops-205351}, doi = {10.4230/LIPIcs.SAT.2024.13}, annote = {Keywords: Generalization, Minimization, Prime Implicant, AllSAT, SAT, Circuits} } @InProceedings{havlena_et_al:LIPIcs.SAT.2024.14, author = {Havlena, Vojt\v{e}ch and Hol{\'\i}k, Luk\'{a}\v{s} and Leng\'{a}l, Ond\v{r}ej and S{\'\i}\v{c}, Juraj}, title = {{Cooking String-Integer Conversions with Noodles}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {14:1--14: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.14}, URN = {urn:nbn:de:0030-drops-205365}, doi = {10.4230/LIPIcs.SAT.2024.14}, annote = {Keywords: string solving, string conversions, SMT solving} } @InProceedings{holik_et_al:LIPIcs.SAT.2024.15, author = {Hol{\'\i}k, Luk\'{a}\v{s} and Vargov\v{c}{\'\i}k, Pavol}, title = {{Antichain with SAT and Tries}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {15:1--15:24}, 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.15}, URN = {urn:nbn:de:0030-drops-205372}, doi = {10.4230/LIPIcs.SAT.2024.15}, annote = {Keywords: SAT, Trie, Antichain, Alternating automata, Subset query} } @InProceedings{ignatiev_et_al:LIPIcs.SAT.2024.16, author = {Ignatiev, Alexey and Tan, Zi Li and Karamanos, Christos}, title = {{Towards Universally Accessible SAT Technology}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {16:1--16:11}, 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.16}, URN = {urn:nbn:de:0030-drops-205382}, doi = {10.4230/LIPIcs.SAT.2024.16}, annote = {Keywords: PySAT, Python, Prototyping, Practical Applicability} } @InProceedings{iida_et_al:LIPIcs.SAT.2024.17, author = {Iida, Yoichiro and Sonobe, Tomohiro and Inaba, Mary}, title = {{Parallel Clause Sharing Strategy Based on Graph Structure of SAT Problem}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {17:1--17: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.17}, URN = {urn:nbn:de:0030-drops-205392}, doi = {10.4230/LIPIcs.SAT.2024.17}, annote = {Keywords: SAT Solver, Structure of SAT, Parallel application, Clause Learning} } @InProceedings{iser_et_al:LIPIcs.SAT.2024.18, author = {Iser, Markus and Jabs, Christoph}, title = {{Global Benchmark Database}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {18:1--18:10}, 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.18}, URN = {urn:nbn:de:0030-drops-205405}, doi = {10.4230/LIPIcs.SAT.2024.18}, annote = {Keywords: Maintenance and Distribution of Benchmark Instances and their Features} } @InProceedings{itsykson_et_al:LIPIcs.SAT.2024.19, author = {Itsykson, Dmitry and Ovcharov, Sergei}, title = {{On Limits of Symbolic Approach to SAT Solving}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {19:1--19:22}, 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.19}, URN = {urn:nbn:de:0030-drops-205415}, doi = {10.4230/LIPIcs.SAT.2024.19}, annote = {Keywords: Symbolic quantifier elimination, OBDD, lower bounds, tree-like resolution, proof complexity, error-correcting codes, binary pigeonhole principle} } @InProceedings{kolodziejczyk_et_al:LIPIcs.SAT.2024.20, author = {Ko{\l}odziejczyk, Leszek Aleksander and Thapen, Neil}, title = {{The Strength of the Dominance Rule}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {20:1--20:22}, 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.20}, URN = {urn:nbn:de:0030-drops-205421}, doi = {10.4230/LIPIcs.SAT.2024.20}, annote = {Keywords: proof complexity, DRAT, symmetry breaking, dominance} } @InProceedings{lagniez_et_al:LIPIcs.SAT.2024.21, author = {Lagniez, Jean-Marie and Marquis, Pierre and Biere, Armin}, title = {{Dynamic Blocked Clause Elimination for Projected Model Counting}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {21:1--21:17}, 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.21}, URN = {urn:nbn:de:0030-drops-205430}, doi = {10.4230/LIPIcs.SAT.2024.21}, annote = {Keywords: Projected model counting, blocked clause elimination, propositional logic} } @InProceedings{nieuwenhuis_et_al:LIPIcs.SAT.2024.22, author = {Nieuwenhuis, Robert and Oliveras, Albert and Rodr{\'\i}guez-Carbonell, Enric and Zhao, Rui}, title = {{Speeding up Pseudo-Boolean Propagation}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {22:1--22: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.22}, URN = {urn:nbn:de:0030-drops-205449}, doi = {10.4230/LIPIcs.SAT.2024.22}, annote = {Keywords: SAT, Pseudo-Boolean Solving, Implementation-level Details} } @InProceedings{reichl_et_al:LIPIcs.SAT.2024.23, author = {Reichl, Franz-Xaver and Slivovsky, Friedrich and Szeider, Stefan}, title = {{eSLIM: Circuit Minimization with SAT Based Local Improvement}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {23:1--23:14}, 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.23}, URN = {urn:nbn:de:0030-drops-205458}, doi = {10.4230/LIPIcs.SAT.2024.23}, annote = {Keywords: QBF, Exact Synthesis, Circuit Minimization, SLIM} } @InProceedings{scholl_et_al:LIPIcs.SAT.2024.24, author = {Scholl, Christoph and Seufert, Tobias and Siegwolf, Fabian}, title = {{Hierarchical Stochastic SAT and Quality Assessment of Logic Locking}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {24:1--24:22}, 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.24}, URN = {urn:nbn:de:0030-drops-205462}, doi = {10.4230/LIPIcs.SAT.2024.24}, annote = {Keywords: Stochastic Boolean Satisfiability, Hierarchical Stochastic SAT, Binary Decision Diagrams, Decision Procedure} } @InProceedings{schreiber:LIPIcs.SAT.2024.25, author = {Schreiber, Dominik}, title = {{Trusted Scalable SAT Solving with On-The-Fly LRAT Checking}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {25:1--25: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.25}, URN = {urn:nbn:de:0030-drops-205477}, doi = {10.4230/LIPIcs.SAT.2024.25}, annote = {Keywords: SAT solving, distributed algorithms, proofs} } @InProceedings{shaik_et_al:LIPIcs.SAT.2024.26, author = {Shaik, Irfansha and van de Pol, Jaco}, title = {{Optimal Layout Synthesis for Deep Quantum Circuits on NISQ Processors with 100+ Qubits}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {26:1--26: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.26}, URN = {urn:nbn:de:0030-drops-205487}, doi = {10.4230/LIPIcs.SAT.2024.26}, annote = {Keywords: Layout Synthesis, Transpiling, Qubit Mapping and Routing, Quantum Circuits, Propositional Satisfiability, Parallel Plans} } @InProceedings{shavit_et_al:LIPIcs.SAT.2024.27, author = {Shavit, Hadar and Hoos, Holger H.}, title = {{Revisiting SATZilla Features in 2024}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {27:1--27:26}, 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.27}, URN = {urn:nbn:de:0030-drops-205496}, doi = {10.4230/LIPIcs.SAT.2024.27}, annote = {Keywords: Satisfiability, feature extraction, running time prediction, satisfiability prediction} } @InProceedings{slivovsky:LIPIcs.SAT.2024.28, author = {Slivovsky, Friedrich}, title = {{Strategy Extraction by Interpolation}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {28:1--28:20}, 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.28}, URN = {urn:nbn:de:0030-drops-205509}, doi = {10.4230/LIPIcs.SAT.2024.28}, annote = {Keywords: QBF, Expansion, Strategy Extraction, Interpolation} } @InProceedings{yang_et_al:LIPIcs.SAT.2024.29, author = {Yang, Jiong and Kharkov, Yaroslav A. and Shi, Yunong and Heule, Marijn J. H. and Dutertre, Bruno}, title = {{Quantum Circuit Mapping Based on Incremental and Parallel SAT Solving}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {29:1--29: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.29}, URN = {urn:nbn:de:0030-drops-205517}, doi = {10.4230/LIPIcs.SAT.2024.29}, annote = {Keywords: Quantum computing, Quantum compilation, SAT solving, Incremental solving, Parallel solving} } @InProceedings{yu_et_al:LIPIcs.SAT.2024.30, author = {Yu, Jinqiang and Farr, Graham and Ignatiev, Alexey and Stuckey, Peter J.}, title = {{Anytime Approximate Formal Feature Attribution}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {30:1--30: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.30}, URN = {urn:nbn:de:0030-drops-205526}, doi = {10.4230/LIPIcs.SAT.2024.30}, annote = {Keywords: Explainable AI, Formal Feature Attribution, Minimal Unsatisfiable Subsets, MUS Enumeration} } @InProceedings{zhang_et_al:LIPIcs.SAT.2024.31, author = {Zhang, Tianwei and Peitl, Tom\'{a}\v{s} and Szeider, Stefan}, title = {{Small Unsatisfiable k-CNFs with Bounded Literal Occurrence}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {31:1--31:22}, 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.31}, URN = {urn:nbn:de:0030-drops-205531}, doi = {10.4230/LIPIcs.SAT.2024.31}, annote = {Keywords: k-CNF, (k,s)-SAT, minimally unsatisfiable formulas, symmetry breaking} }