Parallel SAT Solving in Bounded Model Checking

ERIKA ÁBRAHÁM
TOBIAS SCHUBERT and BERND BECKER
MARTIN FRÄNZLE and CHRISTIAN HERDE

Abstract
Bounded model checking (BMC) is an incremental refutation technique to search for counterexamples of increasing length. The existence of a counterexample of a fixed length is expressed by a first-order logic formula that is checked for satisfiability using a suitable solver. We apply communicating parallel solvers to check satisfiability of the BMC formulae. In contrast to other parallel solving techniques, our method does not parallelize the satisfiability check of a single formula, but the parallel solvers work on formulae for different counterexample lengths.We adapt the method of constraint sharing and replication of Shtrichman, originally developed for sequential BMC, to the parallel setting. Since the learning mechanism is now parallelized, it is not obvious whether there is a benefit from the concepts of Shtrichman in the parallel setting.We demonstrate on a number of benchmarks that adequate communication between the parallel solvers yields the desired results.

Keywords: Parallel programs, bounded model checking, SAT solving, linear programming, hybrid systems.

Journal of Logic and Computation
http://logcom.oxfordjournals.org/cgi/reprint/exp002v1.pdf


(...)
For discrete systems a SAT solver is used, while the analysis of linear hybrid automata, for example, requires the application of a combined SAT-LP solver. Some popular solvers are, e.g. zChaff [21], BerkMin [14], MiniSAT [12],
HySat [13], MathSAT [4], CVCLite [5] and ICS [9].
(...)
2 Bounded model checking
We first give a short review of BMC [7, 15] and briefly describe how state-of-the-art SAT solvers
check satisfiability of propositional formulae. In this article we restrict ourselves to safety properties;
for lifeness properties see e.g. [7].
(...)
2.2 Satisfiability checking
The formulae ϕk describing counterexamples of length k are checked for satisfiability by a traditional
SAT solver.
First, the Boolean formula is transformed into a conjunctive normal form (CNF). In order to
keep the formula as small as possible, auxiliary Boolean variables are used to build the CNF
[26]. A formula in CNF form is a conjunction of clauses, while each clause is the disjunction of
literals.We distinguish between positive literals being Boolean variables, and negative literals being
negated ones.
In order to satisfy the formula, each of the clauses must be satisfied, i.e. at least one literal in each
clause must be true. The SAT solver assigns values to the variables in an iterative manner. After each
decision, i.e. free choice of an assignment, the solver propagates the assignment by searching for
unit clauses, i.e. clauses in that all literals but one are already false; the remaining literal is implied
to be true, since otherwise the clause would not be satisfied.
If two unit clauses imply different values for the same variable, a conflict occurs. In this case
a conflict analysis can take place which results in non-chronological backtracking and conflict
learning [20, 28]. Intuitively, the solver applies resolution to some unit clauses, using the implication
tree, and inserts a new conflict clause thereby strengthening the problem constraints and restricting
the state space for further search.
(...)

3 Parallel BMC
(...)
4 Experimental results
We implemented a prototype SAT solver that works mainly as described in Section 2.2. For
communication we use MPICH2 [16], an implementation of the message passing interface (MPI)
standard.
(...)
5 Conclusions
In this article we introduced a parallel SAT-solving technique for BMC.The parallelization is different
from existing approaches: instead of solving a single problem instance using parallel solvers, we let
different solvers solve different BMC instances. In order to speed up the search, we apply CSR and
let the solvers communicate the conflict clauses found during their SAT-checks. The experiments
performed show that the positive effect of CSR can only be preserved under parallelization if the
solvers communicate the conflict clauses among themselves.With communication, the full advantage
of sequential CSR can be maintained in the concurrent setting, yielding nearly linear speedup from
parallelization.
(...)
[26] G. Tseitin. On the complexity of derivations in propositional calculus. In Studies in Constructive
Mathematics and Mathematical Logics, Slisenko ed., pp. 115–125. Springer, Berlin, 1970.
(...)