Parallel SAT Solving in Bounded Model Checking

 

Erika Ábrahám

 

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.