Original: https://ceur-ws.org/Vol-4008/ | Mirror: https://ceur-ws.wikidata.dbis.rwth-aachen.de/Vol-4008/ | Year: 2025

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 https://creativecommons.org/licenses/by/4.0/.

SMT+PoS 2025

Joint Proceedings of the 23rd International Workshop on Satisfiability Modulo Theories and the 16th Pragmatics of SAT International Workshop
co-located with CP 2025 & SAT 2025 & SoCS 2025

Glasgow, UK, August 10–11, 2025.

Edited by

Jochen Hoenicke
Mikoláš Janota
Aina Niemetz
Sophie Tourret

Table of Contents

PDF
Deciding Satisfiability of Quantified Bitvector Formulae with BDDs 1-1 PDF
Jan Strejček
SAT Reasoning in CDCL(T) Solvers 2-2 PDF
Katalin Fazekas
Evaluating Binary Polynomials using Subpolynomials 3-15 PDF
Jacob M. Howe, Martin Brain, Arnau Gàmez-Montolio
An Optimization Modulo Theories-Based Approach to Cumulative Scheduling with Delays 16-28 PDF
Antton Kasslin, Jeremias Berg
A Proposal for an OMT Extension to SMT-LIB 29-44 PDF
Nestan Tsiskaridze, Andrew Reynolds, Cesare Tinelli, Clark Barrett
Quantifier Instantiations: To Mimic or To Revolt 45-51 PDF
Jan Jakubův, Mikoláš Janota
From MBQI to Enumerative Instantiation and Back 52-58 PDF
Marek Dančo, Petra Hozzová, Mikoláš Janota
A Few Exercises on the Complexity of Congruence Closure with Cardinality Constraints 59-64 PDF
Ellen Dasnois, Pascal Fontaine
Constraint Propagation for Bit-Vectors in Alt-Ergo 65-76 PDF
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 PDF
Guy Frankel, Rudi Schneider, Michel Steuwer, Elizabeth Polgreen
On Writing SMT-LIB Scripts: Metrics and a New Dataset 91-102 PDF
Soaibuzzaman, Jan Oliver Ringert
Comparative Analysis of SMT Solvers for Differential Cryptanalysis of SHA-2 103-125 PDF
Marcel Barlik, Martin Brain
Visualization of Execution Traces in Colibri 2 SMT Solver 126-135 PDF
Christophe Junke, François Bobot
A Conjecture Regarding SMT Instability 136-147 PDF
Can Cebeci, Nikolaj Bjørner, George Candea, Clément Pit-Claudel
Instability Track for SMT-COMP 148-152 PDF
Amar Shah, Yi Zhou, Marijn Heule, Bryan Parno
Revisiting Clause Vivification 153-167 PDF
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 PDF
James Madgwick, Martin Mariusz Lester
Improving Watched Pseudo-Boolean Propagation with Significant Literals 177-189 PDF
Mia Müßig, Jan Johannsen
Incremental Inprocessing Rules beyond Resolution 190-200 PDF
Katalin Fazekas, Florian Pollitt, Mathias Fleury, Armin Biere
PDF
PDF
PDF
PDF
PDF

2025-08-07: published on CEUR Workshop Proceedings (CEUR-WS.org, ISSN 1613-0073) |valid HTML5|