TY - JOUR
AU - Vinyals, Marc
PY - 2020/04/03
Y2 - 2023/05/29
TI - Hard Examples for Common Variable Decision Heuristics
JF - Proceedings of the AAAI Conference on Artificial Intelligence
JA - AAAI
VL - 34
IS - 02
SE - AAAI Technical Track: Constraint Satisfaction and Optimization
DO - 10.1609/aaai.v34i02.5527
UR - https://ojs.aaai.org/index.php/AAAI/article/view/5527
SP - 1652-1659
AB - <p>The CDCL algorithm for SAT is equivalent to the resolution proof system under a few assumptions, one of them being an optimal non-deterministic procedure for choosing the next variable to branch on. In practice this task is left to a variable decision heuristic, and since the so-called VSIDS decision heuristic is considered an integral part of CDCL, whether CDCL with a VSIDS-like heuristic is also equivalent to resolution remained a significant open question.</p><p>We give a negative answer by building a family of formulas that have resolution proofs of polynomial size but require exponential time to decide in CDCL with common heuristics such as VMTF, CHB, and certain implementations of VSIDS and LRB.</p>
ER -