SAT-Solver

A SAT-solver implemented in C++ using the DPLL algorithm.

Input

The input is taken in a CNF file (.cnf).
A sample input file would be:

c sentences starting with c are comments and not compiled
c next line would be compiled and the first number gives the literal count
c and second number gives the number of clauses
p cnf 3 6
1 2 0
1 -2 0
3 2 0
-3 1 0
1 2 3 0
-1 -2 0

Output

SAT
1 -2 3 0

Positive literal defines it will be true. Negative literal defines it will be false.