varisat 0.1.3

A CDCL based SAT solver (library)
docs.rs failed to build varisat-0.1.3
Please check the build logs for more information.
See Builds for ideas on how to fix a failed build, or Metadata for how to configure docs.rs builds.
If you believe this is docs.rs' fault, open an issue.
Visit the last successful build: varisat-0.2.2

Varisat

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.

License

The Varisat source code is licensed under either of

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.