Title	Introduction to Proof Complexity for SAT practitioner
Creator	Lauria, Massimo
Publisher	Banff International Research Station for Mathematical Innovation and Discovery
Date Issued	2018-08-27T10:11
Description	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 formula efficiently. 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.
Extent	63.0
Subject	Mathematics; Computer science; Mathematical logic and foundations; Theoretical computer science
Type	Moving Image
File Format	video/mp4
Language	eng
Notes	Author affiliation: Università degli studi di Roma - La Sapienza
Series	BIRS Workshop Lecture Videos (Oaxaca de Juárez (Mexico))
Date Available	2019-03-30
Provider	Vancouver : University of British Columbia Library
Rights	Attribution-NonCommercial-NoDerivatives 4.0 International
DOI	10.14288/1.0377690
URI	http://hdl.handle.net/2429/69356
Affiliation	Non UBC
Peer Review Status	Unreviewed
Scholarly Level	Researcher
Rights URI	http://creativecommons.org/licenses/by-nc-nd/4.0/
Aggregated Source Repository	DSpace

Open Collections

BIRS Workshop Lecture Videos

Introduction to Proof Complexity for SAT practitioner Lauria, Massimo

Description

Item Metadata

Item Media

Item Citations and Data

Rights