A (Biased) Proof Complexity Survey for SAT Practitioners
2014 (English)In: THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2014, 2014, 1-6 p.Conference paper (Refereed)
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, Grobner 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.
Place, publisher, year, edition, pages
2014. 1-6 p.
, Lecture Notes in Computer Science, ISSN 0302-9743 ; 8561
IdentifiersURN: urn:nbn:se:kth:diva-158358DOI: 10.1007/978-3-319-09284-3-1ISI: 000345595300001ScopusID: 2-s2.0-84958536048ISBN: 978-3-319-09284-3; 978-3-319-09283-6OAI: oai:DiVA.org:kth-158358DiVA: diva2:782274
17th International Conference on Theory and Applications of Satisfiability Testing (SAT) Held as Part of the Federated Logic Conference (FLoC) / Vienna Summer of Logic (VSL) Conference, JUL 09-24, 2014, Vienna, AUSTRIA
QC 201501202015-01-202015-01-072015-01-20Bibliographically approved