Hard Examples for Common Variable Decision Heuristics

Authors

  • Marc Vinyals Technion

DOI:

https://doi.org/10.1609/aaai.v34i02.5527

Abstract

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.

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.

Downloads

Published

2020-04-03

How to Cite

Vinyals, M. (2020). Hard Examples for Common Variable Decision Heuristics. Proceedings of the AAAI Conference on Artificial Intelligence, 34(02), 1652-1659. https://doi.org/10.1609/aaai.v34i02.5527

Issue

Section

AAAI Technical Track: Constraint Satisfaction and Optimization