4 ms·
Simple SAT Solver in Haskell
- microarchitect 15y agoNice implementation of DPLL but this algorithm is about 50 years old and nowhere close to the state of the art. The thing is, a modern solver like Chaff [1] is actually quite easy to implement and might be good way of showing off your programming language's elegance and efficiency. [1] http://www.princeton.edu/~chaff/publication/DAC2001v56.pdf http://www.princeton.edu/~chaff/publication/DAC2001v56.pdf
- gatlin 15y agoThis was actually my attempt at learning Haskell moreso than writing something useful. I plan on adding back jumping and clause learning soon. Thanks for the Chaff link, though! Will save me some time. :)
- psykotic 15y agoThe version of MiniSat (a Chaff-style solver) that won the SAT competition a few years ago is only on the order of five hundred lines of code. Code: http://minisat.se/MiniSat.html http://minisat.se/MiniSat.html Paper: http://minisat.se/downloads/MiniSat.pdf http://minisat.se/downloads/MiniSat.pdf
- ZephyrP 15y agoIf a clause contains only a single unassigned literal you can only satisfy by assigning the value that yields this literal as true. Therefore it isn't necessary to make a choice in this case even though unitprop checks. You can avoid a considerable part of the search space by implementing this simple check. Very clever otherwise!
- abecedarius 15y agoBy my reading it doesn't choose a literal until after unit propagating as far as it can.
- tomn 15y agoAs one of my algorithms teachers said, "I don't know how it could have possibly taken four people to come up with DPLL; it's so simple!" Anyway, nice work! A few comments on the Haskell: - Line 16 isn't necessary; that if/then/else is handled by the previous case. - You can change line 16 to "dpll s@(SolverState f r) =". This both pattern matches the argument (so binds f and r), and binds the whole argument to s. This allows you to remove lines 26 and 27. - Line 22 can be written as "let n = negate l". Further, that entire do block is unnecessary -- you could replace the whole thing with a let or a where if you liked.
- gatlin 15y agoLine 16 was necessary because if unitpropagate clears out the formula then chooseLiteral will return Nothing which causes it to say a solvable formula was unsolvable. I'd love more Haskell pointers to help though!
- nandemo 15y ago-- if formula is a null list, this clause will match: dpll (SolverState [] r) = return r -- otherwise this one will match: dpll (SolverState f r) = -- so it is never the case that null f is true here: if null f then return r And the second clause is basically the same as "dpll s =".
- gatlin 15y agoEmpirically I know this not to be the case. Take out the if statement and then run this: > solve [[1],[2]] You'll get "Nothing" when in fact the answer is [2,1]. The reason is that unitpropagate could potentially empty the list before chooseLiteral gets at it. However, I run unitpropagate first because it cuts down the search space dramatically.
- nandemo 15y agoYes, you're right. Sorry, I misread it.
- sold 15y agoclauseSat, simpClause and simplify functions do not need special case for []. You can remove the three lines. Even more, clauseSat s l = elem l s, simpClause c l = filter (/= -l) c.
- gatlin 15y agoNoted and implemented. This has been a most instructive day for me re: Haskell. Thank you very much.