varisat 0.1.1

A CDCL based SAT solver
varisat-0.1.1 is not a library.
Visit the last successful build: varisat-0.2.2

Varisat

Varisat is a CDCL based SAT solver written in (unstable) rust. Given a boolean formula in conjunctive normal form, it either finds a variable assignment that makes the formula true or finds a proof that this is impossible.

It is in an early stage of development, implementing little beyond the minimum required for a modern CDCL based SAT solver. While it already offers competitve performance for some problems that arise in practice, there are also problems where Varisat's run-time will be orders of magnitude slower compared to state of the art solvers.

So far it only offers a command line interface. A rust library interface as well as a C library interface are planned.

Command Line Usage

Varisat reads a boolean formula in the DIMACS CNF format. The input is read from the file given on the command line or from stdin. The header line is ignored and can be omitted.

During the solving process, some statistics are printed to stdout. This output consists of lines prefixed with the character c.

For a satisfiable instance the line s SATISFIABLE is output. This is followed by the solution on lines prefixed with v. The solution is a space-separated list of all literals that are true in the satisfying assignment. The list is terminated by a 0. The exit code will be 10.

For an unsatisfiable instance the line s UNSATISFIABLE is output and the exit code will be 20. A proof of unsatisfiability in the DRAT format will be produced if the -p <FILE> flag was specified. For now the proof is actually in the DRUP format which is a subset of DRAT, but this may change when more advanced techniques are implemented.

Example Usage

$ cat sat.cnf
p cnf 5 12
-1 -2 0
-1 -3 0
-1 -4 0
-1 -5 0
-2 -3 0
-2 -4 0
-2 -5 0
-3 -4 0
-3 -5 0
-4 -5 0
2 5 3 4 1 0
4 2 3 1 5 0
$ varisat sat.cnf
c Reading file 'sat.cnf'
c Read 12 clauses
c total: 0.0 sec
c restarts: 0
c conflicts: 0 (0.0 / sec)
c decisions: 1 (492368.3 / sec)
c propagations: 5 (2461841.5 / sec)
s SATISFIABLE
v 1 -2 -3 -4 -5 0
$ echo $?
10

$ cat unsat.cnf
p cnf 5 20
-1 -2 -3 0
-1 -2 -4 0
-1 -2 -5 0
-1 -3 -4 0
-1 -3 -5 0
-1 -4 -5 0
-2 -3 -4 0
-2 -3 -5 0
-2 -4 -5 0
-3 -4 -5 0
1 2 5 0
1 2 3 0
1 2 4 0
1 5 3 0
1 5 4 0
1 3 4 0
2 5 3 0
2 5 4 0
2 3 4 0
5 3 4 0
$ varisat unsat.cnf
c This is varisat 0.1.1
c Reading file 'unsat.cnf'
c Read 20 clauses
c total: 0.0 sec
c restarts: 0
c conflicts: 6 (680889.7 / sec)
c decisions: 5 (567408.1 / sec)
c propagations: 17 (1929187.5 / sec)
s UNSATISFIABLE
$ echo $?
20

License

The Varisat source code is licensed under either of

at your option.

Contribution

Unless you explicitly state otherwise, any contribution intentionally submitted for inclusion in Varisat by you, as defined in the Apache-2.0 license, shall be dual licensed as above, without any additional terms or conditions.