Deep integration of SAT solving and model checking

Once just considered the archetypal intractable problem, Boolean satisfiability (SAT) has flourished into one of the most effective tools for automated reasoning. One of its most successful applications is model checking, where SAT solvers are used to verify the correctness of systems by checking whether certain properties hold. This thesis investigates how to deepen the integration between SAT solving and model checking to improve performance and increase trust in the results.
We begin by presenting the state-of-the-art incremental SAT solver CaDiCaL 2.0. We extend its assumption-based interface with clause assumptions, and demonstrate how this enhancement accelerates IC3-based model checking. Building on CaDiCaL, we introduce a new backbone extraction tool, CadiBack. A formula’s backbone—the set of literals true in every satisfying assignment—can benefit various SAT-based applications, including verification, state space approximation, and fault localization. As part of this work, we present a polynomial-time backbone extraction algorithm and evaluate it as a preprocessor for CadiBack. Additionally, we formalize ternary simulation through the lens of abstract interpretation and propose a technique to improve accuracy using backbone extraction.
We then address how to achieve a similar level of trust in model checking as is commonly vested in SAT solvers. To this end, we develop a certification approach for hardware model checking. Specifically, we present certificate constructions for the preprocessing techniques of phase abstraction and constraint extraction. Our efforts culminate in the Hardware Model Checking Competition 2024, which marks the introduction of mandatory certificates for all participating tools. The results convincingly show the practical efficiency and effectiveness of our approach.
Finally, this thesis further explores competitions as a scientific method for advancing solver technology. Drawing on the author’s experience co-organizing several SAT and hardware model checking competitions, we examine what insights into solver innovation can be gained from these events.