unsat

An implementation of the O_SAT and O_UNSAT oracles. These oracles cannot exist. They do now.

Efficient Explaining CSPs with Unsatisfiable Subset Optimization

SAT Solver

Verifies SAT solver output. Uses drat-trim proof checker for UNSAT instances.

MaxSAT Solver

SAT and MaxSAT Solver

Counts minimally unsatisfiable (MU) k-SAT formulas via brute-force enumeration, and via a closed-form formula for 2-SAT. An MU formula is an unsatisfiable CNF where removing any single clause restores satisfiability — equivalently, a formula that is its own Minimal Unsatisfiable Subset (MUS).

SAT solver using CDCL procedure and watched literals, VSIDS herustics.