New blog post on SAT solvers

25 views
Skip to first unread message

Siddhartha Gadgil

unread,
May 28, 2021, 10:57:06 PM5/28/21
to Automated Mathematics India
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.
Reply all
Reply to author
Forward
0 new messages