{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,20]],"date-time":"2026-07-20T19:06:20Z","timestamp":1784574380196,"version":"3.55.0"},"reference-count":0,"publisher":"IOS Press","isbn-type":[{"value":"9781643681603","type":"print"},{"value":"9781643681610","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021,2,2]]},"abstract":"<jats:p>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\u00f6bner 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.<\/jats:p>","DOI":"10.3233\/faia200990","type":"book-chapter","created":{"date-parts":[[2021,2,8]],"date-time":"2021-02-08T08:41:42Z","timestamp":1612773702000},"source":"Crossref","is-referenced-by-count":16,"title":["Chapter 7. Proof Complexity and SAT Solving"],"prefix":"10.3233","author":[{"given":"Sam","family":"Buss","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jakob","family":"Nordstr\u00f6m","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"7437","container-title":["Frontiers in Artificial Intelligence and Applications","Handbook of Satisfiability"],"original-title":[],"link":[{"URL":"http:\/\/ebooks.iospress.nl\/pdf\/doi\/10.3233\/FAIA200990","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,2,8]],"date-time":"2021-02-08T08:41:43Z","timestamp":1612773703000},"score":1,"resource":{"primary":{"URL":"http:\/\/ebooks.iospress.nl\/doi\/10.3233\/FAIA200990"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,2,2]]},"ISBN":["9781643681603","9781643681610"],"references-count":0,"URL":"https:\/\/doi.org\/10.3233\/faia200990","relation":{},"ISSN":["0922-6389","1879-8314"],"issn-type":[{"value":"0922-6389","type":"print"},{"value":"1879-8314","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,2,2]]}}}