Validating Unsatisfiability Results of Clause Sharing Parallel SAT Solvers

Marijn J.H. HeuleMarijn J.H. Heule, Norbert MantheyNorbert Manthey, Tobias PhilippTobias Philipp

Marijn J.H. Heule, Norbert Manthey, Tobias Philipp
Validating Unsatisfiability Results of Clause Sharing Parallel SAT Solvers
In Daniel Le Berre, eds., Pragmatics of SAT 2014, volume 27 of EPiC Series, 12-25, 2014. EasyChair

Details
Bibtex

KurzfassungAbstract
As satisfiability (SAT) solver performance has improved, so has their complexity, which make it more likely that SAT solvers contain bugs. One important source of increased complexity is clause sharing in parallel SAT solvers. SAT solvers can emit a proof of unsatisfiability to gain confidence that their results are correct. Such proofs must contain deletion information in order to check them efficiently. Computing deletion information is easy and cheap for parallel solvers without clause sharing, but tricky for parallel solvers with clause sharing. We present a method to generate unsatisfiability proofs from clause sharing parallel SAT solvers. We show that the overhead of our method is small and that the produced proofs can be validated in a time similar to the solving (CPU) time. However, proofs produced by parallel solvers without clause sharing can be checked in a time similar to the solving (wall-clock) time. This raises the question whether our method can be improved such that the checking time of proofs from parallel solvers without clause sharing is comparable to the time to check proofs from parallel solver with clause sharing.
Forschungsgruppe:Research Group: WissensverarbeitungKnowledge Representation and Reasoning

@inproceedings{HMP2014,
  author    = {Marijn {J.H.} Heule and Norbert Manthey and Tobias Philipp},
  title     = {Validating Unsatisfiability Results of Clause Sharing Parallel
               {SAT} Solvers},
  editor    = {Daniel Le Berre},
  booktitle = {Pragmatics of {SAT} 2014},
  series    = {EPiC Series},
  volume    = {27},
  publisher = {EasyChair},
  year      = {2014},
  pages     = {12-25}
}