picosat

PicoSAT solves the SAT problem, which is the classical NP-complete problem of searching for a satisfying assignment of a propositional formula in conjunctive normal form (CNF). PicoSAT can generate proofs and cores in memory by compressing the proof trace. It supports the proof format of TraceCheck.