blob: ae9783ca0339199e20a0026a3c0b686a035d637b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
|
# 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.
[cdcl]: https://en.wikipedia.org/wiki/Conflict-Driven_Clause_Learning
[cnf]: https://en.wikipedia.org/wiki/Conjunctive_normal_form
This is the library version. Varisat is also available as a command line solver
([`varisat-cli` on crates.io][crate-varisat-cli]).
## Documentation
* [User Manual](https://jix.github.io/varisat/manual/0.2.1/)
* [Library API Documentation](https://docs.rs/varisat/0.2.2/varisat/)
## Developer Documentation
The internal APIs are documented using rustdoc. It can be generated using
`cargo doc --document-private-items --all --exclude varisat-cli` or [viewed
online (master)][dev-docs].
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
|
