Simple SAT Solver in Haskell
gist.github.com
gist.github.com
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
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.
-- 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
> 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.
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.
Very clever otherwise!