Are there any algorithms for SAT solving which are not DPLL based? Or are all algorithms used by SAT solvers are DPLL based?
$\begingroup$
$\endgroup$
1
-
8$\begingroup$ related cstheory.stackexchange.com/questions/7469/… $\endgroup$– Radu GRIGoreNov 23, 2011 at 18:28
Add a comment
|
6 Answers
$\begingroup$
$\endgroup$
4
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.
-
10$\begingroup$ DPLL with clause learning (or nogood learning, as you call it) and restarts has been shown to be equivalent to general resolution. $\endgroup$ Nov 24, 2011 at 9:24
-
1$\begingroup$ @JanJohannsen, is this the paper you refer to? arxiv.org/abs/1107.0044 $\endgroup$ Nov 24, 2011 at 14:31
-
5$\begingroup$ 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. dx.doi.org/10.1016/j.artint.2010.10.002 $\endgroup$ Nov 25, 2011 at 9:46
-
3$\begingroup$ 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. $\endgroup$ Nov 25, 2011 at 10:03
$\begingroup$
$\endgroup$
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.
$\begingroup$
$\endgroup$
There are SAT solvers based on the local search. See, for example, this paper for exposition.
$\begingroup$
$\endgroup$
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)
$\begingroup$
$\endgroup$
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.
$\begingroup$
$\endgroup$
23
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.
-
4$\begingroup$ Do you understand that I have asked for algorithms not based on DPLL? $\endgroup$ Oct 23, 2013 at 3:06
-
2
-
7$\begingroup$ 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 $\endgroup$ Oct 23, 2013 at 4:04
-
7$\begingroup$ 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. $\endgroup$– JuhoOct 23, 2013 at 11:56
-
4$\begingroup$ 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. $\endgroup$– JuhoOct 23, 2013 at 12:12