# Asymptotic complexity of CDCL SAT solver that only selects negative literals

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?

• What do you mean by selecting only negative literals? All variables must occur both positively and negatively in the instance, otherwise you could apply the pure literal rule and remove all clauses containing that variable from the instance. – Kyle Jones Jul 20 '16 at 4:06
• The negative literal thing refers to the solver, not the instance. The solver only SELECTS negative literals, but it can set positive literals through unit propogation. – dspyz Jul 20 '16 at 4:12
• I should clarify that by "select" I mean as decision literals. Done. – dspyz Jul 20 '16 at 4:13
• Oh, I found it. It's "Towards Ultra Rapid Restarts" Shai Haim, Marijn Heule in the section about direction heuristics. They mention that MiniSat does this. – dspyz Jul 20 '16 at 5:07
• @dspyz The title suggests that you want the best case asymptotic complexity, which is probably $O(n)$. The discussion suggests that you are actually looking for the worst case asymptotic complexity, given an oracle for optimal negative literal as branching literal. Could you please clarify? – Martin Berger Jul 20 '16 at 8:02