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.
Proof checker for Varisat proofs.
DIMCAS CNF parser and writer.
Literals and variables.
Boolean satisfiability solver.
A formula in conjunctive normal form (CNF).
A boolean literal.
A boolean variable.
Proof formats that can be generated during solving.
Extend a formula with new variables and clauses.