The Cook–Levin theorem

The complete tableau reduction is correct and polynomial-time. Together with the certified SAT verifier, this proves that SAT is NP-complete under polynomial-time many-one reductions. Complementation gives coNP-completeness of UNSAT. No reduction-efficiency hypothesis remains in these statements.

Main results

• Cslib.Complexity.CookLevin.SAT_npHard.
• Cslib.Complexity.CookLevin.SAT_npComplete.
• Cslib.Complexity.CookLevin.UNSAT_coNPComplete.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 2.3.
• C. H. Papadimitriou, Computational Complexity, Theorem 8.2.

theorem Cslib.Complexity.CookLevin.SAT_npHard : NPHard encCNF SAT

Every NP problem reduces to SAT in polynomial time through its verifier's tableau.

theorem Cslib.Complexity.CookLevin.SAT_npComplete : NPComplete encCNF SAT

Cook–Levin: SAT is NP-complete.

theorem Cslib.Complexity.CookLevin.UNSAT_coNPComplete : coNPComplete encCNF UNSAT

UNSAT is coNP-complete under polynomial-time many-one reductions.