cat _posts/2026-08-30-cdclkit-a-readable-cdcl-sat-solver-where-every-answer-comes-with-a-certificate.md
cdclkit: a readable CDCL SAT solver where every answer comes with a certificate
cdclkit is a new public CDCL SAT solver, preprocessor and encoding library, written from scratch in readable Python with an optional Rust engine (roughly 18x faster) shipped as cdclkit-native. Every answer comes with a certificate: a satisfying model is re-evaluated clause by clause, and an UNSAT answer emits a DRAT proof that an independent checker replays. It publishes on PyPI with no third-party code, and the tutorial walks one problem end to end, from DIMACS through the files between stages.