Varisat is a CDCL based SAT solver written in 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.

Varisat is open source software. You can find the Varisat project on GitHub.

Varisat is available as a rust library (varisat on crates.io) and as a command line solver (varisat-cli on crates.io).

In addition to this user manual, Varisat comes with an API documentation.