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?
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.
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.
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.