Formula Simplifications as DRAT Derivations

Norbert MantheyNorbert Manthey, Tobias PhilippTobias Philipp

Norbert Manthey, Tobias Philipp
Formula Simplifications as DRAT Derivations
In Carsten Lutz and Michael Tielscher, eds., KI 2014: Advances in Artificial Intelligence, volume 8736 of Lecture Notes in Computer Science, 111-122, 2014. Springer

Details
Bibtex

KurzfassungAbstract
Many real world problems are solved with satisfiability testing (SAT). However, SAT solvers have documented bugs and therefore the answer that a formula is unsatisfiable can be incorrect. Certifying algorithms are an attractive approach to increase the reliability of SAT solvers. For unsatisfiable formulas an unsatisfiability proof has to be created. This paper presents certificate constructions for various formula simplification techniques, which are crucial to the success of modern SAT solvers
Forschungsgruppe:Research Group: WissensverarbeitungKnowledge Representation and Reasoning

The final publication is available at Springer.

@inproceedings{MP2014,
  author    = {Norbert Manthey and Tobias Philipp},
  title     = {Formula Simplifications as {DRAT} Derivations},
  editor    = {Carsten Lutz and Michael Tielscher},
  booktitle = {KI 2014: Advances in Artificial Intelligence},
  series    = {Lecture Notes in Computer Science},
  volume    = {8736},
  publisher = {Springer},
  year      = {2014},
  pages     = {111-122}
}