Skip to main content

Lund University Publications

LUND UNIVERSITY LIBRARIES

A (biased) proof complexity survey for SAT practitioners

Nordström, Jakob LU (2014) 17th International Conference on Theory and Applications of Satisfiability Testing, SAT 2014, Held as Part of the Vienna Summer of Logic, VSL 2014 In Lecture Notes in Computer Science 8561. p.1-6
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.

Please use this url to cite or link to this publication:
author
publishing date
type
Chapter in Book/Report/Conference proceeding
publication status
published
subject
host publication
Theory and Applications of Satisfiability Testing, SAT 2014 : 17th International Conference, Held as Part of theVienna Summer of Logic, VSL 2014, Proceedings - 17th International Conference, Held as Part of theVienna Summer of Logic, VSL 2014, Proceedings
series title
Lecture Notes in Computer Science
volume
8561
pages
6 pages
publisher
Springer
conference name
17th International Conference on Theory and Applications of Satisfiability Testing, SAT 2014, Held as Part of the Vienna Summer of Logic, VSL 2014
conference location
Vienna, Austria
conference dates
2014-07-14 - 2014-07-17
external identifiers
  • scopus:84958536048
ISSN
1611-3349
0302-9743
ISBN
9783319092836
DOI
10.1007/978-3-319-09284-3_1
language
English
LU publication?
no
id
ebc4e283-9f4e-4b75-89a7-c83c59a194d0
date added to LUP
2020-12-18 22:24:38
date last changed
2024-01-03 01:37:43
@inproceedings{ebc4e283-9f4e-4b75-89a7-c83c59a194d0,
  abstract     = {{<p>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.</p>}},
  author       = {{Nordström, Jakob}},
  booktitle    = {{Theory and Applications of Satisfiability Testing, SAT 2014 : 17th International Conference, Held as Part of theVienna Summer of Logic, VSL 2014, Proceedings}},
  isbn         = {{9783319092836}},
  issn         = {{1611-3349}},
  language     = {{eng}},
  pages        = {{1--6}},
  publisher    = {{Springer}},
  series       = {{Lecture Notes in Computer Science}},
  title        = {{A (biased) proof complexity survey for SAT practitioners}},
  url          = {{http://dx.doi.org/10.1007/978-3-319-09284-3_1}},
  doi          = {{10.1007/978-3-319-09284-3_1}},
  volume       = {{8561}},
  year         = {{2014}},
}