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.