PaSAT — Parallel SAT-Checking with Lemma Exchange: Implementation and Applications

We present PaSAT, a parallel implementation of a Davis-Putnam-style prepositional satisfiability checker incorporating dynamic search space partitioning, intelligent backjumping, as well as lemma generation and exchange; the main focus of our implementation is on speeding up SAT-checking of prepositional encodings of real-world combinatorial problems. We investigate and analyze the speed-ups obtained by parallelization in conjunction with lemma exchange and describe the effects we observed during our experiments. Finally, we present performance measurements from the application of our prover in the areas of formal consistency checking of industrial product documentation, cryptanalysis, and hardware verification. ld like to thank Jürgen Ellinger for help on carrying out the experiments.