A (biased) proof complexity survey for SAT practitioners

Research output: Chapter in Book/Report/Conference proceedingPaper in conference 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.

Details

Authors
External organisations
  • KTH Royal Institute of Technology
Research areas and keywords

Subject classification (UKÄ) – MANDATORY

  • Computer Science
Original languageEnglish
Title of host publicationTheory and Applications of Satisfiability Testing, SAT 2014
Subtitle of host publication17th International Conference, Held as Part of theVienna Summer of Logic, VSL 2014, Proceedings
PublisherSpringer
Pages1-6
Number of pages6
ISBN (Print)9783319092836
Publication statusPublished - 2014
Publication categoryResearch
Peer-reviewedYes
Externally publishedYes
Event17th International Conference on Theory and Applications of Satisfiability Testing, SAT 2014, Held as Part of the Vienna Summer of Logic, VSL 2014 - Vienna, Austria
Duration: 2014 Jul 142014 Jul 17

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume8561
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference17th International Conference on Theory and Applications of Satisfiability Testing, SAT 2014, Held as Part of the Vienna Summer of Logic, VSL 2014
CountryAustria
CityVienna
Period2014/07/142014/07/17