SAtRes    News    FMCAD'26: Scalable Equivalence Sweeping and Verified Distributed SAT

FMCAD'26: Scalable Equivalence Sweeping and Verified Distributed SAT

July 20, 2026

We are happy to announce that two of our works have been accepted for publication at the 2026 Formal Methods for Computer Aided Design (FMCAD), which will take place in September in Graz, Austria.

The paper Verified Real-time Proof Checking for Large-Scale SAT Solving (Yong Kiam Tan, Dominik Schreiber, Johannes Åman Pohjola, Magnus Myreen) introduces the first formally verified implementation of real-time proof checking for distributed clause-sharing SAT solvers, together with a soundness theorem for an abstract model of clause-sharing solving/checking. We experimentally show that our solving setup only incurs modest running time overhead (< 20%) over unverified real-time proof checking. As such, our work yields what can be considered the first scalable formally certified SAT solver (in terms of distributed UNSAT soundness) to date.

The paper Parallel SAT Sweeping on CNFs (Niccolò Rigi-Luperti, Armin Biere, Dominik Schreiber) presents a careful parallelization of SAT sweeping, i.e., detecting semantic literal equivalences in propositional satisfiability (SAT) instances, which is in particular an essential ingredient for determining whether two given combinational circuits are equivalent (Combinational Equivalence Checking, CEC). Our approach scales to hundreds of cores and thus substantially accelerates the equivalence sweeping process. We also demonstrate how this scalable sweeping can be integrated seamlessly in an existing massively parallel SAT solver as a means of scalable preprocessing for CEC inputs.