If a CDCL SAT solver only selects negative literals as decision literals (but can set positive literals through unit propogation) but has a perfect heuristic for determining which literal to select next, what kind of claims can be made about its running time?
Is it necessarily exponential on some infinite class of satisfiable instances?