@Proceedings{mahajan_et_al:LIPIcs.SAT.2023,
title = {{LIPIcs, Volume 271, SAT 2023, Complete Volume}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {1--522},
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},
URN = {urn:nbn:de:0030-drops-184615},
doi = {10.4230/LIPIcs.SAT.2023},
annote = {Keywords: LIPIcs, Volume 271, SAT 2023, Complete Volume}
}
@InProceedings{mahajan_et_al:LIPIcs.SAT.2023.0,
author = {Mahajan, Meena and Slivovsky, Friedrich},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {0:i--0:xviii},
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.0},
URN = {urn:nbn:de:0030-drops-184625},
doi = {10.4230/LIPIcs.SAT.2023.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
@InProceedings{anders_et_al:LIPIcs.SAT.2023.1,
author = {Anders, Markus and Schweitzer, Pascal and Soos, Mate},
title = {{Algorithms Transcending the SAT-Symmetry Interface}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {1:1--1:21},
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.1},
URN = {urn:nbn:de:0030-drops-184635},
doi = {10.4230/LIPIcs.SAT.2023.1},
annote = {Keywords: boolean satisfiability, symmetry exploitation, computational group theory}
}
@InProceedings{beyersdorff_et_al:LIPIcs.SAT.2023.2,
author = {Beyersdorff, Olaf and Hoffmann, Tim and Spachmann, Luc Nicolas},
title = {{Proof Complexity of Propositional Model Counting}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {2:1--2:18},
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.2},
URN = {urn:nbn:de:0030-drops-184647},
doi = {10.4230/LIPIcs.SAT.2023.2},
annote = {Keywords: model counting, #SAT, proof complexity, proof systems, lower bounds}
}
@InProceedings{biere_et_al:LIPIcs.SAT.2023.3,
author = {Biere, Armin and Froleyks, Nils and Wang, Wenxi},
title = {{CadiBack: Extracting Backbones with CaDiCaL}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {3:1--3:12},
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.3},
URN = {urn:nbn:de:0030-drops-184655},
doi = {10.4230/LIPIcs.SAT.2023.3},
annote = {Keywords: Satisfiability, Backbone, Incremental Solving}
}
@InProceedings{bohm_et_al:LIPIcs.SAT.2023.4,
author = {B\"{o}hm, Benjamin and Beyersdorff, Olaf},
title = {{QCDCL vs QBF Resolution: Further Insights}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {4:1--4:17},
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.4},
URN = {urn:nbn:de:0030-drops-184660},
doi = {10.4230/LIPIcs.SAT.2023.4},
annote = {Keywords: QBF, CDCL, resolution, proof complexity, simulations, lower bounds}
}
@InProceedings{bonacina_et_al:LIPIcs.SAT.2023.5,
author = {Bonacina, Ilario and Bonet, Maria Luisa and Levy, Jordi},
title = {{Polynomial Calculus for MaxSAT}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {5:1--5:17},
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.5},
URN = {urn:nbn:de:0030-drops-184670},
doi = {10.4230/LIPIcs.SAT.2023.5},
annote = {Keywords: Polynomial Calculus, MaxSAT, Proof systems, Algebraic reasoning}
}
@InProceedings{bryant_et_al:LIPIcs.SAT.2023.6,
author = {Bryant, Randal E. and Nawrocki, Wojciech and Avigad, Jeremy and Heule, Marijn J. H.},
title = {{Certified Knowledge Compilation with Application to Verified Model Counting}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {6:1--6:20},
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.6},
URN = {urn:nbn:de:0030-drops-184685},
doi = {10.4230/LIPIcs.SAT.2023.6},
annote = {Keywords: Propositional model counting, Proof checking}
}
@InProceedings{decolnet:LIPIcs.SAT.2023.7,
author = {de Colnet, Alexis},
title = {{Separating Incremental and Non-Incremental Bottom-Up Compilation}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {7:1--7:20},
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.7},
URN = {urn:nbn:de:0030-drops-184696},
doi = {10.4230/LIPIcs.SAT.2023.7},
annote = {Keywords: Knowledge Compilation, Bottom-up Compilation, DNNF, OBDD}
}
@InProceedings{fazekas_et_al:LIPIcs.SAT.2023.8,
author = {Fazekas, Katalin and Niemetz, Aina and Preiner, Mathias and Kirchweger, Markus and Szeider, Stefan and Biere, Armin},
title = {{IPASIR-UP: User Propagators for CDCL}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {8:1--8:13},
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.8},
URN = {urn:nbn:de:0030-drops-184709},
doi = {10.4230/LIPIcs.SAT.2023.8},
annote = {Keywords: SAT, CDCL, Satisfiability Modulo Theories, Satisfiability Modulo Symmetries}
}
@InProceedings{fried_et_al:LIPIcs.SAT.2023.9,
author = {Fried, Dror and Nadel, Alexander and Shalmon, Yogev},
title = {{AllSAT for Combinational Circuits}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {9:1--9:18},
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.9},
URN = {urn:nbn:de:0030-drops-184717},
doi = {10.4230/LIPIcs.SAT.2023.9},
annote = {Keywords: AllSAT, SAT, Circuits}
}
@InProceedings{fung_et_al:LIPIcs.SAT.2023.10,
author = {Fung, Long-Hin and Tan, Tony},
title = {{On the Complexity of k-DQBF}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {10:1--10:15},
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.10},
URN = {urn:nbn:de:0030-drops-184729},
doi = {10.4230/LIPIcs.SAT.2023.10},
annote = {Keywords: Dependency quantified boolean formulas, existential variables, complexity}
}
@InProceedings{haberlandt_et_al:LIPIcs.SAT.2023.11,
author = {Haberlandt, Andrew and Green, Harrison and Heule, Marijn J. H.},
title = {{Effective Auxiliary Variables via Structured Reencoding}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {11:1--11: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.11},
URN = {urn:nbn:de:0030-drops-184736},
doi = {10.4230/LIPIcs.SAT.2023.11},
annote = {Keywords: Reencoding, Auxiliary Variables, Extended Resolution}
}
@InProceedings{katsirelos:LIPIcs.SAT.2023.12,
author = {Katsirelos, George},
title = {{An Analysis of Core-Guided Maximum Satisfiability Solvers Using Linear Programming}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {12:1--12: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.12},
URN = {urn:nbn:de:0030-drops-184745},
doi = {10.4230/LIPIcs.SAT.2023.12},
annote = {Keywords: maximum satisfiability, core-guided solvers, minimum hitting set problem, linear programming}
}
@InProceedings{kirchweger_et_al:LIPIcs.SAT.2023.13,
author = {Kirchweger, Markus and Peitl, Tom\'{a}\v{s} and Szeider, Stefan},
title = {{A SAT Solver’s Opinion on the Erd\H{o}s-Faber-Lov\'{a}sz Conjecture}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {13:1--13:17},
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.13},
URN = {urn:nbn:de:0030-drops-184752},
doi = {10.4230/LIPIcs.SAT.2023.13},
annote = {Keywords: hypergraphs, graph coloring, SAT modulo symmetries}
}
@InProceedings{kirchweger_et_al:LIPIcs.SAT.2023.14,
author = {Kirchweger, Markus and Scheucher, Manfred and Szeider, Stefan},
title = {{SAT-Based Generation of Planar Graphs}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {14:1--14:18},
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.14},
URN = {urn:nbn:de:0030-drops-184767},
doi = {10.4230/LIPIcs.SAT.2023.14},
annote = {Keywords: SAT modulo Symmetry (SMS), dynamic symmetry breaking, planarity test, universal point set, order dimension, Schnyder’s theorem, Kuratowski’s theorem, Tur\'{a}n’s theorem, Earth-Moon problem}
}
@InProceedings{masina_et_al:LIPIcs.SAT.2023.15,
author = {Masina, Gabriele and Spallitta, Giuseppe and Sebastiani, Roberto},
title = {{On CNF Conversion for Disjoint SAT Enumeration}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {15:1--15:16},
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.15},
URN = {urn:nbn:de:0030-drops-184775},
doi = {10.4230/LIPIcs.SAT.2023.15},
annote = {Keywords: CNF conversion, AllSAT, AllSMT}
}
@InProceedings{mengel:LIPIcs.SAT.2023.16,
author = {Mengel, Stefan},
title = {{Bounds on BDD-Based Bucket Elimination}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {16:1--16:11},
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.16},
URN = {urn:nbn:de:0030-drops-184789},
doi = {10.4230/LIPIcs.SAT.2023.16},
annote = {Keywords: Bucket Elimination, Binary Decision Diagrams, Satisfiability, Complexity}
}
@InProceedings{nadel:LIPIcs.SAT.2023.17,
author = {Nadel, Alexander},
title = {{Solving Huge Instances with Intel(R) SAT Solver}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {17:1--17:12},
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.17},
URN = {urn:nbn:de:0030-drops-184790},
doi = {10.4230/LIPIcs.SAT.2023.17},
annote = {Keywords: SAT, CDCL}
}
@InProceedings{oliveras_et_al:LIPIcs.SAT.2023.18,
author = {Oliveras, Albert and Li, Chunxiao and Wu, Darryl and Chung, Jonathan and Ganesh, Vijay},
title = {{Learning Shorter Redundant Clauses in SDCL Using MaxSAT}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {18:1--18:17},
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.18},
URN = {urn:nbn:de:0030-drops-184803},
doi = {10.4230/LIPIcs.SAT.2023.18},
annote = {Keywords: SAT, SDCL, MaxSAT}
}
@InProceedings{orvalho_et_al:LIPIcs.SAT.2023.19,
author = {Orvalho, Pedro and Manquinho, Vasco and Martins, Ruben},
title = {{UpMax: User Partitioning for MaxSAT}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {19:1--19:13},
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.19},
URN = {urn:nbn:de:0030-drops-184819},
doi = {10.4230/LIPIcs.SAT.2023.19},
annote = {Keywords: Maximum Satisfiability, Formula partitioning, Graph-based methods}
}
@InProceedings{plank_et_al:LIPIcs.SAT.2023.20,
author = {Plank, Andreas and Seidl, Martina},
title = {{QMusExt: A Minimal (Un)satisfiable Core Extractor for Quantified Boolean Formulas}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {20:1--20:10},
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.20},
URN = {urn:nbn:de:0030-drops-184824},
doi = {10.4230/LIPIcs.SAT.2023.20},
annote = {Keywords: Minimal Unsatisfiable Core, Quantified Boolean Formula}
}
@InProceedings{pollitt_et_al:LIPIcs.SAT.2023.21,
author = {Pollitt, Florian and Fleury, Mathias and Biere, Armin},
title = {{Faster LRAT Checking Than Solving with CaDiCaL}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {21:1--21:12},
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.21},
URN = {urn:nbn:de:0030-drops-184837},
doi = {10.4230/LIPIcs.SAT.2023.21},
annote = {Keywords: SAT solving, Proof Checking, DRAT, LRAT, FRAT}
}
@InProceedings{rebolapardo:LIPIcs.SAT.2023.22,
author = {Rebola-Pardo, Adri\'{a}n},
title = {{Even Shorter Proofs Without New Variables}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {22:1--22:20},
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.22},
URN = {urn:nbn:de:0030-drops-184844},
doi = {10.4230/LIPIcs.SAT.2023.22},
annote = {Keywords: Interference, SAT solving, Unsatisfiability proofs, Unsatisfiable cores}
}
@InProceedings{schwarzova_et_al:LIPIcs.SAT.2023.23,
author = {Schwarzov\'{a}, Tereza and Strej\v{c}ek, Jan and Major, Juraj},
title = {{Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {23:1--23:20},
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.23},
URN = {urn:nbn:de:0030-drops-184859},
doi = {10.4230/LIPIcs.SAT.2023.23},
annote = {Keywords: Emerson-Lei automata, TELA, automata reduction, QBF, telatko}
}
@InProceedings{shaik_et_al:LIPIcs.SAT.2023.24,
author = {Shaik, Irfansha and Heisinger, Maximilian and Seidl, Martina and van de Pol, Jaco},
title = {{Validation of QBF Encodings with Winning Strategies}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {24:1--24:10},
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.24},
URN = {urn:nbn:de:0030-drops-184863},
doi = {10.4230/LIPIcs.SAT.2023.24},
annote = {Keywords: QBF, Validation, Winning Strategy, Equivalence, Certificates}
}
@InProceedings{sharma_et_al:LIPIcs.SAT.2023.25,
author = {Sharma, Anshujit and Burns, Matthew and Huang, Michael C.},
title = {{Combining Cubic Dynamical Solvers with Make/Break Heuristics to Solve SAT}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {25:1--25:21},
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.25},
URN = {urn:nbn:de:0030-drops-184871},
doi = {10.4230/LIPIcs.SAT.2023.25},
annote = {Keywords: Satisfiability, Ising machines, Stochastic Heuristics, Natural Computation}
}
@InProceedings{toran_et_al:LIPIcs.SAT.2023.26,
author = {Tor\'{a}n, Jacobo and W\"{o}rz, Florian},
title = {{Cutting Planes Width and the Complexity of Graph Isomorphism Refutations}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {26:1--26:20},
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.26},
URN = {urn:nbn:de:0030-drops-184884},
doi = {10.4230/LIPIcs.SAT.2023.26},
annote = {Keywords: Cutting Planes, Proof Complexity, Linear Programming, Combinatorial Optimization, Weisfeiler-Leman Algorithm, Graph Isomorphism}
}
@InProceedings{vinyals_et_al:LIPIcs.SAT.2023.27,
author = {Vinyals, Marc and Li, Chunxiao and Fleming, Noah and Kolokolova, Antonina and Ganesh, Vijay},
title = {{Limits of CDCL Learning via Merge Resolution}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {27:1--27: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.27},
URN = {urn:nbn:de:0030-drops-184894},
doi = {10.4230/LIPIcs.SAT.2023.27},
annote = {Keywords: proof complexity, resolution, merge resolution, CDCL, learning scheme}
}
@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}
}
@InProceedings{zhou_et_al:LIPIcs.SAT.2023.29,
author = {Zhou, Junping and Liang, Jiaxin and Yin, Minghao and He, Bo},
title = {{LS-DTKMS: A Local Search Algorithm for Diversified Top-k MaxSAT Problem}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {29:1--29:16},
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.29},
URN = {urn:nbn:de:0030-drops-184912},
doi = {10.4230/LIPIcs.SAT.2023.29},
annote = {Keywords: Top-k, MaxSAT, local search}
}
@InProceedings{zhou_et_al:LIPIcs.SAT.2023.30,
author = {Zhou, Neng-Fa and Wang, Ruiwei and Yap, Roland H. C.},
title = {{A Comparison of SAT Encodings for Acyclicity of Directed Graphs}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {30:1--30:9},
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.30},
URN = {urn:nbn:de:0030-drops-184927},
doi = {10.4230/LIPIcs.SAT.2023.30},
annote = {Keywords: Graph constraints, Acyclic constraint, SAT encoding, Graph Synthesis}
}
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