Here is the description for 3SAT satisfiability problem. I already know about the DPLL algorithm, but it's implementation is pretty complex. I would like some algorithm that is relatively simpler but improves the performance by some extent. I would prefer something that is not Tree/Graph based instead bit-mask or multi-bit assignment based approach.
3
-
4$\begingroup$ Why not use a SAT solver where all the hard work has already been done for you? There are also libraries for popular languages that provide solver routines. $\endgroup$– JuhoNov 7, 2020 at 6:38
-
1$\begingroup$ Exhaustive search is straightforward to implement. $\endgroup$– Yuval FilmusNov 7, 2020 at 7:24
-
1$\begingroup$ DPLL isn't all that complex. I can't think of an algorithm that would provide a meaningful speedup over exhaustive search that'd be simpler than DPLL. $\endgroup$– orlpNov 7, 2020 at 12:50
Add a comment
|
2 Answers
$\begingroup$
$\endgroup$
If you're determined not to use the standard deterministic algorithm, the usual alternative is what's known as local search or stochastic search. The basic idea is that you start with a random bit pattern as a variable assignment, observe what's wrong with it in terms of unsatisfied clauses and try to improve it by flipping one or more variable assignments. Observe how this new assignment fails, try to improve it, and repeat.
Local search typically outperforms deterministic search for satisfiable random SAT instances, but performs poorly on more structured instances. It also offers no way to prove unsatisfiability unless some proof system is layered atop it.
There are various local search algorithms on offer, from Uwe Schöning's scheme to PPSZ and its variants. None of them outperform DPLL-based solvers on all instances.
answered Nov 8, 2020 at 2:37
$\begingroup$
$\endgroup$
I've implemented my own CDCL solver (which is the main modern variant of DPLL), and I found that the hardest part by far was understanding and implementing the 1-UIP heuristic, which in my opinion is well-motivated but not very well-explained in the literature.
If you want to see how fast and simple SAT solvers can be, check out Tinisat. It's only around 500 lines of C++, 20% of which is parsing DIMACS files.
