SAT-Solver-CDCL
SAT-Solver-CDCL copied to clipboard
A simple SAT solver based on the CDCL algorithm
SAT-Solver-CDCL
A SAT Solver based on Conflict Driven Clause Learning (CDCL).
Installation
Prerequisites
- g++ (or any other C++ compiler) with C++11 support
- GNU make
Building the project
- Clone the repository
$ git clone https://github.com/sukrutrao/SAT-Solver-CDCL.git
$ cd SAT-Solver-CDCL
- Compile the program
$ make
If you use a different compiler, please edit the Makefile accordingly.
Running the solver
The solver accepts input from standard input (STDIN) and sends output to the standard output (STDOUT).
Input format
The input is a SAT formula is DIMACS format. A detailed description can be found here.
Output format
- 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 a0
. - If the formula is unsatisfiable, the output consists of a single word,
UNSAT
.
Running the solver
If the input is in a file input.cnf, use
$ ./solver < input.cnf
Example
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.
License
This project is licensed under the MIT License.
Author
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.