Formula Simplifications as DRAT Derivations

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche

Toggle side column

Formula Simplifications as DRAT Derivations

Norbert MantheyNorbert Manthey,  Tobias PhilippTobias Philipp
Formula Simplifications as DRAT Derivations


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
  • 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}
}