Title	Hard Examples for Common Variable Decision Heuristics
Creator	Vinyals, Marc
Publisher	Banff International Research Station for Mathematical Innovation and Discovery
Date Issued	2020-01-24T09:34
Description	The CDCL algorithm, which is nowadays the top-performing algorithm to solve SAT in practice, is polynomially equivalent to resolution when we view it as a proof system, that is we replace some of its heuristics by nondeterministic choices. In this talk we show that this is no longer true if we leave the heuristics in place; more precisely we build a family of formulas that have resolution proofs of polynomial size but require exponential time to decide in CDCL with a class of variable decision heuristics that includes the most common heuristics such as VSIDS.
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: Technion
Series	BIRS Workshop Lecture Videos (Banff, Alta)
Date Available	2020-07-23
Provider	Vancouver : University of British Columbia Library
Rights	Attribution-NonCommercial-NoDerivatives 4.0 International
DOI	10.14288/1.0392499
URI	http://hdl.handle.net/2429/75252
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