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::ProofFormat;

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.

Traits

ExtendFormula

Extend a formula with new variables and clauses.