Hacker News Reader

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

View on HN

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. :)

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

Reply on news.ycombinator.com