| Vol-4008 urn:nbn:de:0074-4008-X Copyright © 2025 for the individual papers by the papers' authors. Copyright © 2025 for the volume as a collection by its editors. This volume and its papers are published under the Creative Commons License Attribution 4.0 International (CC BY 4.0).

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

### Joint Proceedings of the 23rd International Workshop on Satisfiability Modulo Theories and the 16th Pragmatics of SAT International Workshop
co-located with the 31st International Conference on Principles and Practice of Constraint Programming, the 28th International Conference on Theory and Applications of Satisfiability Testing and the 18th International Symposium on Combinatorial Search (CP 2025 & SAT 2025 & SoCS 2025)

### Glasgow, UK, August 10–11, 2025.

### Websites: SMT 2025 and PoS 2025

Edited by

### Jochen Hoenicke 1 (SMT)
Mikoláš Janota 2 (PoS)
Aina Niemetz 3 (PoS)
Sophie Tourret 4,5 (SMT)

1 Certora GmbH, Schleißheimer Str. 23, 80233 München, Germany
2 CIIRC, CTU Prague, Jugoslávských partyzánů 1580/3, 160 00 Prague 6, Prague, Czech Republic
3 Stanford University, 450 Jane Stanford Way Stanford, CA 94305-2004, USA
4 Inria, Loria, CNRS, Lorraine Univ., France
5 Max Planck Institute for Informatics, Saarland University Campus, Saarland, Germany

## 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

2025-07-28: submitted by Jochen Hoenicke, metadata incl. bibliographic data published under Creative Commons CC0
2025-08-07: published on CEUR Workshop Proceedings (CEUR-WS.org, ISSN 1613-0073) |valid HTML5|