Certified frame-first SAT middleware — decide structured regions (2-SAT · GF(2) parity · counting) before CDCL, and independently verify every verdict (model replay · DRAT). A research harness for where SAT hardness lives.
python lambda-calculus sat-solver formal-verification drat computational-complexity boolean-satisfiability proof-checking satisfiability cdcl cryptominisat constraint-solving kissat nullstellensatz certified-solving resolution-width
-
Updated
Aug 29, 2026 - Python