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.
Check unsatisfiability proofs.
DIMACS CNF parsing and writing.
Literals and variables.
Boolean satisfiability solver.