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