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

analyze_conflict	Learns a new clause by analyzing a conflict.
assumptions	Incremental solving.
binary	Binary clauses.
cdcl	Conflict driven clause learning.
checker	Proof checker for Varisat proofs.
clause	Clause storage.
cnf	CNF formulas.
config	Solver configuration.
context	Central solver data structure.
decision	Decision heuristics.
dimacs	DIMCAS CNF parser and writer.
glue	Compute glue levels of clauses.
lit	Literals and variables.
load	Loading a formula into the solver.
model	Global model reconstruction
proof	Proof generation.
prop	Unit propagation.
schedule	Scheduling of processing and solving steps.
solver	Boolean satisfiability solver.
state	Miscellaneous solver state.
tmp	Temporary data.
unit_simplify	Simplification using unit clauses.
variables	Variable mapping and metadata.

Macros

cnf	Shortcut for tests
lit	Shortcut for tests

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.