SAT-Solver-CDCL

KO | EN

gitlite — search

#javascript #python #ai #typescript #golang #linux #docker #nodejs #awesome #awesome-list #vue #pytorch #openai #open-source

SAT-Solver-CDCL

(★ 20)

A simple SAT solver based on the CDCL algorithm

SAT-Solver-CDCL Latest Version Download

Download Latest Version (.zip)

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

# SAT-Solver-CDCL

[![Build Status](https://travis-ci.com/sukrutrao/SAT-Solver-CDCL.svg?branch=master)](https://travis-ci.com/sukrutrao/SAT-Solver-CDCL)

A SAT Solver based on [Conflict Driven Clause Learning (CDCL)](https://en.wikipedia.org/wiki/Conflict-Driven_Clause_Learning).

## 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](http://www.satcompetition.org/2009/format-benchmarks2009.html).

### 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](LICENSE).

## Author
[Sukrut Rao](https://sukrutrao.github.io)

For any issues, queries, or suggestions, please [open an issue](https://github.com/sukrutrao/SAT-Solver-CDCL/issues/new).

---

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

SAT-Solver-CDCL

SAT-Solver-CDCL Latest Version Download

Today's picks

Was this content helpful?

Recent Feedback

SAT-Solver-CDCL

SAT-Solver-CDCL Latest Version Download

Today's picks

Was this content helpful?

Recent Feedback

Download README