Jix' Site


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.

It has a stable command line interface and an unstable rust library interface. A C library interface is planned.

Varisat can be installed using the cargo package manager and nightly rust:

cargo install varisat-cli

Alternatively you can download a statically linked linux binary: varisat 0.1.3 x86_64

The MIT/Apache-2.0 dual licensed source code is available on GitLab