Title	Automating Resolution is NP-Hard
Creator	Atserias, Albert
Publisher	Banff International Research Station for Mathematical Innovation and Discovery
Date Issued	2020-01-22T09:55
Description	We show that it is NP-hard to distinguish formulas that have Resolution refutations of almost linear length from formulas that do not even have weakly exponentially long ones. It follows from this that Resolution is not automatable in polynomial time unless P = NP, or in weakly exponential time unless ETH fails. In the talk I will try to explain the process of discovery that led us to the result.
Extent	50.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: Universitat Politecnica de Catalunya
Series	BIRS Workshop Lecture Videos (Banff, Alta)
Date Available	2020-07-21
Provider	Vancouver : University of British Columbia Library
Rights	Attribution-NonCommercial-NoDerivatives 4.0 International
DOI	10.14288/1.0392479
URI	http://hdl.handle.net/2429/75226
Affiliation	Non UBC
Peer Review Status	Unreviewed
Scholarly Level	Faculty
Rights URI	http://creativecommons.org/licenses/by-nc-nd/4.0/
Aggregated Source Repository	DSpace

Open Collections

BIRS Workshop Lecture Videos