Proof Complexity and SAT Solving
Research output: Chapter in Book/Report/Conference proceeding › Book chapter › Research › peer-review
Standard
Proof Complexity and SAT Solving. / Buss, Sam; Nordström, Jakob.
Handbook of Satisfiability. ed. / Armin Biere; Marijn J. H. Heule; Hans van Maaren; Toby Walsh. 2. ed. IMIA and IOS Press, 2021. p. 233 - 350 (Frontiers in Artificial Intelligence and Applications, Vol. 336).Research output: Chapter in Book/Report/Conference proceeding › Book chapter › Research › peer-review
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - CHAP
T1 - Proof Complexity and SAT Solving
AU - Buss, Sam
AU - Nordström, Jakob
N1 - Chapter to appear in the 2nd edition. Draft version available at http://www.csc.kth.se/~jakobn/research/ProofComplexityChapter.pdf
PY - 2021
Y1 - 2021
N2 - This chapter gives an overview of proof complexity and connections to SAT solving, focusing on proof systems such as resolution, Nullstellensatz, polynomial calculus, and cutting planes (corresponding to conflict-driven clause learning, algebraic approaches using linear algebra or Gröbner bases, and pseudo-Boolean solving, respectively). There is also a discussion of extended resolution (which is closely related to DRAT proof logging) and Frege and extended Frege systems more generally. An ample supply of references for further reading is provided, including for some topics omitted in this chapter.
AB - This chapter gives an overview of proof complexity and connections to SAT solving, focusing on proof systems such as resolution, Nullstellensatz, polynomial calculus, and cutting planes (corresponding to conflict-driven clause learning, algebraic approaches using linear algebra or Gröbner bases, and pseudo-Boolean solving, respectively). There is also a discussion of extended resolution (which is closely related to DRAT proof logging) and Frege and extended Frege systems more generally. An ample supply of references for further reading is provided, including for some topics omitted in this chapter.
U2 - 10.3233/FAIA200990
DO - 10.3233/FAIA200990
M3 - Book chapter
SN - 978-1-64368-160-3
T3 - Frontiers in Artificial Intelligence and Applications
SP - 233
EP - 350
BT - Handbook of Satisfiability
A2 - Biere, Armin
A2 - Heule, Marijn J. H.
A2 - van Maaren, Hans
A2 - Walsh, Toby
PB - IMIA and IOS Press
ER -
ID: 251872222