A (biased) proof complexity survey for SAT practitioners

Jakob Nordström

doi:10.1007/978-3-319-09284-3_1

A (biased) proof complexity survey for SAT practitioners

Jakob Nordström

KTH Royal Institute of Technology

Research output: Chapter in Book/Report/Conference proceeding › Paper in conference proceeding › peer-review

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.

Original language	English
Title of host publication	Theory and Applications of Satisfiability Testing, SAT 2014
Subtitle of host publication	17th International Conference, Held as Part of theVienna Summer of Logic, VSL 2014, Proceedings
Publisher	Springer
Pages	1-6
Number of pages	6
ISBN (Print)	9783319092836
DOIs	https://doi.org/10.1007/978-3-319-09284-3_1
Publication status	Published - 2014
Externally published	Yes
Event	17th 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 14 → 2014 Jul 17

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	8561
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	17th International Conference on Theory and Applications of Satisfiability Testing, SAT 2014, Held as Part of the Vienna Summer of Logic, VSL 2014
Country/Territory	Austria
City	Vienna
Period	2014/07/14 → 2014/07/17

Subject classification (UKÄ)

Computer Science

Access to Document

10.1007/978-3-319-09284-3_1

Cite this

@inproceedings{ebc4e2839f4e4b7589a7c83c59a194d0,

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, Gr{\"o}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.",

author = "Jakob Nordstr{\"o}m",

year = "2014",

doi = "10.1007/978-3-319-09284-3_1",

language = "English",

isbn = "9783319092836",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "1--6",

booktitle = "Theory and Applications of Satisfiability Testing, SAT 2014",

address = "Germany",

note = "17th International Conference on Theory and Applications of Satisfiability Testing, SAT 2014, Held as Part of the Vienna Summer of Logic, VSL 2014 ; Conference date: 14-07-2014 Through 17-07-2014",

}

Nordström, J 2014, A (biased) proof complexity survey for SAT practitioners. in Theory and Applications of Satisfiability Testing, SAT 2014: 17th International Conference, Held as Part of theVienna Summer of Logic, VSL 2014, Proceedings. Lecture Notes in Computer Science, vol. 8561, Springer, pp. 1-6, 17th International Conference on Theory and Applications of Satisfiability Testing, SAT 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, 2014/07/14. https://doi.org/10.1007/978-3-319-09284-3_1

A (biased) proof complexity survey for SAT practitioners. / Nordström, Jakob.
Theory and Applications of Satisfiability Testing, SAT 2014: 17th International Conference, Held as Part of theVienna Summer of Logic, VSL 2014, Proceedings. Springer, 2014. p. 1-6 (Lecture Notes in Computer Science; Vol. 8561).

Research output: Chapter in Book/Report/Conference proceeding › Paper in conference proceeding › peer-review

TY - GEN

T1 - A (biased) proof complexity survey for SAT practitioners

AU - Nordström, Jakob

PY - 2014

Y1 - 2014

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-319-09284-3_1

DO - 10.1007/978-3-319-09284-3_1

M3 - Paper in conference proceeding

AN - SCOPUS:84958536048

SN - 9783319092836

T3 - Lecture Notes in Computer Science

SP - 1

EP - 6

BT - Theory and Applications of Satisfiability Testing, SAT 2014

PB - Springer

T2 - 17th International Conference on Theory and Applications of Satisfiability Testing, SAT 2014, Held as Part of the Vienna Summer of Logic, VSL 2014

Y2 - 14 July 2014 through 17 July 2014

ER -

A (biased) proof complexity survey for SAT practitioners

Abstract

Publication series

Conference

Subject classification (UKÄ)

Access to Document

Fingerprint

Cite this