A (biased) proof complexity survey for SAT practitioners

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

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.

Original languageEnglish
Title of host publicationTheory and Applications of Satisfiability Testing, SAT 2014 - 17th International Conference, Held as Part of theVienna Summer of Logic, VSL 2014, Proceedings
Number of pages6
PublisherSpringer Verlag,
Publication date2014
Pages1-6
ISBN (Print)9783319092836
DOIs
Publication statusPublished - 2014
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: 14 Jul 201417 Jul 2014

Conference

Conference17th International Conference on Theory and Applications of Satisfiability Testing, SAT 2014, Held as Part of the Vienna Summer of Logic, VSL 2014
LandAustria
ByVienna
Periode14/07/201417/07/2014
Sponsor17th International Conference on Theory and, Applications of Satisfiability Testing, SAT 2014,, Held as Part of the Vienna Summer of Logic, VSL 2014
SeriesLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8561 LNCS
ISSN0302-9743

ID: 251869794