varisat-cli 0.1.3

A CDCL based SAT solver (command line tool)
varisat-cli-0.1.3 is not a library.

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.

Varisat can be used as a command line utility (this crate) or as a rust library (the varisat crate). The library interface is unstable and may change at any time. The command line interface follows the same conventions as other command line SAT solvers. Additionally a C wrapper using the IPASIR interface is 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 will be produced if a second argument is given on the command line. The proof format can be selected with the --proof-format option. In addition to the DRAT format supported by most SAT solvers (and the binary version BDRAT), varisat supports generation of LRAT proofs (and the binary version CLRAT). This allows for faster and verified proof checking. The runtime overhead for LRAT proof generation is lower than generation of DRAT followed by conversion to LRAT using DRAT-trim.

Varisat also supports on the fly proof trimming, which can remove some unnecessary proof steps during proof generation. This is enabled by --trim-proof. The result is similar to the output of the DRAT-trim tool. The runtime overhead of on the fly proof trimming is lower than a separate DRAT-trim run.

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 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.