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?
Not a direct answer to the question but, as DPLL can be seen as a special case of CDCL, hopefully of interest.

The problem of finding optimal branching literals for DPLL is (in a way) harder than SAT itself: the paper "On the complexity of choosing
the branching literal in DPLL" by Liberatore shows that 
choosing optimal branching literals in DPLL  is both NP-hard and coNP-hard.