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