Every NP language, as a formula

Cook--Levin and Tseitin already reduce any NP language to encoded 3SAT. What the gap reduction needs is slightly more: not a string that lies in 3SAT, but the formula itself, so that the constraint graph can be built from it.

The Tseitin reduction is total — malformed inputs go to a fixed unsatisfiable formula — so the formula is always there to be named: redCNF names it, and reduction_eq_encode says the reduction writes exactly its encoding.

Main definitions

• Complexity.redCNF — the 3CNF a string reduces to

Main results

• Complexity.exists_reduction_cnf — every NP language is the satisfiability of an FP family of 3CNFs

noncomputable def Complexity.redCNF (z : List Bool) : SAT.CNF

The exact 3-CNF that the total Tseitin reduction produces.

Equations

• Complexity.redCNF z = match Complexity.SAT.CNF.decode? z with | some φ => (Complexity.SAT.CNF.to3Aux (z.length + 1) φ).1 | none => Complexity.SAT.ThreeSAT.falseFormula

theorem Complexity.reduction_eq_encode (z : List Bool) : SAT.ThreeSAT.reduction z = (redCNF z).encode

theorem Complexity.redCNF_is3CNF (z : List Bool) : (redCNF z).Is3CNF

theorem Complexity.satisfiable_redCNF_iff (z : List Bool) : (redCNF z).Satisfiable ↔ z ∈ SAT.CNFSAT.language

theorem Complexity.exists_reduction_cnf {L : Language} (hL : L ∈ NP) : ∃ (E : List Bool → List Bool) (Φ : List Bool → SAT.CNF), E ∈ FP ∧ (∀ (x : List Bool), E x = (Φ x).encode) ∧ (∀ (x : List Bool), (Φ x).Is3CNF) ∧ ∀ (x : List Bool), x ∈ L ↔ (Φ x).Satisfiable

Every NP language is the satisfiability of an FP family of exact 3-CNFs.