Search code examples
randombrute-forcestochasticsat-solverssat

SAT-Solving: DPLL vs.?

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.

Solution

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