[−][src]Crate varisat
Varisat is a CDCL based SAT solver written in 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.
In addition to this API documentation, Varisat comes with a user manual.
Re-exports
pub use solver::Solver; |
Modules
checker | Proof checker for Varisat proofs. |
cnf | CNF formulas. |
config | Solver configuration. |
dimacs | DIMCAS CNF parser and writer. |
lit | Literals and variables. |
solver | Boolean satisfiability solver. |
Structs
CnfFormula | A formula in conjunctive normal form (CNF). |
Lit | A boolean literal. |
Var | A boolean variable. |
Enums
ProofFormat | Proof formats that can be generated during solving. |
Traits
ExtendFormula | Extend a formula with new variables and clauses. |