Skip to content
  1. CLRS-Lean
  2. Chapter 34. NP-Completeness
  3. 34.4. NP-Completeness Proofs
  4. 34.4. Standalone SAT Certificate Semantics
Browse chapters
Imports
import CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.SAT.NPCompleteness

Standalone SAT verification and NP-completeness

This facade exposes the canonical raw assignment format, total checker, exact all-input acceptance semantics, and linear certificate bound for SAT. It also exposes a fixed polynomial-time reduction-backed verifier and the public SAT_mem_ClassNP and SAT_npComplete theorems. Compiling the smaller assignment checker itself to a fixed machine remains an optional implementation refinement.