Automated reasoning - Very Simple Sat solver

Need help with automated reasoning?

Satisfiability (SAT) is the problem of determining if a formula can be evaluate to TRUE.

A nice example after Lewis Carroll is:
1. Good-natured tenured professors are dynamic
2. Grumpy student advisors play slot machines
3. Smokers wearing a cap are phlegmatic
4. Comical student advisors are professors
5. Smoking untenured members are nervous
6. Phlegmatic tenured members wearing caps are comical
7. Student advisors who are not stock market players are scholars
8. Relaxed student advisors are creative
9. Creative scholars who do not play slot machines wear caps
10. Nervous smokers play slot machines
11. Student advisors who play slot machines do not smoke
12. Creative good-natured stock market players wear caps
13. Therefore no student advisor is smoking 

Is it true that claim 13 can be concluded from statements 1 until 12? 

We want this to be determined by in a automated manner. First we need to translating this to something a computer can understand: 

(((A & B & C) -> D) &
((!A & M) -> L) &
((F & E) -> !D) &
((G &M) -> C) &
((F & :B) -> !H) &
((!D & B & E) -> G) &
((!I &M) -> J) &
((H &M) -> K) &
((K & J & !L) -> E) &
((!H & F) -> L) &
((L &M) -> !F) &
((K & A & I) -> E) ) -> !(M & F)

A simple method now would be the use of truth tables, but this would result in having 8192 rows (2 to the power of the number of variables). For a computer this is doable, however in many situations the number of variables would be very high there for unusable. One have to know there is no polynomial algorithm known for SAT. It has been proven that SAT is NP-complete. There are algorithms that are faster than the truth table method, one of them is the Semantic tableaux method. This method can be used in my tool for determining SAT of a propositional formula. Another method is resolution, but resolution is only applicable to formulas in a CNF (conjunctive normal form) shape. The tool can there for transform a arbitrary propositional formula into a CNF formula by a Tseitin transformation. Resolution with the Davis-Putnam's procedure is now possible on the formula. Another method that can be use on the CNF is the DPLL method for determining satisfiability. The last method that can be used by the tool to determine SAT is ROBDD, Reduced Ordered Binary Decision Diagrams.

One has to know that this tool is for educational purpose and not really for big formulas (then use minisat, yices or any other SAT solver or SMT solver). You can see the steps that the algorithm make, thereby understanding the algorithms (hopefully). All algorithms give a log what and why did a step. Some algorithms even can be done step by step, together with a graphical representation. For an explanation of the algorithms I refer you to the Internet, there is enough information on it on this topic

Here I have added some screen-shots of the program. If you want to run the program you NEED to install Graphviz and add the install folder to your path!

Sybren Roede (1 july 2011)

The main form and truth table, the formula is a tautology.

The Semantic tableaux form, not all paths are closed.

The Tseitin form for converting a formula into a CNF formula.

Resolution via Davis-Putnam's procedure.

Resolution via DPLL procedure.

ROBBD somewhere in the middle of the algorithm.

ROBDD algorithm at the end.