Proceedings

The proceedings are published as volume 341 of LIPIcs and available at: https://www.dagstuhl.de/dagpub/978-3-95977-381-2

Accepted Papers

  • Certifying Projected Knowledge Compilation 10.4230/LIPIcs.SAT.2025.8, Randal Bryant, Yong Kiam Tan, Marijn Heule
  • CNFs and DNFs with exactly k solutions 10.4230/LIPIcs.SAT.2025.9, L. Sunil Chandran, Rishikesh Gajjala, Kuldeep S. Meel
  • Scalable Precise Computation of Shannon Entropy 10.4230/LIPIcs.SAT.2025.20, Yong Lai, Haolong Tong, Zhenghang Xu, Minghao Yin
  • Enumerating All Boolean Matches 10.4230/LIPIcs.SAT.2025.22, Alexander Nadel, Yogev Shalmon
  • Towards Practical First-Order Model Counting 10.4230/LIPIcs.SAT.2025.18, Ananth Kidambi, Guramrit Singh, Paulius Dilkas, Kuldeep S. Meel
  • On Top-Down Pseudo-Boolean Model Counting 10.4230/LIPIcs.SAT.2025.31, Suwei Yang, Yong Lai, Kuldeep S. Meel
  • QRP+Gen: A Framework for Checking Q-Resolution Proofs with Generalized Axioms 10.4230/LIPIcs.SAT.2025.25, Mark Peyrer, Martina Seidl
  • An Algebraic Approach to MaxCSP 10.4230/LIPIcs.SAT.2025.6, Ilario Bonacina, Jordi Levy
  • Bit-precise Reasoning with Parametric Bit-vectors 10.4230/LIPIcs.SAT.2025.4, Zvika Berger, Yoni Zohar, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, Cesare Tinelli
  • Random local access for sampling k-SAT solutions 10.4230/LIPIcs.SAT.2025.13, Dingding Dong, Nitya Mani
  • Semi-Algebraic Proof Systems for QBF 10.4230/LIPIcs.SAT.2025.5, Olaf Beyersdorff, Ilario Bonacina, Kaspar Kasche, Meena Mahajan, Luc Spachmann
  • Better Extension Variables in DQBF via Independence 10.4230/LIPIcs.SAT.2025.11, Leroy Chew, Tomáš Peitl
  • Reencoding Unique Literal Clauses 10.4230/LIPIcs.SAT.2025.29, Aeacus Sheng, Joseph Reeves, Marijn Heule
  • SAT-Metropolis: Combining Markov Chain Monte Carlo with SAT/SMT sampling 10.4230/LIPIcs.SAT.2025.12, Maja Aaslyng Dall, Raúl Pardo, Thomas Lumley , Andrzej Wasowski
  • SAT-based CEGAR Method for the Hamiltonian Cycle Problem Enhanced by Cut-Set Constraints 10.4230/LIPIcs.SAT.2025.24, Ryoga Ohashi, Takehide Soh, Daniel Le Berre, Hidetomo Nabeshima, Mutsunori Banbara, Katsumi Inoue, Naoyuki Tamura
  • CNOT-Optimal Clifford Synthesis as SAT 10.4230/LIPIcs.SAT.2025.28, Irfansha Shaik, Jaco van de Pol
  • Depth-Optimal Quantum Layout Synthesis as SAT 10.4230/LIPIcs.SAT.2025.16, Anna B. Jakobsen, Anders B. Clausen, Jaco van de Pol, Irfansha Shaik
  • Fine-Grained Complexity Analysis of Dependency Quantified Boolean Formulas 10.4230/LIPIcs.SAT.2025.10, Che Cheng, Long-Hin Fung, Jie-Hong Roland Jiang, Friedrich Slivovsky, Tony Tan
  • Problem Partitioning via Proof Prefixes 10.4230/LIPIcs.SAT.2025.3, Zachary Battleman, Joseph Reeves, Marijn Heule
  • Analyzing Reformulation Performance in Core-Guided MaxSAT Solving 10.4230/LIPIcs.SAT.2025.26, Andre Schidler, Stefan Szeider
  • Redundancy rules for MaxSAT 10.4230/LIPIcs.SAT.2025.7, Ilario Bonacina, María-Luisa Bonet, Sam Buss, Massimo Lauria
  • Symbolic Conflict Analysis in Pseudo-Boolean Optimization 10.4230/LIPIcs.SAT.2025.23, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez Carbonell, Rui Zhao
  • Streamlining Distributed SAT Solver Design 10.4230/LIPIcs.SAT.2025.27, Dominik Schreiber, Niccolò Rigi-Luperti, Armin Biere
  • RustSAT: A Library for SAT Solving in Rust 10.4230/LIPIcs.SAT.2025.15, Christoph Jabs
  • Learn to Unlearn 10.4230/LIPIcs.SAT.2025.14, Bernhard Gstrein, Florian Pollitt, André Schidler, Mathias Fleury, Armin Biere
  • Improving Reduction Techniques in Pseudo-Boolean Conflictct Analysis 10.4230/LIPIcs.SAT.2025.21, Orestis Lomis, Jo Devriendt, Hendrik Bierlee, Tias Guns
  • Core-Guided Linear Programming-based Maximum Satisfiability 10.4230/LIPIcs.SAT.2025.17, George Katsirelos
  • Bridging Language Models and Symbolic Solvers via the the Model Context Protocol 10.4230/LIPIcs.SAT.2025.30, Stefan Szeider
  • Efficient Certified Reasoning for Binarized Neural Networks 10.4230/LIPIcs.SAT.2025.32, Jiong Yang, Yong Kiam Tan, Mate Soos, Magnus O. Myreen, Kuldeep S. Meel
  • An application of SAT solvers in Integer Programming Games 10.4230/LIPIcs.SAT.2025.19, Pravesh Koirala, Aditya Shrey, Forrest Laine