SAT-Solving: DPLL vs.?

Question

right now I am writing about SAT-solving and I am stuck at a point. I am hoping that you can help me.

I want to describe some methods to solve SAT-Problems. Right now I have three different ways:

1. Bruteforce
2. Random (naive)
3. DPLL (with different heuristics)
4. ? missing ?
5. ...

My Problem is that the only effective algorithm is DPLL (and some other that differ slightly from DPLL). thus I have nothing to compare DPLL with.

My Question: It would be great if you can tell me some algorithms that are not based an DPLL (DP) which I can compare it to.

Here are some that I found but can't decide if they would be a good choice or if there are better ones:

• Monien-Speckenmeyer
• Dantsin, Goerdt, Hirsch and Schöning
• Paturi-Pudlák-Zane-Algorithmus
• Hofmeister, Schöning, Schuler and Watanabe

Thanks for your help.

Answer 1

State-of-art sat solver currently uses CDCL(Conflict Drive Clause Learning) based on the DPLL.

Answer 2

Of the SAT solving algorithms that you have suggested, bruteforce and DPLL are both complete algorithms that, given enough time, are guaranteed to find a satisfying assignment or prove the problem unsatisfiable. As Million mentions, CDCL, an advancement of DPLL, is also complete.

If you are looking to discuss alternatives, I would recommend looking at Incomplete algorithms. These are often based on stochastic local search, and include GSAT and WalkSAT. While these algorithms are not guaranteed to find an answer, they are traditionally very good at solving random (as apposed to industrial) SAT problems. They have also been used to solve larger SAT problems than any solver implementing a DPLL-based algorithms has been able to solve.

For further research I recommend Biere's wonderful book, 'Handbook of Satisfiability'.