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).
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.
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.
The Varisat source code is licensed under either of
- Apache License, Version 2.0 (LICENSE-APACHE or http://www.apache.org/licenses/LICENSE-2.0)
- MIT license (LICENSE-MIT or http://opensource.org/licenses/MIT)
at your option.
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.