Title
A (Biased) Proof Complexity Survey for SAT Practitioners.
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, 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.
Year
DOI
Venue
2014
10.1007/978-3-319-09284-3_1
Lecture Notes in Computer Science
Keywords
Field
DocType
computer science
Probabilistically checkable proof,Discrete mathematics,Computer-assisted proof,Computer science,Boolean satisfiability problem,Conjunctive normal form,Polynomial calculus,Proof complexity,Gröbner basis,Computation
Conference
Volume
ISSN
Citations 
8561
0302-9743
3
PageRank 
References 
Authors
0.37
30
1
Name
Order
Citations
PageRank
Jakob Nordström117721.76