Soundness of Inprocessing in Clause Sharing SAT Solvers

Norbert MantheyNorbert Manthey, Tobias PhilippTobias Philipp, Christoph WernhardChristoph Wernhard

Norbert Manthey, Tobias Philipp, Christoph Wernhard
Soundness of Inprocessing in Clause Sharing SAT Solvers
In Matti Järvisalo and Allen Van Gelder, eds., Theory and Applications of Satisfiability Testing, 16th International Conference, SAT 2013, volume 7962 of LNCS, 22-39, 2013. Springer

Details
Bibtex

KurzfassungAbstract
We present a formalism that models the computation of clause sharing portfolio solvers with inprocessing. The soundness of these solvers is not a straightforward property since shared clauses can make a formula unsatisfiable. Therefore, we develop characterizations of simplification techniques and suggest various settings how clause sharing and inprocessing can be combined. Our formalization models most of the recent implemented portfolio systems and we indicate possibilities to improve these. A particular improvement is a novel way to combine clause addition techniques – like blocked clause addition – with clause deletion techniques – like blocked clause elimination or variable elimination.
Bemerkung: Note: Received the SAT 2013 Best Paper Award
Forschungsgruppe:Research Group: WissensverarbeitungKnowledge Representation and Reasoning

The final publication is available at Springer.

@inproceedings{MPW2013,
  author    = {Norbert Manthey and Tobias Philipp and Christoph Wernhard},
  title     = {Soundness of Inprocessing in Clause Sharing {SAT} Solvers},
  editor    = {Matti J{\"{a}}rvisalo and Allen Van Gelder},
  booktitle = {Theory and Applications of Satisfiability Testing, 16th
               International Conference, {SAT} 2013},
  series    = {LNCS},
  volume    = {7962},
  publisher = {Springer},
  year      = {2013},
  pages     = {22-39}
}