A SAT Solver based on the Davis-Putnam-Logemann-Loveland (DPLL) algorithm.

• g++ (or any other C++ compiler) with C++11 support
• GNU make

• Clone the repository

$ git clone https://github.com/sukrutrao/SAT-Solver-DPLL.git
$ cd SAT-Solver-DPLL

• Compile the program

$ make

If you use a different compiler, please edit the Makefile accordingly.

The solver accepts input from standard input (STDIN) and sends output to the standard output (STDOUT).

The input is a SAT formula is DIMACS format. A detailed description can be found here.

• If the formula is satisfiable, the output consists of two lines. The first line of the output is a single word, SAT. The second line is any satisfying assignment. It consists of space separated boolean variables in ascending order, where the variables have a negative sign if assigned false and no negative sign if assigned true. The last variable is followed by a space and then a 0.
• If the formula is unsatisfiable, the output consists of a single word, UNSAT.

If the input is in a file input.cnf, use

$ ./solver < input.cnf

Let the input be

c 3 variables, 6 clauses
p cnf 3 6
1 2 0
1 -2 0
3 2 0
-3 1 0
1 2 3 0
-1 -2 0

The output is

SAT
1 -2 3 0

Here, the formuls is satisfiable. Variables 1 and 3 are assigned true, and variable 2 is assigned false. This is one possible satisfying assignment.

This project is licensed under the MIT License.

Sukrut Rao

For any issues, queries, or suggestions, please open an issue.

This project was created as a part of the course CS6403: Constraint Solving at IIT Hyderabad.