Skip to content

A simple SAT solver that implements the DPLL algorithm with unit resolution

License

Notifications You must be signed in to change notification settings

sukrutrao/SAT-Solver-DPLL

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

24 Commits
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

SAT-Solver-DPLL

Build Status

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

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-DPLL.git
$ cd SAT-Solver-DPLL
  • 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 a 0.
  • 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

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.

About

A simple SAT solver that implements the DPLL algorithm with unit resolution

Topics

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published