[][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.