Verified Real-time Proof Checking for Large-Scale SAT Solving

Abstract

Parallel and distributed propositional satisfiability (SAT) solvers based on clause sharing can serve as powerful tools for solving challenging automated reasoning problems. Real-time proof checking can be used to gain confidence in results obtained from clause-sharing solving without constructing an (often impractically large) explicit proof. In this work, we present the first 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.