Comment by tomn | Hacker News Reader

Comment by tomn | Hacker News Reader

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.

Yes, you're right. Sorry, I misread it.

Nah, it had me for a while, too :)

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.

Reply on news.ycombinator.com