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.
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. :)
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.
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!
-- 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 =".
Empirically 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.
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.
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.
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.
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