PROJECT 3. 

IMPLEMENTATION OF THE DAVIS-PUTNAM PROCEDURE

==============================================


1. The Davis-Putnam Procedure


The Davis-Putnam procedure is an algorithm for deciding the satisfiability 
of formulas in the propositional calculus. With some aditional effort it 
can also return models of the formula.

The Davis-Putnam procedure operates on formulas in clausal form. Its input 
is a set of clauses, where each clause is a set of literals and each literal 
is either an atomic formula (a positive literal) or its negation (a negative 
literal). A clause is interpreted as the disjunction of its literals and a 
set of clauses as the conjunction of its clauses. A positive clause contains 
only positive literals. A negative clause contains only negative literals. 
The empty clause contains no literals and is unsatisfiable. A unit clause 
has a single literal.

A version of Davis-Putnam procedure is defined below. Calling DP(S,{}) returns 
a set of models for the set of clauses S. The assign operation applies an 
atom's truth-value assignment to a set of clauses.

---------------------------------------------

DP(S,M) ==

   1. If S={} (S is the satisfiable empty set of clauses), return {M}.
   2. If {} belongs to S (S contains the unsatisfiable empty clause, return {}.
   3. If a positive unit clause {A} belongs to S, return DP(assign(A,true,S), M union {A}).
   4. If a negative unit clause {not A} belongs to S, return DP(assign(A,false,S),M).
   5. If S contains no positive clauses, return {M}.
   6. Let A be an atomic formula occurring a positive clause with smallest size in S. Return:
      DP(assign(A,true,S),M union {A}) union DP(assign(A,false,S),M).

---------------------------------------------

assign(A,true,S)==
   
   1. Let S'={C | C belongs to S and A does not belong to C} (do unit subsumption by A)
   2. Return {C-{not A} | C belongs to S'} (do unit resolution with A).

---------------------------------------------

assign(A,false,S)==

   1. Let S'={C | C belongs to S and not A does not belong to C} (do unit subsumption by not A)
   2. Return {C-{A} | C belongs to S'} (do unit resolution with not A).

==========================================================


2. Transformation of a Propositional Formula into Conjunctive Normal Form.

The following rules are used to transform an arbitrary propositional formula into 
equivalent conjunctive normal form (conjunction of disjunctions of literals):

1. Elimination of double negation: 
	       not (not A) ---> A 

2. Elimination of implication: 
	       A implies B ---> not A or B

3. De Morgan's law 1:
	       not (A and B) ---> not A or not B

4. De Morgan's law 2:
	       not (A or B) ---> not A and not B

5. Distribution 1:
	       (A and B) or C ---> (A or C) and (B or C)

6. Distribution 2:
	       C or (A and B) ---> (C or A) and (C or B)


A formula into conjunctive normal form 
	  (l1 or ... or ln) and ... and (r1 or ... or rm)
can be represented as a set of clauses
          {{l1, ..., ln},...,{r1,...,rm}}.

=========================================================

3. Requirements.


Write a Prolog program that implements the satisfiablity checker for propositional 
formulas. The program 

1. Accepts a propositional formula as an input.
2. Transforms it into a set of clauses using the conjunctive normal form transformations. 
3. Runs the Davis-Putnam procedure on the set of clauses obtained at step 2.
4. Returns the answer computed by the procedure, with an additional explanation 
(e.g. if the set of models returned by the procedure is empty, it should write 
something like 'The formula is unsatisfiable'. If the set of models are not empty, 
the answer should be 'The formula is satisfiable. Some of its models are:' and the set of models).
5. Should have options to choose between taking the input either from the keyboard, 
or from a file. The output also optionally should be shown on the screen or written 
to a file.
6. Uses operator declarations.
7. Is well documented.

The whole project can be splitted into three Prolog files: one for conjunction 
normal form computation, second for the Davis-Putnam procedure and the third for 
the main procedure that loads the other two files and controls input and output.

=========================================================

4. References.

1. M. Davis and H. Putnam. A compution procedure for quantification theory. 
J. ACM 7 (1960), 201-215.

2. C. L. Chang and R.C. Lee. Symbolic Logic and Mechanical Theorem Proving. 
Academic Press. New York. 1973.

3. T. E. Uribe and M. E. Stickel. Ordered Binary Decision Diagrams and the 
Davis-Putnam Procedure. In First International Conference on Constraints in 
Computational Logics, Lecture Notes in Computer Science, Vol. 845, pages 34-49, 
Springer-Verlag, Munich, September 1994. 
Available from http://theory.stanford.edu/people/uribe/papers.html