# Varisat
Varisat is a [CDCL][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][ipasir] interface
is planned.
## Command Line Usage
Varisat reads a boolean formula in the [DIMACS CNF][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][drat] format supported
by most SAT solvers (and the binary version BDRAT), varisat supports generation
of [LRAT][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][drattrim].
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][drattrim] 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](LICENSE-APACHE) or
http://www.apache.org/licenses/LICENSE-2.0)
* MIT license
([LICENSE-MIT](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.
[cdcl]: https://en.wikipedia.org/wiki/Conflict-Driven_Clause_Learning
[dimacs cnf]: http://www.satcompetition.org/2009/format-benchmarks2009.html
[drat]: https://www.cs.utexas.edu/~marijn/drat-trim/
[lrat]: https://www.cs.utexas.edu/~marijn/publications/lrat.pdf
[ipasir]: https://github.com/biotomas/ipasir
[drattrim]: https://www.cs.utexas.edu/~marijn/drat-trim/