New blog post on SAT solvers

[Siddhartha Gadgil]

Dear friends,

        I have blogged about my experiments with implementing SAT solvers at https://siddhartha-gadgil.github.io/automating-mathematics/posts/sat-solving/

Summary:

      To better understand the SAT (i.e., boolean satisfiability) problem and SAT solvers, I decided to implement a basic one. I was pleasantly surprised that wikipedia has enough details to implement the so called DLPP algorithm quite easily, with even some improvements described in wikipedia. Even better, in the case when there was no solution, the same algorithm gives a proof that there is no solution. The proof that there is no solution was based on resolution due to Davis-Putnam — so the algorithm gives as a bonus a proof that resolution is refutation complete for propositional calculus.