Title	SETH and Resolution
Creator	Bonacina, Ilario
Publisher	Banff International Research Station for Mathematical Innovation and Discovery
Date Issued	2020-01-23T09:31
Description	There are unsatisfiable $k$-CNF formulas in n variables such that each regular resolution refutation of those has size at least $2^{n(1 - c_k)}$ where where $c_k$ goes to 0 as $k$ goes to infinity. The problem of finding $k$-CNF formulas for which we can prove such strong size lower bounds in resolution (or stronger systems) is open. A lower bound of this form for resolution would imply that CDCL solvers cannot disprove the Strong Exponential Time Hypothesis. In this talk we give a simple proof of the result for regular resolution with the idea in mind to attack the problem for general resolution (or stronger systems). (Talk based on joint works with Navid Talebanfard)
Extent	26.0 minutes
Subject	Mathematics; Computer science; Mathematical logic and foundations; Theoretical computer science
Type	Moving Image
File Format	video/mp4
Language	eng
Notes	Author affiliation: UPC Universitat Politècnica de Catalunya
Series	BIRS Workshop Lecture Videos (Banff, Alta)
Date Available	2020-07-22
Provider	Vancouver : University of British Columbia Library
Rights	Attribution-NonCommercial-NoDerivatives 4.0 International
DOI	10.14288/1.0392487
URI	http://hdl.handle.net/2429/75235
Affiliation	Non UBC
Peer Review Status	Unreviewed
Scholarly Level	Postdoctoral
Rights URI	http://creativecommons.org/licenses/by-nc-nd/4.0/
Aggregated Source Repository	DSpace

Open Collections

BIRS Workshop Lecture Videos