<h2>LIPIcs, Volume 271, SAT 2023</h2>
<ul>
<li>
<span class="authors">Meena Mahajan and Friedrich Slivovsky</span>
<span class="title">LIPIcs, Volume 271, SAT 2023, Complete Volume</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.SAT.2023">10.4230/LIPIcs.SAT.2023</a>
</li>
<li>
<span class="authors">Meena Mahajan and Friedrich Slivovsky</span>
<span class="title">Front Matter, Table of Contents, Preface, Conference Organization</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.SAT.2023.0">10.4230/LIPIcs.SAT.2023.0</a>
</li>
<li>
<span class="authors">Markus Anders, Pascal Schweitzer, and Mate Soos</span>
<span class="title">Algorithms Transcending the SAT-Symmetry Interface</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.SAT.2023.1">10.4230/LIPIcs.SAT.2023.1</a>
</li>
<li>
<span class="authors">Olaf Beyersdorff, Tim Hoffmann, and Luc Nicolas Spachmann</span>
<span class="title">Proof Complexity of Propositional Model Counting</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.SAT.2023.2">10.4230/LIPIcs.SAT.2023.2</a>
</li>
<li>
<span class="authors">Armin Biere, Nils Froleyks, and Wenxi Wang</span>
<span class="title">CadiBack: Extracting Backbones with CaDiCaL</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.SAT.2023.3">10.4230/LIPIcs.SAT.2023.3</a>
</li>
<li>
<span class="authors">Benjamin Böhm and Olaf Beyersdorff</span>
<span class="title">QCDCL vs QBF Resolution: Further Insights</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.SAT.2023.4">10.4230/LIPIcs.SAT.2023.4</a>
</li>
<li>
<span class="authors">Ilario Bonacina, Maria Luisa Bonet, and Jordi Levy</span>
<span class="title">Polynomial Calculus for MaxSAT</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.SAT.2023.5">10.4230/LIPIcs.SAT.2023.5</a>
</li>
<li>
<span class="authors">Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad, and Marijn J. H. Heule</span>
<span class="title">Certified Knowledge Compilation with Application to Verified Model Counting</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.SAT.2023.6">10.4230/LIPIcs.SAT.2023.6</a>
</li>
<li>
<span class="authors">Alexis de Colnet</span>
<span class="title">Separating Incremental and Non-Incremental Bottom-Up Compilation</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.SAT.2023.7">10.4230/LIPIcs.SAT.2023.7</a>
</li>
<li>
<span class="authors">Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, and Armin Biere</span>
<span class="title">IPASIR-UP: User Propagators for CDCL</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.SAT.2023.8">10.4230/LIPIcs.SAT.2023.8</a>
</li>
<li>
<span class="authors">Dror Fried, Alexander Nadel, and Yogev Shalmon</span>
<span class="title">AllSAT for Combinational Circuits</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.SAT.2023.9">10.4230/LIPIcs.SAT.2023.9</a>
</li>
<li>
<span class="authors">Long-Hin Fung and Tony Tan</span>
<span class="title">On the Complexity of k-DQBF</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.SAT.2023.10">10.4230/LIPIcs.SAT.2023.10</a>
</li>
<li>
<span class="authors">Andrew Haberlandt, Harrison Green, and Marijn J. H. Heule</span>
<span class="title">Effective Auxiliary Variables via Structured Reencoding</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.SAT.2023.11">10.4230/LIPIcs.SAT.2023.11</a>
</li>
<li>
<span class="authors">George Katsirelos</span>
<span class="title">An Analysis of Core-Guided Maximum Satisfiability Solvers Using Linear Programming</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.SAT.2023.12">10.4230/LIPIcs.SAT.2023.12</a>
</li>
<li>
<span class="authors">Markus Kirchweger, Tomáš Peitl, and Stefan Szeider</span>
<span class="title">A SAT Solver’s Opinion on the Erdős-Faber-Lovász Conjecture</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.SAT.2023.13">10.4230/LIPIcs.SAT.2023.13</a>
</li>
<li>
<span class="authors">Markus Kirchweger, Manfred Scheucher, and Stefan Szeider</span>
<span class="title">SAT-Based Generation of Planar Graphs</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.SAT.2023.14">10.4230/LIPIcs.SAT.2023.14</a>
</li>
<li>
<span class="authors">Gabriele Masina, Giuseppe Spallitta, and Roberto Sebastiani</span>
<span class="title">On CNF Conversion for Disjoint SAT Enumeration</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.SAT.2023.15">10.4230/LIPIcs.SAT.2023.15</a>
</li>
<li>
<span class="authors">Stefan Mengel</span>
<span class="title">Bounds on BDD-Based Bucket Elimination</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.SAT.2023.16">10.4230/LIPIcs.SAT.2023.16</a>
</li>
<li>
<span class="authors">Alexander Nadel</span>
<span class="title">Solving Huge Instances with Intel(R) SAT Solver</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.SAT.2023.17">10.4230/LIPIcs.SAT.2023.17</a>
</li>
<li>
<span class="authors">Albert Oliveras, Chunxiao Li, Darryl Wu, Jonathan Chung, and Vijay Ganesh</span>
<span class="title">Learning Shorter Redundant Clauses in SDCL Using MaxSAT</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.SAT.2023.18">10.4230/LIPIcs.SAT.2023.18</a>
</li>
<li>
<span class="authors">Pedro Orvalho, Vasco Manquinho, and Ruben Martins</span>
<span class="title">UpMax: User Partitioning for MaxSAT</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.SAT.2023.19">10.4230/LIPIcs.SAT.2023.19</a>
</li>
<li>
<span class="authors">Andreas Plank and Martina Seidl</span>
<span class="title">QMusExt: A Minimal (Un)satisfiable Core Extractor for Quantified Boolean Formulas</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.SAT.2023.20">10.4230/LIPIcs.SAT.2023.20</a>
</li>
<li>
<span class="authors">Florian Pollitt, Mathias Fleury, and Armin Biere</span>
<span class="title">Faster LRAT Checking Than Solving with CaDiCaL</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.SAT.2023.21">10.4230/LIPIcs.SAT.2023.21</a>
</li>
<li>
<span class="authors">Adrián Rebola-Pardo</span>
<span class="title">Even Shorter Proofs Without New Variables</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.SAT.2023.22">10.4230/LIPIcs.SAT.2023.22</a>
</li>
<li>
<span class="authors">Tereza Schwarzová, Jan Strejček, and Juraj Major</span>
<span class="title">Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.SAT.2023.23">10.4230/LIPIcs.SAT.2023.23</a>
</li>
<li>
<span class="authors">Irfansha Shaik, Maximilian Heisinger, Martina Seidl, and Jaco van de Pol</span>
<span class="title">Validation of QBF Encodings with Winning Strategies</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.SAT.2023.24">10.4230/LIPIcs.SAT.2023.24</a>
</li>
<li>
<span class="authors">Anshujit Sharma, Matthew Burns, and Michael C. Huang</span>
<span class="title">Combining Cubic Dynamical Solvers with Make/Break Heuristics to Solve SAT</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.SAT.2023.25">10.4230/LIPIcs.SAT.2023.25</a>
</li>
<li>
<span class="authors">Jacobo Torán and Florian Wörz</span>
<span class="title">Cutting Planes Width and the Complexity of Graph Isomorphism Refutations</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.SAT.2023.26">10.4230/LIPIcs.SAT.2023.26</a>
</li>
<li>
<span class="authors">Marc Vinyals, Chunxiao Li, Noah Fleming, Antonina Kolokolova, and Vijay Ganesh</span>
<span class="title">Limits of CDCL Learning via Merge Resolution</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.SAT.2023.27">10.4230/LIPIcs.SAT.2023.27</a>
</li>
<li>
<span class="authors">Jiong Yang, Arijit Shaw, Teodora Baluta, Mate Soos, and Kuldeep S. Meel</span>
<span class="title">Explaining SAT Solving Using Causal Reasoning</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.SAT.2023.28">10.4230/LIPIcs.SAT.2023.28</a>
</li>
<li>
<span class="authors">Junping Zhou, Jiaxin Liang, Minghao Yin, and Bo He</span>
<span class="title">LS-DTKMS: A Local Search Algorithm for Diversified Top-k MaxSAT Problem</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.SAT.2023.29">10.4230/LIPIcs.SAT.2023.29</a>
</li>
<li>
<span class="authors">Neng-Fa Zhou, Ruiwei Wang, and Roland H. C. Yap</span>
<span class="title">A Comparison of SAT Encodings for Acyclicity of Directed Graphs</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.SAT.2023.30">10.4230/LIPIcs.SAT.2023.30</a>
</li>
</ul>
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