<p>Not a direct answer to the question but, as DPLL can be seen as a special case of CDCL, hopefully of interest.</p>

<p>The problem of finding optimal branching literals for DPLL is (in a way) harder than SAT itself: the paper "<a href="http://www.dis.uniroma1.it/~liberato/papers/libe-00-a.pdf" rel="nofollow">On the complexity of choosing
the branching literal in DPLL</a>" by Liberatore shows that 
choosing optimal branching literals in DPLL  is both NP-hard and coNP-hard.</p>

CC BY-SA 3.0
2016-07-20T13:32:40.460Z
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).
dspyz
CC BY-SA 3.0
2016-07-20T13:51:28.537Z
@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.
Martin Berger
CC BY-SA 3.0
2016-07-20T13:58:58.740Z
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.
dspyz
CC BY-SA 3.0
2016-07-20T14:14:32.713Z
@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.
Martin Berger
CC BY-SA 3.0
2016-07-20T08:06:08.837Z
2016-07-20T08:15:21.357Z
2016-07-20T08:15:21.357Z
Martin Berger
<p>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?</p>

<p>Is it necessarily exponential on some infinite class of satisfiable instances?</p>

CC BY-SA 3.0
2016-07-20T04:06:49.823Z
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
CC BY-SA 3.0
2016-07-20T04:12:48.220Z
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
CC BY-SA 3.0
2016-07-20T04:13:47.563Z
I should clarify that by "select" I mean as decision literals. Done.
dspyz
CC BY-SA 3.0
2016-07-20T04:16:41.800Z
How do you define perfection in the perfect literal to select next?
Kyle Jones
CC BY-SA 3.0
2016-07-20T04:22:08.367Z
This sounds a bit like an assignment. Why are you interested in this question?
Kaveh
CC BY-SA 3.0
2016-07-20T04:53:59.727Z
@KyleJones The one that gets you to the answer the quickest
dspyz
CC BY-SA 3.0
2016-07-20T05:04:02.930Z
@Kaveh
a) I'm offended at the implication and
b) It really doesn't
In case you're curious, I read in a paper (I can't find it now) that one popular SAT solver always selects only negative literals.  It explained that the decision isn't arbitrary because of the way many real-world problems are encoded, most variables are more likely to be false than true, and because it always makes the same decision, learned clauses are more likely to be reusable.  But I thought that may mean it's impossible for the solver to run in polynomial time on some sat instances, even with a really good heuristic.
dspyz
CC BY-SA 3.0
2016-07-20T05:07:34.117Z
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
CC BY-SA 3.0
2016-07-20T05:45:41.523Z
When a DPLL based algorithm selects a variable it has to explore both of its subtrees if the formula is unsatisfiable. There are simple SAT instances like PHP where any CDCL SAT algorithm would take exponential time to solve. This is because they correspond to Resolution proofs. You may want to look at the proof of exponential lower bounds on the size of resolution proof for PHP, e.g. check the proof in Jan Krajicek's book from 1995.
Kaveh
CC BY-SA 3.0
2016-07-20T05:49:11.770Z
ps: This question looks a bit like an assignment to me as I said and if that offends you that is your problem. In place of being offended next time please add some background and your motivation to the question. Also if you use your real name people will be less likely to suspect that your questions are assignments.
Kaveh
CC BY-SA 3.0
2016-07-20T05:54:02.413Z
PHP is exponential time because it's UNSAT. The question was specifically about a class of SATISFIABLE instances. In general a SAT solver which has no restriction on which direction it can assign each variable can run in polynomial time just by making the right choice every time. So this question can't be answered by anything which applies to all solvers.
dspyz
CC BY-SA 3.0
2016-07-20T08:02:16.760Z
@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
CC BY-SA 3.0
2016-07-20T13:28:35.597Z
Best-case over heuristic decisions; worst-case over problem instances.
dspyz
CC BY-SA 3.0
2016-07-21T04:14:13.903Z
The original version didn't ask for a satisfiable instance and PHP would have been an answer to the original version. There are not much in general on proving lower bounds on satisfiable instances and was considered an open problem. The only paper I know that proves such a result is Krajicek's "A note on SAT algorithms and proof complexity", 2012. There might be possible to prove something for this special case if one explores what class of resolution proofs correspond to these execution histories.
Kaveh
<sat>
Asymptotic complexity of CDCL SAT solver that only selects negative literals
dspyz
# Asymptotic complexity of CDCL SAT solver that only selects negative literals

(Asked by: username_0 on 2016-07-20)

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?

**Tags:** sat

> **Comments:**
> **username_1**: 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.  
> **username_0**: 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.  
> **username_0**: I should clarify that by "select" I mean as decision literals. Done.  
> **username_1**: How do you define perfection in the perfect literal to select next?  
> **username_2**: This sounds a bit like an assignment. Why are you interested in this question?  
> **username_0**: @KyleJones The one that gets you to the answer the quickest  
> **username_0**: @username_2 a) I'm offended at the implication and b) It really doesn't In case you're curious, I read in a paper (I can't find it now) that one popular SAT solver always selects only negative literals.  It explained that the decision isn't arbitrary because of the way many real-world problems are encoded, most variables are more likely to be false than true, and because it always makes the same decision, learned clauses are more likely to be reusable.  But I thought that may mean it's impossible for the solver to run in polynomial time on some sat instances, even with a really good heuristic.  
> **username_0**: 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.  
> **username_2**: When a DPLL based algorithm selects a variable it has to explore both of its subtrees if the formula is unsatisfiable. There are simple SAT instances like PHP where any CDCL SAT algorithm would take exponential time to solve. This is because they correspond to Resolution proofs. You may want to look at the proof of exponential lower bounds on the size of resolution proof for PHP, e.g. check the proof in Jan Krajicek's book from 1995.  
> **username_2**: ps: This question looks a bit like an assignment to me as I said and if that offends you that is your problem. In place of being offended next time please add some background and your motivation to the question. Also if you use your real name people will be less likely to suspect that your questions are assignments.  
> **username_0**: PHP is exponential time because it's UNSAT. The question was specifically about a class of SATISFIABLE instances. In general a SAT solver which has no restriction on which direction it can assign each variable can run in polynomial time just by making the right choice every time. So this question can't be answered by anything which applies to all solvers.  
> **username_3**: @username_0 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?  
> **username_0**: Best-case over heuristic decisions; worst-case over problem instances.  
> **username_2**: The original version didn't ask for a satisfiable instance and PHP would have been an answer to the original version. There are not much in general on proving lower bounds on satisfiable instances and was considered an open problem. The only paper I know that proves such a result is Krajicek's "A note on SAT algorithms and proof complexity", 2012. There might be possible to prove something for this special case if one explores what class of resolution proofs correspond to these execution histories.  

---

## 1 answers

### Answer by username_3 on 2016-07-20. Score: 3

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](http://www.dis.uniroma1.it/~liberato/papers/libe-00-a.pdf)" by Liberatore shows that
choosing optimal branching literals in DPLL is both NP-hard and coNP-hard.

> **Comments:**
> **username_0**: 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).  
> **username_3**: @username_0 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.  
> **username_0**: 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.  
> **username_3**: @username_0 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.  

---

