Clever Geek Handbook

SAT solution: DPLL vs.

I'm writing about a SAT solution right now and I'm stuck at a certain point. I hope you can help me.

I want to describe some methods for solving SAT problems. Right now I have three different ways:

  • Bruteforce
  • Random (naive)
  • DPLL (with various heuristics)
  • ? is absent?
  • ...

My problem is that the only efficient algorithm is DPLL (and some others that are slightly different from DPLL). so I have nothing to compare DPLL.

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

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

  • Monien-Speckenmeyer
  • Dantzin, Gerdt, Hirsch and Schöning
  • Paturi-Pudlák-Zein-Algorithmus
  • Hofmeister, Schöning, Schuler and Watanabe

Thank you for your help.

+3


source to share


2 answers


A modern satellite solver currently uses DPLL based CDCL (Conflict Drive Clause Learning).



+4


source


Of the algorithms you proposed, the SAT, bruteforce, and DPLL solutions are both complete algorithms that, given enough time, are guaranteed to find a satisfactory task or confirm that the problem is not satisfactory. As Million mentions, CDCL, DPLL's promotion is also complete.

If you want to discuss alternatives, I would recommend looking at incomplete algorithms. They are often based on stochastic local search and include GSAT and WalkSAT. While these algorithms are not guaranteed to find the answer, they are traditionally very well versed in random (as it relates to industrial) SAT problems. They have also been used to solve more SAT problems than any solver implementing DPLL-based algorithms could solve.



For further research, I recommend Biere's excellent Satisfaction Guide.

+1


source






More articles:


All Articles