3 ms·
A fun exercise is to write a series of sat solvers: brute force, DPLL and CDCL you really get an immediate feel for the strength of the algorithms and none of t
by xavxav 3y ago
A fun exercise is to write a series of sat solvers: brute force, DPLL and CDCL you really get an immediate feel for the strength of the algorithms and none of these implementations need to go much beyond 50-100 lines in a modern language.
You can then of course spend months tuning and optimizing the hell out of your code to squeeze a further 10x performance.
If you're really crazy like Sarek, you can also formally verify these implementations: https://sarsko.github.io/_pages/SarekSkot%C3%A5m_thesis.pdf https://sarsko.github.io/_pages/SarekSkot%C3%A5m_thesis.pdf
- ykonstant 3y agoWhat a lovely and well-written thesis; I am reading it with great interest.
- philzook 3y agoExcellent link. I would love to see a CDCL implementation in a 100 (understandable) lines. From what I see in the repo, creusat is probably more like 1000?
- GregarianChild 3y agoI found the description of CDCL as an abstract rewrite system illuminating. It's much shorter than an implementation. See e.g. [1]. There is/was a more readable version online, but I can't find it now. [1] https://easychair.org/publications/open/b7Cr https://easychair.org/publications/open/b7Cr
- xavxav 3y agoIndeed, but CreuSAT is actually a high-performance implementation (ie: worst of the best), I should probably just write up a Rust gist of CDCL.
- aaw 3y agoThis one's 250 understandable lines: https://github.com/marijnheule/microsat https://github.com/marijnheule/microsat. You could probably get it to below 200 lines if you removed the restart logic and learned clause compaction, but it's actually a surprisingly competitive solver as is.
- GregarianChild 3y agoIt's worth mentioning Mathias Fleury work who first verified a CDCL implementation [1]. He has written follow-up stuff. [1] https://fmv.jku.at/fleury/papers/Fleury-thesis.pdf https://fmv.jku.at/fleury/papers/Fleury-thesis.pdf
- deleted 3y ago[deleted]