An Incremental Algorithm to Check Satisfiability for Bounded Model Checking

AbstractIn Bounded Model Checking (BMC), the search for counterexamples of increasing lengths is translated into a sequence of satisfiability (SAT) checks. It is natural to try to exploit the similarity of these SAT instances by forwarding clauses learned during conflict analysis from one instance to the next. The methods proposed to identify clauses that remain valid fall into two categories: Those that are oblivious to the mechanism that generates the sequence of SAT instances and those that rely on it. In the case of a BMC run, it was observed by Strichman [O. Shtrichman. Pruning techniques for the SAT-based bounded model checking problem. In Correct Hardware Design and Verification Methods (CHARME 2001), pages 58–70, Livingston, Scotland, Sept. 2001. Springer. LNCS 2144] that those clauses learned during one SAT check that only depend on the structure of the model remain valid when checking for longer counterexamples. Eén and Sörensson [N. Eén and N. Sörensson. Temporal induction by incremental SAT solving. Electronic Notes in Theoretical Computer Science, 89(4), 2003. First International Workshop on Bounded Model Checking. http://www.elsevier.nl/locate/entcs/] pointed out that all learned clauses can be forwarded if the translation into SAT obeys commonly followed rules. Many clauses that are forwarded this way, however, are of little usefulness and may degrade performance. This paper presents an extension to Strichman's approach in the form of a more general criterion to filter conflict clauses that can be profitably forwarded to successive instances. This criterion, in particular, is still syntactic and quite efficient, but accounts for the presence of both primary and auxiliary objectives in the SAT instance. This paper also introduces a technique to distill clauses to be forwarded even though they fail the syntactic check. Distillation is a semantic approach that can be applied in general to incremental SAT, and often produces clauses that are independent of the primary objective, and hence remain valid for the remainder of the sequence of instances. In addition, distillation often improves the quality of the clauses, that is, their ability to prevent the examination of large regions of the search space. Experimental results obtained with the CirCUs SAT solver confirm the efficacy of the proposed techniques, especially for large, hard problems