Simple SAT Solver in Haskell

https://gist.github.com/1755736

by gatlin • 14 years ago

57 14 14 years ago

gist.github.com

Nice 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

gatlin5• 14 years ago

This 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• 14 years ago

The 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

Paper: http://minisat.se/downloads/MiniSat.pdf

ZephyrP• 14 years ago

If 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• 14 years ago

By my reading it doesn't choose a literal until after unit propagating as far as it can.

tomn2• 14 years ago

As 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.

gatlin5• 14 years ago

Line 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!

nandemo2• 14 years 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 =".

tomn2• 14 years ago

Yeah, sorry about that... I totally missed the ' in "f = formula s'" and "f = record s'"!

In that case, I would probably turn the whole thing into a case on "unitpropagate s", and get rid of the outer where, but my advice is clearly best taken with a pinch of salt.

sold• 14 years ago

clauseSat, 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.

gatlin5• 14 years ago

Noted and implemented. This has been a most instructive day for me re: Haskell. Thank you very much.

Simple SAT Solver in Haskell

Related Stories