SMT+PoS 2025
Satisfiability Modulo Theories & Pragmatics of SAT 2025

Table of Contents

• Preface
  Summary: SMT had 24 papers submitted for peer-review of which 19 were accepted, 6 as presentation-only, 3 as original papers, and 10 as extended abstract. PoS had 11 papers submitted for peer-review of which 10 were accepted, 6 as presentation-only and 4 regular paper. In total, there were 35 papers submitted for peer-review to these two workshops. Out of these, 29 papers were accepted, of which 17 appear in this volume, the remaining 12 being presentation-only. Of the published papers 7 are regular papers and 10 are short papers.

Part 1: SMT

Invited Talks Abstracts

• Deciding Satisfiability of Quantified Bitvector Formulae with BDDs 1
  Jan Strejček
• SAT Reasoning in CDCL(T) Solvers 2
  Katalin Fazekas

Original Papers

• Evaluating Binary Polynomials using Subpolynomials 3–15
  Jacob M. Howe, Martin Brain, Arnau Gàmez-Montolio
• An Optimization Modulo Theories-Based Approach to Cumulative Scheduling with Delays 16–28
  Antton Kasslin, Jeremias Berg
• A Proposal for an OMT Extension to SMT-LIB 29–44
  Nestan Tsiskaridze, Andrew Reynolds, Cesare Tinelli, Clark Barrett

Extended Abstracts

• Quantifier Instantiations: To Mimic or To Revolt 45–51
  Jan Jakubův, Mikoláš Janota
• From MBQI to Enumerative Instantiation and Back 52–58
  Marek Dančo, Petra Hozzová, Mikoláš Janota
• A Few Exercises on the Complexity of Congruence Closure with Cardinality Constraints 59–64
  Ellen Dasnois, Pascal Fontaine
• Constraint Propagation for Bit-Vectors in Alt-Ergo 65–76
  Hichem Rami Ait-El-Hara, Guillaume Bury, Basile Clément, Pierre Villemot
• Syntax-Guided Synthesis with Counterexample-Guided E-graphs: A Work-in-Progress Report 77–90
  Guy Frankel, Rudi Schneider, Michel Steuwer, Elizabeth Polgreen
• On Writing SMT-LIB Scripts: Metrics and a New Dataset 91–102
  Soaibuzzaman, Jan Oliver Ringert
• Comparative Analysis of SMT Solvers for Differential Cryptanalysis of SHA-2 103–125
  Marcel Barlik, Martin Brain
• Visualization of Execution Traces in Colibri 2 SMT Solver 126–135
  Christophe Junke, François Bobot
• A Conjecture Regarding SMT Instability 136–147
  Can Cebeci, Nikolaj Bjørner, George Candea, Clément Pit-Claudel
• Instability Track for SMT-COMP 148–152
  Amar Shah, Yi Zhou, Marijn Heule, Bryan Parno

Presentation-Only Papers (References)

• Being Polite is Not Enough (and Other Limits of Theory Combination)
  Guilherme Toledo, Benjamin Przybocki, Yoni Zohar
  CADE-30 (preprint available here)
• Satisfiability Modulo Exponential Integer Arithmetic
  Florian Frohn, Jürgen Giesl
  IJCAR 2024 (paper available here)
• Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search
  Enrico Lipparini, Thomas Hader, Ahmed Irfan, Stéphane Graham-Lengrand
  CADE-30 (preprint available here)
• Space Explanations of Neural Network Classification
  Faezeh Labbaf, Tomáš Kolárik, Martin Blicha, Grigory Fedyukovich, Michael Wand, Natasha Sharygina
  CAV 2025 (paper available here)
• Approximate SMT Counting Beyond Discrete Domains
  Arijit Shaw, Kuldeep S. Meel
  DAC 2025 (preprint available here)
• A Catalog of SMT-LIB Benchmarks
  Hans-Jörg Schurr, Mathias Preiner, Aina Niemetz, Clark Barrett, Pascal Fontaine, Cesare Tinelli
  (to be distributed with SMT-LIB benchmark library releases available here)

Part 2: PoS

Original Papers

• Revisiting Clause Vivification 153–167
  Florian Pollitt, Mathias Fleury, Armin Biere, Karem Sakallah, Marijn Heule, Jiawei Chen, Yonathan Fisseha
• SAT-Web: A Web-Based Educational SAT Visualisation Tool 168–176
  James Madgwick, Martin Mariusz Lester
• Improving Watched Pseudo-Boolean Propagation with Significant Literals 177–189
  Mia Müßig, Jan Johannsen
• Incremental Inprocessing Rules beyond Resolution 190–200
  Katalin Fazekas, Florian Pollitt, Mathias Fleury, Armin Biere

Presentation-Only Papers (References)

• Certifying Pareto Optimality in Multi-Objective Maximum Satisfiability
  Christoph Jabs, Jeremias Berg, Bart Bogaerts and Matti Järvisalo
  TACAS 2025 (paper available here)
• Conflict-Driven SAT Solving using XOR-OR-AND Normal Forms
  Julian Danner and Martin Kreuzer
• How to Discover Short, Shorter, and the Shortest Proofs of Unsatisfiability: A Branch-and-Bound Approach for Resolution Proof Length Minimization
  Konstantin Sidorov, Jacobus G. M. van der Linden, Gonçalo Correia, Mathijs de Weerdt and Emir Demirović
  (preprint available here)
• Certified Implicit Hitting Set Solving with Local Search for Pseudo-Boolean Optimization
  Benjamin Bogø, Xiamin Chen, Wietze Koops, Pinyan Lu, Jakob Nordström, Marc Vinyals and Qingzhao Wu
• Faster Certified Symmetry Breaking using Orders with Auxiliary Variables
  Markus Anders, Bart Bogaerts, Benjamin Bogø, Arthur Gontier, Wietze Koops, Ciaran McCreesh, Magnus Myreen, Jakob Nordström, Andy Oertel, Adrian Rebola-Pardo and Yong Kiam Tan
• Ordered Objectives in MaxSAT
  Jeremias Berg, André Schidler and Matti Järvisalo