@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}
}