jix/varisat

SAT solver written in Rust

Source code at GitHub https://jix.one/project/varisat

{
  "createdAt": "2019-02-03T16:19:00Z",
  "defaultBranch": "master",
  "description": "SAT solver written in Rust",
  "fullName": "jix/varisat",
  "homepage": "https://jix.one/project/varisat",
  "language": "Rust",
  "name": "varisat",
  "pushedAt": "2022-11-02T21:46:18Z",
  "stargazersCount": 275,
  "topics": [],
  "updatedAt": "2025-09-26T07:02:33Z",
  "url": "https://github.com/jix/varisat"
}

Varisat

Varisat is a [CDCL][cdcl] based SAT solver written in rust. Given a boolean formula in [conjunctive normal form][cnf], 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][crate-varisat]) and as a command line solver ([varisat-cli on crates.io][crate-varisat-cli]).

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][releases] for Linux and Windows.

Documentation

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][blog-series].

License

The Varisat source code is licensed under either of

Apache License, Version 2.0 ([LICENSE-APACHE]!(LICENSE-APACHE) or http://www.apache.org/licenses/LICENSE-2.0)
MIT license ([LICENSE-MIT]!(LICENSE-MIT) or http://opensource.org/licenses/MIT)

at your option.

Contribution

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.

[cdcl] !: https://en.wikipedia.org/wiki/Conflict-Driven_Clause_Learning [cnf] !: https://en.wikipedia.org/wiki/Conjunctive_normal_form [dev-docs] !: https://jix.github.io/varisat/dev/varisat/ [blog-series] !: https://jix.one/tags/refactoring-varisat/ [crate-varisat] !: https://crates.io/crates/varisat [crate-varisat-cli] !: https://crates.io/crates/varisat-cli [manual-master] !: https://jix.github.io/varisat/manual/master/ [releases] !: https://github.com/jix/varisat/releases