SAtRes    News    Our FLoC 2026

Our FLoC 2026

July 28, 2026



Lake in the city of Lisbon, Portugal, near the conference venue


In the last two weeks, the Federated Logic Conference (FLoC) took place in Lisbon (Portugal). The aim of this large collection of conferences and events, which takes place once every four years, is to “[bring] together the world’s leading researchers in logic and computer science” (see FLoC webpage).

The collocated events at FLoC, among many others, particularly include the conferences on Theory & Applications of Satisfiability Testing (SAT) and Computer Aided Verification (CAV) as well as their associated workshops and competitions.

The days in Lisbon were a great occasion to connect with others from the broader formal methods community, have fun together, appreciate each other’s work, and discuss potential future projects. Moreover, our group was actively involved in several FLoC conferences, workshops, and competitions:


Pragmatics of SAT Workshop


Chaired by Bart Bogaerts (KU Leuven) and Dominik Schreiber (SAtRes), the 17th iteration of the Pragmatics of SAT (PoS) workshop took place July 19 as a SAT-affiliated FLoC workshop. Due to a record number of submissions, the workshop day was filled with many exciting and insightful talks and discussions, ranging from new MaxSAT solver implementations (Alexander Nadel et al. with “Aperture” and E. Justus et al. with an overhauled “MaxHS”) over a sophisticated educative online tool for illustrating SAT solving algorithms (W. Bermeo Quito et al., “SAT-IT”) to reverse-engineering the encoding model from a plain CNF formula via AI agents (J. Fichte et al.).

Following a successful and fun PoS workshop day (apart from high temperatures), the according proceedings are planned to be published soon at CEUR-WS.


SAT Paper: Natively Parallel Proofs


Ruben Götz (SAtRes) presented our work on the parallel proof framework PalRUP at the SAT conference. The according paper A Natively Parallel Proof Framework for Clause-Sharing SAT Solving (Ruben Götz, Michael Dörr, Dominik Schreiber) marks the first milestone in our DFG project Propositional Proofs as Big Data. We managed to devise a proof format for clause-sharing solving that allows to produce and check proofs in parallel. This greatly increases the scalability of fully dependable and certified SAT solving for critical use cases.

Ruben Götz during the presentation of PalRUP at SAT 2026


SAT and SMT Competition


For this year’s SAT competition, our submission to the Parallel and Cloud tracks featured a collaboration with Markus Anders (RPTU Kaiserslautern-Landau) and Cayden Codel (CMU) - augmenting Mallob’s preprocessing with their award-winning symmetry breaking tool Satsuma (TACAS'26 Distinguished Paper, SAT'26 Best Paper). The combination of these systems performed remarkably well, scoring the 1st place in the Parallel UNSAT sub-track and in the Parallel track overall. Being the only qualified participant in the 800-core Cloud track, Mallob remains uncontested as the most powerful SAT solver, solving more inputs than any other system:

We also submitted a variant featuring real-time proof checking (and CaDiCaL instead of Kissat solvers), which performed significantly weaker overall but in turn offers extremely high confidence in all obtained results.

SAT Competition 2026 Parallel track results, taken from Ashlin Iser’s presentation slides

For the SMT competition, we submitted Bitwuzllob, the (massively) parallel bit-precise verification tool based on a liaison of Bitwuzla (Aina Niemetz & Mathias Preiner, Stanford) and Mallob, to the 64-core Parallel track. Our system scored 1st in the non-incremental quantifier-free bit-vectors track (the only track where our system and sufficient competitors participated) by a wide margin and additionally leads the Best Overall Ranking in terms of the Parallel Track “Parallel Performance” and “UNSAT Performance” (3rd place in “SAT Performance”).


Invited talk at SMT Workshop


On July 25, Dominik Schreiber gave an invited talk entitled From Scalable SAT to Scalable SMT? - Successes and Challenges at this year’s SMT workshop, aiming to build a bridge between established methods in parallel SAT solving and the SMT world. This particularly included some thoughts on how we may exploit distributed (incremental) SAT solving or, more generally speaking, careful and flexible combinations of task parallelism and distributed combinatorial search in order to accelerate SMT solving.


Distinguished CAV Paper: Mallob - Automated Reasoning on Demand


We have received a CAV 2026 Distinguished Paper Award for our tool paper Mallob: Scalable Automated Reasoning On Demand (Dominik Schreiber, Niccolò Rigi-Luperti, Peter Sanders), presented July 27 by Dominik Schreiber at CAV.

The paper presents our distributed Automated Reasoning platform Mallob to the wider verification community: We provide an overview of the design, capabilities, and use cases of Mallob (such as incremental SAT for BMC, MaxSAT solving, and bit-blasting SMT solving), discuss a wide range of experimental results gathered throughout the last few years (including some new analyses surrounding incremental solving), and reflect on our system’s impact thus far (and going forward). The paper also lists and acknowledges the many contributors and collaboration partners we had the fortune to work with along the way.

We are excited about this recognition from the CAV community and hope that Mallob will continue to prove a valuable and powerful tool for researchers as well as industrial users.

Our CAV 2026 Distinguished Paper Award