# Sat Solving

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 **DPLL** 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.

# Automating Mathematics India

I have created a google group meant for informal discussions among those interested in Automated Theorem Proving. This is aimed mainly at those in/from India, but everyone interested in the topic is of course welcome.

# Solving (but not proving?) Pappus

Thanks to some very nice work done by Anand Tadipatri after he read the previous post on proving theorems using SMT solvers, we find that in a sense the theorem of Pappus can be **solved** (but, so far at least, in some sense not **proved**) by **Z3** — a happier conclusion than last time. I make this precise below, assuming the reader is familiar with the previous post.