BIRS Workshop Lecture Videos
Introduction to Proof Complexity for SAT practitioner Lauria, Massimo
Running a SAT solver on an UNSAT formula produces (implicitly or
explicitly) a proof that the formula is unsatisfiable, usually
expressible in an established formal language called proof system.
This observation leads to study SAT solving methods by looking at the
generated proofs. I.e., if an UNSAT formula has no short proof in a
given proof system, the corresponding SAT solvers cannot solve the
We introduce the area and the methods of proof complexity, that studies the length and the structure of proofs of UNSAT. In particular we define and discuss Resolution, Polynomial Calculus, Cutting Planes and Extended Resolution, which are the most relevant proof systems for current SAT solver technology.
Since a SAT solver goal is, among other things, to look for proofs as short as possible, we briefly discuss the complexity of efficiently finding such short proofs.
Item Citations and Data
Attribution-NonCommercial-NoDerivatives 4.0 International