A (biased) proof complexity survey for SAT practitioners

Forskningsoutput: Kapitel i bok/rapport/Conference proceedingKonferenspaper i proceeding

Abstract

This talk is intended as a selective survey of proof complexity, focusing on some comparatively weak proof systems that are of particular interest in connection with SAT solving. We will review resolution, polynomial calculus, and cutting planes (related to conflict-driven clause learning, Gröbner basis computations, and pseudo-Boolean solvers, respectively) and some proof complexity measures that have been studied for these proof systems. We will also briefly discuss if and how these proof complexity measures could provide insights into SAT solver performance.

Detaljer

Författare
Externa organisationer
  • KTH Royal Institute of Technology
Forskningsområden

Ämnesklassifikation (UKÄ) – OBLIGATORISK

  • Datavetenskap (datalogi)
Originalspråkengelska
Titel på värdpublikationTheory and Applications of Satisfiability Testing, SAT 2014
Undertitel på gästpublikation17th International Conference, Held as Part of theVienna Summer of Logic, VSL 2014, Proceedings
FörlagSpringer
Sidor1-6
Antal sidor6
ISBN (tryckt)9783319092836
StatusPublished - 2014
PublikationskategoriForskning
Peer review utfördJa
Externt publiceradJa
Evenemang17th International Conference on Theory and Applications of Satisfiability Testing, SAT 2014, Held as Part of the Vienna Summer of Logic, VSL 2014 - Vienna, Österrike
Varaktighet: 2014 jul 142014 jul 17

Publikationsserier

NamnLecture Notes in Computer Science
FörlagSpringer
Volym8561
ISSN (tryckt)0302-9743
ISSN (elektroniskt)1611-3349

Konferens

Konferens17th International Conference on Theory and Applications of Satisfiability Testing, SAT 2014, Held as Part of the Vienna Summer of Logic, VSL 2014
LandÖsterrike
OrtVienna
Period2014/07/142014/07/17