This is largely for me to to learn Rust, but I think it may have the potential to turn into something cool. Next on the todo list is optimizations to DPLL as the existing implementation is currently in its most basic form (I skipped optimizations there for the time being in order to move on to predicate calculus).
Unfortunately, Harrison's book, despite its many other merits, doesn't really treat CDCL (= conflict-driven clause learning), which is really what makes SAT solvers fly.
I'll be happy to circle back to more modern methods once the core parts of the field are addressed. The point of the library is not really to deliver a competitive solver (yet).
Survey propagation works primarily with random SAT instances, but isn't competitive with SAT instances that arise in industrial verification, where CDCL shines. Some gossip: survey propagation was proposed by Mezard, Parisi, and Zecchina [1], and
G. Parisi won the physics Nobel price in 2021 [2].
I'm working on a Rust library for SAT solving and other things informed by John Harrison's text on Automated Theorem Proving.
https://github.com/aetilley/harrison-rust
This is largely for me to to learn Rust, but I think it may have the potential to turn into something cool. Next on the todo list is optimizations to DPLL as the existing implementation is currently in its most basic form (I skipped optimizations there for the time being in order to move on to predicate calculus).