@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}
}
The metadata provided by Dagstuhl Publishing on its webpages, as well as their export formats (such as XML or BibTeX) available at our website, is released under the CC0 1.0 Public Domain Dedication license. That is, you are free to copy, distribute, use, modify, transform, build upon, and produce derived works from our data, even for commercial purposes, all without asking permission. Of course, we are always happy if you provide a link to us as the source of the data.
Read the full CC0 1.0 legal code for the exact terms that apply: https://creativecommons.org/publicdomain/zero/1.0/legalcode
Feedback for Dagstuhl Publishing