Hacker Newsnew | comments | show | ask | jobs | submit login

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




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

-----




Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | DMCA | Apply to YC | Contact

Search: