5 ms·
Not laid off but on an extended sabbatical. I'm working on a Rust library for SAT solving and other things informed by John Harrison's text on Automated Theore
by AxEy 4y ago
Not laid off but on an extended sabbatical.
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 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).
- theGnuMe 4y agoInteresting.. What do you think about Survey Propagation?
- AxEy 4y agoI'm afraid I was not familiar, although I'm looking at a few related papers on the arxiv now. What brought that approach to mind?
- theGnuMe 4y agoSurvey Propagation is one of the best algorithms for solving very hard SAT instances. Here's a good review paper that captures it. http://www.cs.cornell.edu/~sabhar/publications/surveyPropUAI07b.pdf http://www.cs.cornell.edu/~sabhar/publications/surveyPropUAI...
- AxEy 4y agoThanks
- YorkshireSeason 4y agoSurvey 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]. [1] M. Mezard, G. Parisi, R. Zecchina, Analytic and Algorithmic Solution of Random Satisfiability Problems. https://aiichironakano.github.io/cs653/Mezard-RSAT-Science02.pdf https://aiichironakano.github.io/cs653/Mezard-RSAT-Science02... [2] https://en.wikipedia.org/wiki/Giorgio_Parisi https://en.wikipedia.org/wiki/Giorgio_Parisi
- YorkshireSeason 4y agoUnfortunately, 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.
- AxEy 4y agoI'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).