Please check build logs and if you believe this is docs.rs' fault, report into this issue report.
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
- 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.