BIRS Workshop Lecture Videos
Hard Examples for Common Variable Decision Heuristics Vinyals, Marc
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.
Item Citations and Data
Attribution-NonCommercial-NoDerivatives 4.0 International