Varisat

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 available as a Rust library (varisat on crates.io) and as a command line solver (varisat-cli on crates.io).

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

Installation

Varisat is available using Rust’s package manager cargo. The command line solver can be installed or updated using cargo install --force varisat-cli. Cargo can be installed using rustup.

The command line solver is also available as a pre-compiled binary for Linux and Windows.

Documentation

• User Manual
• Library API Documentation

Developer Documentation

The internal APIs are documented using rustdoc. It can be generated using cargo doc --document-private-items --all --exclude varisat-cli or viewed online (master).

A version of the user manual built from the master branch is also available.

You can also read a series of blog posts about the development of varisat.