Speculative SAT Modulo SAT

TL;DR

This paper introduces SPEC SMS, a bi-directional extension of SAT modulo SAT, allowing multiple modules to speculate decisions, leading to exponential performance improvements in challenging model checking benchmarks.

Contribution

The paper proposes SPEC SMS, a novel bi-directional SAT modulo SAT approach that enhances modular solving by enabling speculative decisions across modules.

Findings

SPEC SMS outperforms traditional SMS on hard benchmarks

Exponential performance improvements observed in experiments

Extended proofs and interpolation support model checking applications

Abstract

State-of-the-art model-checking algorithms like IC3/PDR are based on uni-directional modular SAT solving for finding and/or blocking counterexamples. Modular SAT solvers divide a SAT-query into multiple sub-queries, each solved by a separate SAT solver (called a module), and propagate information (lemmas, proof obligations, blocked clauses, etc.) between modules. While modular solving is key to IC3/PDR, it is obviously not as effective as monolithic solving, especially when individual sub-queries are harder to solve than the combined query. This is partially addressed in SAT modulo SAT (SMS) by propagating unit literals back and forth between the modules and using information from one module to simplify the sub-query in another module as soon as possible (i.e., before the satisfiability of any sub-query is established). However, bi-directionality of SMS is limited because of the strict order between decisions and propagation -- only one module is allowed to make decisions, until its sub-query is SAT. In this paper, we propose a generalization of SMS, called SPEC SMS, that speculates decisions between modules. This makes it bi-directional -- decisions are made in multiple modules, and learned clauses are exchanged in both directions. We further extend DRUP proofs and interpolation, these are useful in model checking, to SPEC SMS. We have implemented SPEC SMS in Z3 and show that it performs exponentially better on a series of benchmarks that are provably hard for SMS.