On Incremental Satisability and Bounded Model Checking

Design and Implementation of Formal Tools and Systems 2011.

计算机科学;

Siert Wieringa

Others  :  http://ceur-ws.org/Vol-832/paper_4.pdf
PID  :  33669

学科分类：计算机科学（综合）

来源: CEUR

【 摘 要 】

Bounded Model Checking (BMC) is a symbolic model checking technique in which the existence of a counterexample of a bounded length is represented by the satisfiability of a propositional logic formula. Although solving a single instance of the satisfiability problem (SAT) is suffcient to decide on the existence of a counterexample for any arbitrary bound typically one starts from bound zero and solves the sequence of formulas for all consecutive bounds until a satisfiable formula is found. This is especially effcient in the presence of incremental SAT-solvers, which solve sequences of incrementally encoded formulas. In this article we analyze empirical results that demonstrate the difference in run time behavior between incremental and non-incremental SAT-solvers. We show a relation between the observed run time behavior and the way in which the activity of variables inside the solver propagates across bounds. This observation has not been previously presented and is particularly useful for designing solving strategies for parallelized model checkers.