4
$\begingroup$

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?

Improve this question
$\endgroup$
14
  • $\begingroup$ 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. $\endgroup$ – Kyle Jones Jul 20 '16 at 4:06
  • $\begingroup$ 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. $\endgroup$ – dspyz Jul 20 '16 at 4:12
  • $\begingroup$ I should clarify that by "select" I mean as decision literals. Done. $\endgroup$ – dspyz Jul 20 '16 at 4:13
  • 1
    $\begingroup$ 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. $\endgroup$ – dspyz Jul 20 '16 at 5:07
  • 1
    $\begingroup$ @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? $\endgroup$ – Martin Berger Jul 20 '16 at 8:02
3
$\begingroup$

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.

Improve this answer
$\endgroup$
4
  • $\begingroup$ So in other words, my question isn't particularly realistic considering that the black box involved solves a (likely) harder problem than the solver itself (assuming Liberatore's complexity result still applies when restricted only to negative literals). $\endgroup$ – dspyz Jul 20 '16 at 13:32
  • $\begingroup$ @dspyz I don't know of the top of my head whether Liberatore's proofs can be moved from DPLL to CDCL and to negative literals only. My intuition says that you cannot easily escape to power of optimal literal selection. Worth checking out. $\endgroup$ – Martin Berger Jul 20 '16 at 13:51
  • $\begingroup$ Looking at the paper, their example construction specifically unions a large many-way satisfiable instance with a small UNSAT instance in order to get the exponential-vs-polynomial complexity. But a CDCL solver would solve all such problems in polynomial time because as soon as it selects one of the literals from the UNSAT instance, it would quickly generate the empty clause and terminate regardless of how deep the search is currently. Further, the paper generally discusses only UNSAT instances whereas my question is specifically about satisfiable instances. $\endgroup$ – dspyz Jul 20 '16 at 13:58
  • 1
    $\begingroup$ @dspyz Yes you might be right, but CDCL is no magic wand: it might be possible to augment Liberatore's formulae so CDCL can't crack them in poly-time. Bear in mind that CDCL polynomially simulates resolution, and that short proofs may be worst-case intractable to find. Moreover CDCL has space/time trade-offs, which means that you might have to erase learnt clauses from clause DB, because unit propagation gets slow when you have too many clauses. Proof complexity results say aggressive clause removal can hurt badly. It is also known that sometimes CDCL fails miserably on easy formulas. $\endgroup$ – Martin Berger Jul 20 '16 at 14:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.