Varisat is a CDCL based SAT solver written in (unstable) 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.
It is in an early stage of development, implementing little beyond the minimum required for a modern CDCL based SAT solver. While it already offers competitve performance for some problems that arise in practice, there are also problems where Varisat's run-time will be orders of magnitude slower compared to state of the art solvers.
Varisat can be used as a command line utility (the varisat-cli crate) or as a
rust library (this crate). The library interface is unstable and may change at
any time. The command line interface follows the same conventions as other
command line SAT solvers. Additionally a C wrapper using the IPASIR
interface is planned.
The Varisat source code is licensed under either of
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.