SMT 2025

Invited Speakers

Jan Strejček, Masaryk University, Brno

The talk will explain a naive approach to deciding the satisfiability of quantified bitvector formulae based on binary decision diagrams. We then describe techniques and improvements that make this approach competitive, namely simplifications of formulas with unconstrained variables, approximations based on effective bit-width reduction, and operation abstraction. Finally, we present some future research directions.

Katalin Fazekas, TU Wien

In our recent work we introduced an extension for the IPASIR interface of incremental SAT solvers. This extension, named IPASIR-UP, supports continuous interactions with the solver during SAT reasoning, allowing SMT solvers to seamlessly integrate any IPASIR-UP-compatible SAT solver as their core engine. While IPASIR-UP enables crucial interactions between SAT and theory solvers, the full potential of modern incremental SAT features, such as advanced inprocessing techniques, comprehensive proof production, and diverse search heuristics, remains largely untapped within this framework. In this talk, I will present the current landscape of embedding SAT solvers into SMT solvers via IPASIR-UP. I will highlight the currently supported features, discuss their limitations, and present some open problems and challenges that need to be addressed in the future.

This talk is based on joint work with Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, and Armin Biere.