NP-completeness of 3SAT

The total Tseitin transformation is a polynomial-time many-one reduction from the existing encoded CNF-SAT language to the exact-3 language. Together with Cook--Levin and the direct proof that 3SAT belongs to NP, this gives the headline NP-completeness theorem.

Main results

• ThreeSAT.cnfsat_le_language
• ThreeSAT.NPHard_language
• ThreeSAT.NPComplete_language

theorem Complexity.SAT.ThreeSAT.cnfsat_le_language : CNFSAT.language ≤ₚ language

The total Tseitin transformation is a polynomial-time many-one reduction from encoded CNF-SAT to encoded 3SAT.

theorem Complexity.SAT.ThreeSAT.NPHard_language : NPHard language

Encoded 3SAT is NP-hard.

theorem Complexity.SAT.ThreeSAT.NPComplete_language : NPComplete language

3SAT is NP-complete.