3 ms·
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
by microarchitect 15y ago
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 http://www.princeton.edu/~chaff/publication/DAC2001v56.pdf
- gatlin 15y agoThis 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. :)
- psykotic 15y agoThe 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 http://minisat.se/MiniSat.html Paper: http://minisat.se/downloads/MiniSat.pdf http://minisat.se/downloads/MiniSat.pdf