<p>Survey propagation is another algorithm that has been used with success on some kinds of SAT problems, notably random SAT instances.  Like WalkSAT, it cannot be used to prove unsatisfiability, but it is based on very different ideas (message-passing algorithms) from WalkSAT.</p>

CC BY-SA 3.0
2011-11-26T01:01:01.747Z
2011-11-26T01:01:01.747Z
Timothy Chow
<p>There are SAT solvers based on the local search. See, for example, <a href="http://www.satisfiability.org/SAT04/programme/106.pdf">this paper</a> for exposition.</p>

CC BY-SA 3.0
2011-11-23T18:29:22.343Z
2011-11-23T18:29:22.343Z
ilyaraz
<p>You can also say, that all CSP solvers are also SAT solvers. And there are as far as I know two methods used in CSP:</p>

<ul>
<li>Exhaustive DFS with prunning of the search space and checking arc consistency, possibly using shaving to ensure that consistency is maintained as soon as possible.</li>
<li>Local methods (taboo search, simulated annealing)</li>
</ul>

CC BY-SA 3.0
2011-11-23T21:57:30.050Z
2011-11-23T21:57:30.050Z
malejpavouk
<p><a href="http://mcts.ai/index.html" rel="nofollow">Monte Carlo Tree Search (MCTS)</a> has recently achieved some impressive results on games such as Go. The rough basic idea is interleaving random simulation with tree search. It is lightweight and easy to implement, the research hub page I linked contains many examples, papers and some code as well.</p>

<p>Previti et al. [1] did some preliminary investigation of MCTS applied to SAT. They call the MCTS-based search algorithm UCTSAT ("upper confidence bounds applied to trees SAT", if you will). They compared the performance of DPLL and UCTSAT on instances from the SATLIB repository, with the goal of seeing if UCTSAT would produce significantly smaller search trees than DPLL. </p>

<p>For uniform random 3-SAT and flat-graph coloring instances of different sizes, there were no significant differences. However, UCTSAT performed better for real-world instances. Average tree sizes (in terms of the number of nodes) for four different SSA circuit fault analysis instances were in several thousands for DPLL, while always less than 200 for UCTSAT.</p>

<hr>

<p>[1] <a href="http://link.springer.com/chapter/10.1007/978-3-642-23954-0_18" rel="nofollow">Previti, Alessandro, Raghuram Ramanujan, Marco Schaerf, and Bart Selman. "Monte-carlo style UCT search for boolean satisfiability." In AI* IA 2011: Artificial Intelligence Around Man and Beyond, pp. 177-188. Springer Berlin Heidelberg, 2011.</a></p>

CC BY-SA 3.0
2013-10-23T12:09:25.520Z
2013-10-23T12:09:25.520Z
Juho
<p>DPLL does not strictly specify the variable-visit ordering and there is a lot of interesting research looking at optimal variable ordering attack strategies. some of this is incorporated into variable selection logic in SAT algorithms. in a sense some of this research is preliminary in that it shows that different variable attack orderings lead to different sequential constrainedness (which is highly correlated with instance hardness), and devising the most effective heuristics or strategies to exploit this apparently key insight seems to be in the early stages of research.</p>

<ul>
<li><p><a href="http://autodeskresearch.org/pdf/ictai04.pdf" rel="nofollow">Guiding Real-World SAT Solving with Dynamic Hypergraph Separator
Decomposition</a> Li, van Beek</p></li>
<li><p><a href="http://www.st.ewi.tudelft.nl/sat/theses/paul.pdf" rel="nofollow">Decomposing satisﬁability problems
or
Using graphs to get a better insight into satisﬁability problems</a> Herwig</p></li>
<li><p><a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.2.3267" rel="nofollow">The Constrainedness Knife-Edge (1998)</a> Walsh</p></li>
</ul>

CC BY-SA 3.0
2013-10-23T02:32:36.067Z
also, also unspecified by DPLL, similar theory can help with "expected value/what assignment `true/false` to try 1st on each var". also a key theme of this line of research as in the Herwig ref is "clause graph structure".
vzn
CC BY-SA 3.0
2013-10-23T03:06:06.310Z
Do you understand that I have asked for **algorithms not based on DPLL**?
Anonymous
CC BY-SA 3.0
2013-10-23T03:16:54.103Z
?!? yes the algorithms listed are distinctly different as indicated
vzn
CC BY-SA 3.0
2013-10-23T04:03:52.663Z
Do you understand what **"based"** means? **[Told you](http://cstheory.stackexchange.com/questions/14609/are-there-any-known-np-problems-which-are-conjectured-to-be-exponentially-hard-o/14627#comment39668_14627): don't use my questions to comment on whatever you want to comment on!**
Anonymous
CC BY-SA 3.0
2013-10-23T04:04:04.443Z
you yourself are saying they are DPLL based. to me it seems this is like saying that different pivot rules for simplex give you an algorithm that is not a simplex algorithm
Sasho Nikolov
CC BY-SA 3.0
2013-10-23T11:56:12.507Z
I agree with Sasho. Also, the research on variable ordering heuristics is definitely *not* in early stages. The importance has been realized a long time ago (imagine the consequences of a perfect oracle), and a lot of time has been spent on analyzing them. *Value ordering* heuristics become more interesting in CSP solvers, and for some reason, I don't think the research on them has been as booming as for variable ordering.
Juho
CC BY-SA 3.0
2013-10-23T12:12:18.987Z
To be more specific, the initial research on variable ordering heuristics goes back to the 70s. If you are interested, I can dig up the relevant references for you.
Juho
CC BY-SA 3.0
2013-10-23T15:15:42.437Z
anonymous did not strictly define ***"based on"*** and **rants against a reasonable new effort/angle to answer the old question as if respondent is a mind reader**. afaik DPLL **did not specify variable ordering rules or default variable values**. feel free to skip the example. broadly speaking virtually any SAT algorithm is going to assign tentative values to variables. is that all DPLL? too broadly defined, virtually every algorithm is "based on" DPLL merely because its historically very old and very basic. variable reordering ideas go back far, but new ideas are substantially different.
vzn
CC BY-SA 3.0
2013-10-23T17:53:57.807Z
@vzn "Virtually every algorithm is based on DPLL" -- doesn't this question already have plenty of answers saying otherwise? Instead of arguing and trying to nitpick, why not try to see where you might be mistaken, and improve your answer based on the comments?
Juho
CC BY-SA 3.0
2013-10-23T18:02:52.907Z
J, do you or others have _any specific/constructive suggestion?_ am not convinced anyone replying so far understands the answer or has looked at any of the refs to illustrate/support it, there is mostly just "baseless" arguing, nitpicking, apparent mistaken assumptions, & no actual ref to the refs so far =|
vzn
CC BY-SA 3.0
2013-10-23T19:45:46.367Z
@vzn I think it is constructive and specific to point out that say your claim of "research on ordering heuristics is new" is wrong. But if you say you are a not a mind reader, nor is anyone reading your answer :-) That is, even if you list references, you should be the one making the explicit connection as to why a reference supports it, instead of "read all these references here and try to find something supporting me".
Juho
CC BY-SA 3.0
2013-10-23T20:33:46.647Z
juho you fabricate quotes attributed to me, quote me out of context, and put words into my mouth and do not read the actual assertions carefully & adamantly refuse to concede basic valid points. think "evidence is" all respondents incl you have already made up their mind in opposition & are not actually open to a contrary pov. could the real problem be this exact pov is not taught in a book, paper, or a class somewhere? ie is at heart a _research lead or research program as indicated_; nothing can be said that will convince anyone who _apriori_ refuses to read the refs for insight/relevance...
vzn
CC BY-SA 3.0
2013-10-23T23:05:54.370Z
Now you are the only person who says he doesn't get what "based" means! No one else had any trouble with it! Here is an idea: maybe the problem is with you?! You want a constructive comment? Here are mine: Drop this silly self-victimization. You made a mistake. Accept it. Fix it by deleting the answer. Move on. And next time make sure you understand what is being asked before posting.
Anonymous
CC BY-SA 3.0
2013-10-23T23:16:20.560Z
_mistake?_ and what _mistake_ is that? what is this, a college test? owned/graded by Anonymous? indeed, did apparently make a _big mistake_ —in thinking anyone commenting here could note/grasp/understand the (newly emerging) concept, read a paper on the subj, or talk intelligently/politely about it....! dont even see a lot of evidence in the two-line question that you know what you're talking about! re J's fake quote strawman, "Virtually every algorithm is based on DPLL"... _"Or are all algorithms used by SAT solvers are DPLL based?"_
vzn
CC BY-SA 3.0
2013-10-24T09:40:13.307Z
@vzn I'm confused, you did say "virtually every algorithm is "based on" DPLL ..." in a comment (8th comment as of now). Anyway, I suppose we should drop this if we can't discuss in a calm way. There are surely better ways of spending time :-)
Juho
CC BY-SA 3.0
2013-10-24T14:59:24.820Z
you are indeed confused! it says exactly, **too broadly defined, virtually every algorithm is "based on" DPLL**.. the misunderstanding is your interpretation! to clarify, an alternate phrasing is, **if "based on" is too broadly defined, then virtually every SAT algorithm is "based on" DPLL**. you neglect to notice anonymous is asking basically that very question, originally, and that is an answer! "we cant discuss in a calm way"... are you now assuming how I feel? speak for yourself, to me there are few better ways of spending time than calmly discussing TCS with those who can stay calm =)
vzn
CC BY-SA 3.0
2013-10-25T03:56:15.663Z
I removed a previous comment which was too harsh. You sometimes do point out interesting directions but often that is not the case and your posts are just irrelevant to what people are asking as is in this case. You would get more positive reactions if you cared more about what I am asking than about justifying your posts. You may want to look knowledgeable but your posts can deceive no expert cause your knowledge barely scratches the surface.
Anonymous
CC BY-SA 3.0
2013-10-25T03:57:10.187Z
Anyone who is working on or studying SAT solvers would know what "based on DPLL" means. Anyone else would have asked if they didn't understand the question. But you don't and insist on what you have posted ignoring even those who try to help respectfully. Admitting mistakes is not a weakness, insisting on them is. Hope you understand some day no one can be an expert in more than a few topics.
Anonymous
CC BY-SA 3.0
2013-10-25T04:18:32.167Z
anonymous, suggest you _limit yourself to what we are talking about on this post_ and raise any other issues on meta. actually imho your question & comments do not suggest you have significantly worked on or studied SAT solvers. why put yourself in the strange position of pretending that you already know what you are asking? the answer to your question indeed _obviously_ demonstrates care for what you are asking. as for your use of the term "based on" wrt SAT algorithms, our dialog only reveals that its not a shallow concept but which apparently nobody so far cares to consider further.
vzn
CC BY-SA 3.0
2013-10-25T06:44:23.343Z
@vzn would you call the simplex algorithm with a new pivoting heuristic an algorithm that is not "based on simplex". if you would not, how is your example with DPLL and variable orderings any different?
Sasho Nikolov
CC BY-SA 3.0
2013-10-25T15:02:39.527Z
the basic point is that ordering of variables (and initial chosen values) is apparently a critical aspect of optimizing search which later SAT research has revealed,  if anyone would _actually look at the supporting refs_....and this key concept was not apparent at the origination of DPLL. there is an entire asymmetric geometry to be explored here. and now there is significant new theory guiding variable selection, continuing to be developed. it seems to be clear it can make a dramatic difference in solution times. and possibly simplex literature [not an expert] supports this view also....
vzn
CC BY-SA 3.0
2013-10-25T16:03:18.753Z
I did look at your references, and i think you've linked to some of them before. it's not that this is not interesting, but these are optimizations of DPLL. similarly, pivoting rules can make an exponential difference for simplex, but, nevertheless, there are valid reasons to ask for a non-simplex algorithm for LP, and if I did that I would expect to get information about things like interior point methods. If I got some references about pivoting rules, I'd be frustrated, just as Anonymous is.
Sasho Nikolov
CC BY-SA 3.0
2013-10-25T16:15:28.087Z
anonymous has many other decent answers on this old question, dont really know why he & everyone else is obsessing over this one (a well-intentioned attempt to add some freshness/novelty to a long-inactive question, shot down in epic & caustic flames). an algorithm that has theoretically sophisticated pivoting rules imho is qualitatively different than one that has _none_, but thats a subjective call [as everyone else here is attempting to deny]. have not cited the hypergraph ref before on this site, suspect it probably is not cited anywhere on the site so far. as for the others, they tie in.
vzn
CC BY-SA 3.0
2013-10-22T23:45:07.937Z
2013-10-22T23:45:07.937Z
vzn
<p>Resolution Search (just applying the resolution rule with some good heuristics) is another possible strategy for SAT solvers. Theoretically it's exponentially more powerful (i.e. there exist problems for which it has exponential shorter proofs) than DPLL (which just does tree resolution though you can augment it with nogood learning to increase its power - whether that makes it as powerful as general resolution is still open as far as I know) but I don't know of an actual implementation that performs better.</p>

<p>If you don't limit yourself to complete search, then WalkSat is a local search solver which can be used to find satisfiable solutions and outperforms DPLL-based search in many cases. One can't use it to prove unsatisfiability though unless one caches all the assignments that have failed which would mean exponential memory requirements.</p>

<p>Edit: Forgot to add - <a href="http://en.wikipedia.org/wiki/Cutting-plane_method">Cutting planes</a> can also be used (by reducing SAT to an integer program). In particular Gomory cuts suffice to solve any integer program to optimality. Again in the worst case, an exponential number may be needed. I think Arora &amp; Barak's Computational Complexity book has a few more examples of proof systems that one could in theory use for something like SAT solving. Again, I haven't really seen a fast implementation of anything apart from DPLL-based or local search based methods.</p>

CC BY-SA 3.0
2011-11-24T09:24:24.437Z
DPLL with clause learning (or nogood learning, as you call it) and restarts has been shown to be equivalent to general resolution.
Jan Johannsen
CC BY-SA 3.0
2011-11-24T14:31:38.367Z
@JanJohannsen, is this the paper you refer to? http://arxiv.org/abs/1107.0044
Radu GRIGore
CC BY-SA 3.0
2011-11-25T09:46:21.130Z
Yes, there is also an improvement in the following paper:
Knot Pipatsrisawat and Adnan Darwiche. On the power of clause-learning SAT solvers as resolution engines. Artificial Intelligence 175 (2), 2011, pp. 512-525. http://dx.doi.org/10.1016/j.artint.2010.10.002
Jan Johannsen
CC BY-SA 3.0
2011-11-25T10:03:23.307Z
While the paper by Beame et al. linked by Radu Grigore shows that general resolution is p-simulated by a DPLL algorithm with a particular, artificial learning strategy, the above paper shows it for natural learning strategies that are actually used.
Jan Johannsen
CC BY-SA 3.0
2011-11-23T18:19:46.987Z
2011-11-23T20:46:39.053Z
2011-11-23T20:46:39.053Z
Opt
<p>Are there any algorithms for SAT solving which are not DPLL based? 
Or are all algorithms used by SAT solvers are DPLL based?</p>

CC BY-SA 3.0
2011-11-23T18:28:44.737Z
related http://cstheory.stackexchange.com/questions/7469/why-is-there-an-enormous-difference-between-sat-solvers
Radu GRIGore
<ds.algorithms><reference-request><sat>
SAT algorithms not based on DPLL
Anonymous
# SAT algorithms not based on DPLL

(Asked by: username_0 on 2011-11-23)

Are there any algorithms for SAT solving which are not DPLL based?
Or are all algorithms used by SAT solvers are DPLL based?

**Tags:** ds.algorithms, reference-request, sat
> **Comments:**
> **username_1**: related http://cstheory.stackexchange.com/questions/7469/why-is-there-an-enormous-difference-between-sat-solvers  

---

## 6 answers

### Answer by username_8 on 2011-11-23. Score: 22 | Accepted answer

Resolution Search (just applying the resolution rule with some good heuristics) is another possible strategy for SAT solvers. Theoretically it's exponentially more powerful (i.e. there exist problems for which it has exponential shorter proofs) than DPLL (which just does tree resolution though you can augment it with nogood learning to increase its power - whether that makes it as powerful as general resolution is still open as far as I know) but I don't know of an actual implementation that performs better.

If you don't limit yourself to complete search, then WalkSat is a local search solver which can be used to find satisfiable solutions and outperforms DPLL-based search in many cases. One can't use it to prove unsatisfiability though unless one caches all the assignments that have failed which would mean exponential memory requirements.

Edit: Forgot to add - [Cutting planes](http://en.wikipedia.org/wiki/Cutting-plane_method) can also be used (by reducing SAT to an integer program). In particular Gomory cuts suffice to solve any integer program to optimality. Again in the worst case, an exponential number may be needed. I think Arora & Barak's Computational Complexity book has a few more examples of proof systems that one could in theory use for something like SAT solving. Again, I haven't really seen a fast implementation of anything apart from DPLL-based or local search based methods.

> **Comments:**
> **username_9**: DPLL with clause learning (or nogood learning, as you call it) and restarts has been shown to be equivalent to general resolution.  
> **username_1**: @JanJohannsen, is this the paper you refer to? http://arxiv.org/abs/1107.0044  
> **username_9**: Yes, there is also an improvement in the following paper: Knot Pipatsrisawat and Adnan Darwiche. On the power of clause-learning SAT solvers as resolution engines. Artificial Intelligence 175 (2), 2011, pp. 512-525. http://dx.doi.org/10.1016/j.artint.2010.10.002  
> **username_9**: While the paper by Beame et al. linked by Radu Grigore shows that general resolution is p-simulated by a DPLL algorithm with a particular, artificial learning strategy, the above paper shows it for natural learning strategies that are actually used.  

---

### Answer by username_2 on 2011-11-26. Score: 12

Survey propagation is another algorithm that has been used with success on some kinds of SAT problems, notably random SAT instances. Like WalkSAT, it cannot be used to prove unsatisfiability, but it is based on very different ideas (message-passing algorithms) from WalkSAT.


---

### Answer by username_3 on 2011-11-23. Score: 10

There are SAT solvers based on the local search. See, for example, [this paper](http://www.satisfiability.org/SAT04/programme/106.pdf) for exposition.


---

### Answer by username_4 on 2011-11-23. Score: 7

You can also say, that all CSP solvers are also SAT solvers. And there are as far as I know two methods used in CSP:

* Exhaustive DFS with prunning of the search space and checking arc consistency, possibly using shaving to ensure that consistency is maintained as soon as possible.
* Local methods (taboo search, simulated annealing)


---

### Answer by username_5 on 2013-10-23. Score: 4

[Monte Carlo Tree Search (MCTS)](http://mcts.ai/index.html) has recently achieved some impressive results on games such as Go. The rough basic idea is interleaving random simulation with tree search. It is lightweight and easy to implement, the research hub page I linked contains many examples, papers and some code as well.

Previti et al. [1] did some preliminary investigation of MCTS applied to SAT. They call the MCTS-based search algorithm UCTSAT ("upper confidence bounds applied to trees SAT", if you will). They compared the performance of DPLL and UCTSAT on instances from the SATLIB repository, with the goal of seeing if UCTSAT would produce significantly smaller search trees than DPLL.

For uniform random 3-SAT and flat-graph coloring instances of different sizes, there were no significant differences. However, UCTSAT performed better for real-world instances. Average tree sizes (in terms of the number of nodes) for four different SSA circuit fault analysis instances were in several thousands for DPLL, while always less than 200 for UCTSAT.

---

[1] [Previti, Alessandro, Raghuram Ramanujan, Marco Schaerf, and Bart Selman. "Monte-carlo style UCT search for boolean satisfiability." In AI\* IA 2011: Artificial Intelligence Around Man and Beyond, pp. 177-188. Springer Berlin Heidelberg, 2011.](http://link.springer.com/chapter/10.1007/978-3-642-23954-0_18)


---

### Answer by username_6 on 2013-10-22. Score: -4

DPLL does not strictly specify the variable-visit ordering and there is a lot of interesting research looking at optimal variable ordering attack strategies. some of this is incorporated into variable selection logic in SAT algorithms. in a sense some of this research is preliminary in that it shows that different variable attack orderings lead to different sequential constrainedness (which is highly correlated with instance hardness), and devising the most effective heuristics or strategies to exploit this apparently key insight seems to be in the early stages of research.

* [Guiding Real-World SAT Solving with Dynamic Hypergraph Separator
  Decomposition](http://autodeskresearch.org/pdf/ictai04.pdf) Li, van Beek
* [Decomposing satisﬁability problems
  or
  Using graphs to get a better insight into satisﬁability problems](http://www.st.ewi.tudelft.nl/sat/theses/paul.pdf) Herwig
* [The Constrainedness Knife-Edge (1998)](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.2.3267) Walsh

> **Comments:**
> **username_6**: also, also unspecified by DPLL, similar theory can help with "expected value/what assignment `true/false` to try 1st on each var". also a key theme of this line of research as in the Herwig ref is "clause graph structure".  
> **username_0**: Do you understand that I have asked for **algorithms not based on DPLL**?  
> **username_6**: ?!? yes the algorithms listed are distinctly different as indicated  
> **username_0**: Do you understand what **"based"** means? **[Told you](http://cstheory.stackexchange.com/questions/14609/are-there-any-known-np-problems-which-are-conjectured-to-be-exponentially-hard-o/14627#comment39668_14627): don't use my questions to comment on whatever you want to comment on!**  
> **username_7**: you yourself are saying they are DPLL based. to me it seems this is like saying that different pivot rules for simplex give you an algorithm that is not a simplex algorithm  
> **username_5**: I agree with Sasho. Also, the research on variable ordering heuristics is definitely *not* in early stages. The importance has been realized a long time ago (imagine the consequences of a perfect oracle), and a lot of time has been spent on analyzing them. *Value ordering* heuristics become more interesting in CSP solvers, and for some reason, I don't think the research on them has been as booming as for variable ordering.  
> **username_5**: To be more specific, the initial research on variable ordering heuristics goes back to the 70s. If you are interested, I can dig up the relevant references for you.  
> **username_6**: anonymous did not strictly define ***"based on"*** and **rants against a reasonable new effort/angle to answer the old question as if respondent is a mind reader**. afaik DPLL **did not specify variable ordering rules or default variable values**. feel free to skip the example. broadly speaking virtually any SAT algorithm is going to assign tentative values to variables. is that all DPLL? too broadly defined, virtually every algorithm is "based on" DPLL merely because its historically very old and very basic. variable reordering ideas go back far, but new ideas are substantially different.  
> **username_5**: @vzn "Virtually every algorithm is based on DPLL" -- doesn't this question already have plenty of answers saying otherwise? Instead of arguing and trying to nitpick, why not try to see where you might be mistaken, and improve your answer based on the comments?  
> **username_6**: J, do you or others have _any specific/constructive suggestion?_ am not convinced anyone replying so far understands the answer or has looked at any of the refs to illustrate/support it, there is mostly just "baseless" arguing, nitpicking, apparent mistaken assumptions, & no actual ref to the refs so far =|  
> **username_5**: @vzn I think it is constructive and specific to point out that say your claim of "research on ordering heuristics is new" is wrong. But if you say you are a not a mind reader, nor is anyone reading your answer :-) That is, even if you list references, you should be the one making the explicit connection as to why a reference supports it, instead of "read all these references here and try to find something supporting me".  
> **username_6**: juho you fabricate quotes attributed to me, quote me out of context, and put words into my mouth and do not read the actual assertions carefully & adamantly refuse to concede basic valid points. think "evidence is" all respondents incl you have already made up their mind in opposition & are not actually open to a contrary pov. could the real problem be this exact pov is not taught in a book, paper, or a class somewhere? ie is at heart a _research lead or research program as indicated_; nothing can be said that will convince anyone who _apriori_ refuses to read the refs for insight/relevance...  
> **username_0**: Now you are the only person who says he doesn't get what "based" means! No one else had any trouble with it! Here is an idea: maybe the problem is with you?! You want a constructive comment? Here are mine: Drop this silly self-victimization. You made a mistake. Accept it. Fix it by deleting the answer. Move on. And next time make sure you understand what is being asked before posting.  
> **username_6**: _mistake?_ and what _mistake_ is that? what is this, a college test? owned/graded by Anonymous? indeed, did apparently make a _big mistake_ —in thinking anyone commenting here could note/grasp/understand the (newly emerging) concept, read a paper on the subj, or talk intelligently/politely about it....! dont even see a lot of evidence in the two-line question that you know what you're talking about! re J's fake quote strawman, "Virtually every algorithm is based on DPLL"... _"Or are all algorithms used by SAT solvers are DPLL based?"_  
> **username_5**: @vzn I'm confused, you did say "virtually every algorithm is "based on" DPLL ..." in a comment (8th comment as of now). Anyway, I suppose we should drop this if we can't discuss in a calm way. There are surely better ways of spending time :-)  
> **username_6**: you are indeed confused! it says exactly, **too broadly defined, virtually every algorithm is "based on" DPLL**.. the misunderstanding is your interpretation! to clarify, an alternate phrasing is, **if "based on" is too broadly defined, then virtually every SAT algorithm is "based on" DPLL**. you neglect to notice anonymous is asking basically that very question, originally, and that is an answer! "we cant discuss in a calm way"... are you now assuming how I feel? speak for yourself, to me there are few better ways of spending time than calmly discussing TCS with those who can stay calm =)  
> **username_0**: I removed a previous comment which was too harsh. You sometimes do point out interesting directions but often that is not the case and your posts are just irrelevant to what people are asking as is in this case. You would get more positive reactions if you cared more about what I am asking than about justifying your posts. You may want to look knowledgeable but your posts can deceive no expert cause your knowledge barely scratches the surface.  
> **username_0**: Anyone who is working on or studying SAT solvers would know what "based on DPLL" means. Anyone else would have asked if they didn't understand the question. But you don't and insist on what you have posted ignoring even those who try to help respectfully. Admitting mistakes is not a weakness, insisting on them is. Hope you understand some day no one can be an expert in more than a few topics.  
> **username_6**: anonymous, suggest you _limit yourself to what we are talking about on this post_ and raise any other issues on meta. actually imho your question & comments do not suggest you have significantly worked on or studied SAT solvers. why put yourself in the strange position of pretending that you already know what you are asking? the answer to your question indeed _obviously_ demonstrates care for what you are asking. as for your use of the term "based on" wrt SAT algorithms, our dialog only reveals that its not a shallow concept but which apparently nobody so far cares to consider further.  
> **username_7**: @vzn would you call the simplex algorithm with a new pivoting heuristic an algorithm that is not "based on simplex". if you would not, how is your example with DPLL and variable orderings any different?  
> **username_6**: the basic point is that ordering of variables (and initial chosen values) is apparently a critical aspect of optimizing search which later SAT research has revealed,  if anyone would _actually look at the supporting refs_....and this key concept was not apparent at the origination of DPLL. there is an entire asymmetric geometry to be explored here. and now there is significant new theory guiding variable selection, continuing to be developed. it seems to be clear it can make a dramatic difference in solution times. and possibly simplex literature [not an expert] supports this view also....  
> **username_7**: I did look at your references, and i think you've linked to some of them before. it's not that this is not interesting, but these are optimizations of DPLL. similarly, pivoting rules can make an exponential difference for simplex, but, nevertheless, there are valid reasons to ask for a non-simplex algorithm for LP, and if I did that I would expect to get information about things like interior point methods. If I got some references about pivoting rules, I'd be frustrated, just as Anonymous is.  
> **username_6**: anonymous has many other decent answers on this old question, dont really know why he & everyone else is obsessing over this one (a well-intentioned attempt to add some freshness/novelty to a long-inactive question, shot down in epic & caustic flames). an algorithm that has theoretically sophisticated pivoting rules imho is qualitatively different than one that has _none_, but thats a subjective call [as everyone else here is attempting to deny]. have not cited the hypergraph ref before on this site, suspect it probably is not cited anywhere on the site so far. as for the others, they tie in.  

---

