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
- Apache License, Version 2.0 (LICENSE-APACHE or http://www.apache.org/licenses/LICENSE-2.0)
- MIT license (LICENSE-MIT or http://opensource.org/licenses/MIT)
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.