State set management for SAT-based unbounded model checking

In recent years, Boolean satisfiability (SAT) has been shown to hold potential for unbounded model checking (UMC). The success of SAT-based UMC largely relies on (i) the SAT solver efficiency, (it) solution cube enlargement, and (Hi) state-set management. In this paper, we propose a simple, yet efficient, clause conversion technique to account for the state set obtained by SAT-based UMC. Our state set is stored in a zero-suppressed binary decision diagram (ZBDD), and the shared structures in the ZBDD are exploited to aggressively avoid repeated manipulation of common subsets in the state-set. The resulting number of clauses, generated for the state set, now depends on the number of nodes in the ZBDD, rather than the number of solutions found. We integrated the proposed techniques in an unbounded model checking framework that uses a pure SAT solver. The experimental results show that we can attain orders of magnitude improvement in both performance and capacity as compared to the existing techniques.