by jix

jix / varisat

SAT solver written in Rust

151 Stars 4 Forks Last release: over 1 year ago (v0.2.1) Other 240 Commits 2 Releases

Available items

No Items, yet!

The developer of this repository has not created any items for sale yet. Need a bug fixed? Help with integration? A different license? Create a request here:


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 (

on and as a command line solver (


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.


Developer Documentation

The internal APIs are documented using rustdoc. It can be generated using

cargo doc --document-private-items --all --exclude varisat-cli

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
  • MIT license (LICENSE-MIT or

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.

We use cookies. If you continue to browse the site, you agree to the use of cookies. For more information on our use of cookies please see our Privacy Policy.