Paper Info
Title
An Incremental Algorithm to Check Satisfiability for Bounded Model Checking
Abstract
In 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. Een and Sorensson [N. Een and N. Sorensson. 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.
Year
DOI
Venue
2005
10.1016/j.entcs.2004.06.062
Electronic Notes in Theoretical Computer Science (ENTCS)
Keywords
Field
DocType
n. een,hard problems. key words: bounded model checking,incremental algorithms.,incremental algorithms,especially for large,valid fall,sat-based bounded model checking,n. sorensson,conflict-learned clauses,propositional satisfiability,bounded model checking,bmc run,sat check,the proposed techniques,incremental sat,circus sat,sat instance,incremental algorithm,sat solver,satisfiability,profitability,search space
Discrete mathematics,Model checking,Computer science,Satisfiability,Boolean satisfiability problem,Remainder,Algorithm,Theoretical computer science,Counterexample,Syntax,Conflict analysis,Bounded function
Journal
Volume
Issue
ISSN
119
2
1571-0661
Citations 
PageRank 
References 
31
1.43
20
Authors
2
Name
Order
Citations
PageRank
HoonSang Jin124415.15
Fabio Somenzi23394302.47