Prashanth K - 08305006

I have implemented the DPLL algorithm. It takes a set of clauses in CNF and outputs a model for it if it is satisfiable, else it reports unsatisfiability. 

The code is written in Java and the class DPLL is contained in package dpll. The constructor takes an arraylist of clauses in CNF as input. Method doDpll() returns true if the set is satisfiable, and throws Unsatisfiable exception if it is not satisfiable. The truth assignments can be obtained from the static Hash array DPLL.result.

-------------------------------------------
Input format:

I have used the following CNF format: Every clause is in a new line. The literals in each clause are separated by a |. There is no \n after the final clause
Example
A|B|C
~A|C
~C

-------------------------------------------
Running instructions.

cd code/dpll
bash run.sh <input_file_name>

Example: bash run.sh contra.txt
(contra.txt has to be in the same directory)

--------------------------------------------
Test cases:

1) Contradiction: contra.txt
	A|B
	~A|C
	~B|D
	~C|F
	~B
	~C
Result:Unsatisfiable

2) DPLL with no backtracking: simple.txt
	A|B|~C
	~A|~B
	C
	A|~B
Result: A:T,B:F,C:T 

3) DPLL with backtracking: complex.txt
	A|B
	~A|~B
	~A|B
Result: A:F,B:T
