Ábrahám, Erika; Schubert, Tobias; Becker, Bernd; Fränzle, Martin; Herde, Christian Parallel SAT solving in bounded model checking. (English) Zbl 1213.68359 J. Log. Comput. 21, No. 1, 5-21 (2011). Summary: 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. Cited in 3 Documents MSC: 68Q60 Specification and verification (program logics, model checking, etc.) 68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) Keywords:parallel programs; bounded model checking; SAT solving; linear programming; hybrid systems Software:MiniSat; MPI/MPICH; BerkMin; Chaff PDFBibTeX XMLCite \textit{E. Ábrahám} et al., J. Log. Comput. 21, No. 1, 5--21 (2011; Zbl 1213.68359) Full Text: DOI