20

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

Anonymous
  • 4,041
  • 19
  • 43

6 Answers6

22

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 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.

Opt
  • 1,311
  • 14
  • 20
  • 10
    DPLL with clause learning (or nogood learning, as you call it) and restarts has been shown to be equivalent to general resolution. – Jan Johannsen Nov 24 '11 at 09:24
  • 1
    @JanJohannsen, is this the paper you refer to? http://arxiv.org/abs/1107.0044 – Radu GRIGore Nov 24 '11 at 14:31
  • 5
    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 Nov 25 '11 at 09:46
  • 3
    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 Nov 25 '11 at 10:03
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.

Timothy Chow
  • 7,550
  • 35
  • 43
10

There are SAT solvers based on the local search. See, for example, this paper for exposition.

ilyaraz
  • 1,569
  • 18
  • 33
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)
malejpavouk
  • 171
  • 3
4

Monte Carlo Tree Search (MCTS) 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.

Juho
  • 3,170
  • 2
  • 26
  • 36
-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.

vzn
  • 11,014
  • 2
  • 31
  • 64
  • 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 Oct 23 '13 at 02:32
  • 4
    Do you understand that I have asked for algorithms not based on DPLL? – Anonymous Oct 23 '13 at 03:06
  • ?!? yes the algorithms listed are distinctly different as indicated – vzn Oct 23 '13 at 03:16
  • 2
    Do you understand what "based" means? Told you: don't use my questions to comment on whatever you want to comment on! – Anonymous Oct 23 '13 at 04:03
  • 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 – Sasho Nikolov Oct 23 '13 at 04:04
  • 7
    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 Oct 23 '13 at 11:56
  • 4
    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 Oct 23 '13 at 12:12
  • 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 Oct 23 '13 at 15:15
  • 2
    @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 Oct 23 '13 at 17:53
  • 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 Oct 23 '13 at 18:02
  • 1
    @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 Oct 23 '13 at 19:45
  • 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 Oct 23 '13 at 20:33
  • 1
    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 Oct 23 '13 at 23:05
  • 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 Oct 23 '13 at 23:16
  • @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 Oct 24 '13 at 09:40
  • 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 Oct 24 '13 at 14:59
  • 1
    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 Oct 25 '13 at 03:56
  • 2
    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 Oct 25 '13 at 03:57
  • 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 Oct 25 '13 at 04:18
  • 2
    @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 Oct 25 '13 at 06:44
  • 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 Oct 25 '13 at 15:02
  • 2
    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 Oct 25 '13 at 16:03
  • 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 Oct 25 '13 at 16:15