A simple SAT solver that implements the DPLL algorithm with unit resolution
A SAT Solver based on the Davis-Putnam-Logemann-Loveland (DPLL) algorithm.
$ git clone https://github.com/sukrutrao/SAT-Solver-DPLL.git
$ cd SAT-Solver-DPLL
$ 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.
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
.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.
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.