What a lovely and well-written thesis; I am reading it with great interest.
Excellent 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?
Re:The Silent (R)evolution of SAT
by GregarianChild on Friday May 26, 2023 @09:36AM
(#36083937)
I 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.
Indeed, but CreuSAT is actually a high-performance implementation (ie: worst of the best), I should probably just write up a Rust gist of CDCL.
This one's 250 understandable lines: 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.
Re:The Silent (R)evolution of SAT
by GregarianChild on Friday May 26, 2023 @09:28AM
(#36083829)
It's worth mentioning Mathias Fleury work who first verified a CDCL implementation [1]. He has written follow-up stuff.
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