Proof Complexity and SAT Solving

Publikation: Bidrag til bog/antologi/rapport › Bidrag til bog/antologi › Forskning › fagfællebedømt

Standard

Proof Complexity and SAT Solving. / Buss, Sam; Nordström, Jakob.

Handbook of Satisfiability. red. / Armin Biere; Marijn J. H. Heule; Hans van Maaren; Toby Walsh. 2. udg. IMIA and IOS Press, 2021. s. 233 - 350 (Frontiers in Artificial Intelligence and Applications, Bind 336).

Publikation: Bidrag til bog/antologi/rapport › Bidrag til bog/antologi › Forskning › fagfællebedømt

Harvard

Buss, S & Nordström, J 2021, Proof Complexity and SAT Solving. i A Biere, MJH Heule, H van Maaren & T Walsh (red), Handbook of Satisfiability. 2 udg, IMIA and IOS Press, Frontiers in Artificial Intelligence and Applications, bind 336, s. 233 - 350. https://doi.org/10.3233/FAIA200990

APA

Buss, S., & Nordström, J. (2021). Proof Complexity and SAT Solving. I A. Biere, M. J. H. Heule, H. van Maaren, & T. Walsh (red.), Handbook of Satisfiability (2 udg., s. 233 - 350). IMIA and IOS Press. Frontiers in Artificial Intelligence and Applications Bind 336 https://doi.org/10.3233/FAIA200990

Vancouver

Buss S, Nordström J. Proof Complexity and SAT Solving. I Biere A, Heule MJH, van Maaren H, Walsh T, red., Handbook of Satisfiability. 2 udg. IMIA and IOS Press. 2021. s. 233 - 350. (Frontiers in Artificial Intelligence and Applications, Bind 336). https://doi.org/10.3233/FAIA200990

Author

Buss, Sam ; Nordström, Jakob. / Proof Complexity and SAT Solving. Handbook of Satisfiability. red. / Armin Biere ; Marijn J. H. Heule ; Hans van Maaren ; Toby Walsh. 2. udg. IMIA and IOS Press, 2021. s. 233 - 350 (Frontiers in Artificial Intelligence and Applications, Bind 336).

Bibtex

@inbook{9b99fba0bf964c5d9730dcab35822e2b,
title = "Proof Complexity and SAT Solving",
abstract = "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{\"o}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.",
author = "Sam Buss and Jakob Nordstr{\"o}m",
note = "Chapter to appear in the 2nd edition. Draft version available at http://www.csc.kth.se/~jakobn/research/ProofComplexityChapter.pdf",
year = "2021",
doi = "10.3233/FAIA200990",
language = "English",
isbn = "978-1-64368-160-3",
series = "Frontiers in Artificial Intelligence and Applications",
publisher = "IMIA and IOS Press",
pages = "233 -- 350",
editor = "Armin Biere and Heule, {Marijn J. H.} and {van Maaren}, Hans and Toby Walsh",
booktitle = "Handbook of Satisfiability",
edition = "2",

}

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