Polynomial-time many-one reductions

PolyTimeReducible encA encB A B: a function computable in polynomial time with respect to the encodings encA and encB maps instances of A to instances of B, preserving membership Arora and Barak, Definition 2.7. It is, by definition, the many-one reducibility Cslib.Complexity.ManyOneReducibleBy by maps computable in polynomial time (Cslib.Complexity.polyTimeReducible_iff_manyOneReducibleBy), and its preorder and complement lemmas are instances of the core's. Its body is kept as the ∃ statement, so that the admissibility goal of an anonymous constructor is ComputableInPolyTime f encA encB itself, as fun_prop expects. The checked client in CslibFrontierTests.NPCompleteness supplies plain decider, verifier and reduction certificates, then transfers IndependentSet hardness to Clique.

A class of problems is given, as NP or coNP, by a set of problems for every type of instances and every encoding of them. A problem B is hard for such a class C when every problem in C, with any encoding of its instances, reduces to B (PolyTimeHard C encB B), and complete when it also belongs to C (PolyTimeComplete C encB B), the instances of Cslib.Complexity.HardUnder and Cslib.Complexity.CompleteUnder for PolyTimeReducible. The second conjunct of PolyTimeComplete is stated as PolyTimeHard, so that its projection keeps the PolyTimeHard API. NPHard, NPComplete, coNPHard and coNPComplete are the instances for NP and coNP. When the problems of a class D are the complements of those of C, the complement of a C-complete problem is D-complete (PolyTimeComplete.compl).

Hardness quantifies over problems whose instances live in Type, with every encoding of instances. Instances of complexity-theoretic problems are finite objects encoded as words, so this loses nothing: a problem in a higher universe is equivalent, through its encoding, to the problem of recognising the encodings of its members.

Mathlib's ManyOneReducible (Mathlib/Computability/Reduce.lean) is the computable, not the polynomial-time, reducibility, and is stated for Primcodable types; it is not reused here.

Finding a proved NP-complete problem

The declarations below give the exact problems, encodings and hypotheses; follow their source module to import a result. Names in this table are relative to Cslib.Complexity. For example, import CslibFrontier.Computability.Complexity.Problems.Clique to use Clique_npComplete and polyTimeReducible_IndependentSet_Clique. Cook–Levin's CookLevin.SAT_npHard reduces every NP problem to SAT. These are navigation tables, not an exhaustive list of reductions or classes.

Problem	NP-completeness declaration
CNF satisfiability (Cook–Levin)	CookLevin.SAT_npComplete
At most three literals per clause	ThreeSAT_npComplete
Exactly three literals, repetitions allowed	ExactThreeSAT_npComplete
Exactly three distinct variables per clause	EUThreeSAT_npComplete
Not-all-equal SAT, clause width at most three	NAEThreeSAT_npComplete
NAE EU3SAT, exactly three distinct variables per clause	NAEEUThreeSAT_npComplete
Not-all-equal SAT, width and variable occurrences at most three	NAEThreeSATThree_npComplete
Boolean circuit satisfiability	CircuitSAT_npComplete
Independent set	IndependentSet_npComplete
Clique	Clique_npComplete
Vertex cover	VertexCover_npComplete
Three-colorability	ThreeColoring_npComplete
Fixed k-colorability, 3 ≤ k	KColoring_npComplete
Chromatic number, k in the input	ChromaticNumber_npComplete
Clique cover	CliqueCover_npComplete
Directed feedback vertex set (Karp's feedback node set)	FeedbackVertexSet_npComplete
Feedback arc set	FeedbackArcSet_npComplete
Directed Hamiltonian path, specified endpoints	DirHamPath_npComplete
Directed Hamiltonian cycle	DirHamCycle_npComplete
Undirected Hamiltonian path, specified endpoints	HamPath_npComplete
Undirected Hamiltonian cycle	HamCycle_npComplete
Subset sum	SubsetSum_npComplete
Partition	Partition_npComplete
Knapsack	Knapsack_npComplete
Weighted maximum cut	MaxCut_npComplete
Sequencing with deadlines and penalties	JobSequencing_npComplete
Zero-one integer programming	ZeroOneIP_npComplete
Traveling salesperson	TSP_npComplete

Source → target	Reduction declaration
SAT → ThreeSAT	polyTimeReducible_SAT_ThreeSAT
ThreeSAT → ExactThreeSAT	polyTimeReducible_ThreeSAT_ExactThreeSAT
SAT → CircuitSAT	SAT.polyTimeReducible_CircuitSAT
SAT → IndependentSet	polyTimeReducible_SAT_IndependentSet
IndependentSet → Clique	polyTimeReducible_IndependentSet_Clique
Clique → IndependentSet	polyTimeReducible_Clique_IndependentSet
IndependentSet → VertexCover	polyTimeReducible_IndependentSet_VertexCover
VertexCover → FeedbackVertexSet	polyTimeReducible_VertexCover_FeedbackVertexSet
FeedbackVertexSet → FeedbackArcSet	polyTimeReducible_FeedbackVertexSet_FeedbackArcSet
SAT → ThreeColoring	polyTimeReducible_SAT_ThreeColoring
ThreeSAT → ThreeColoring	polyTimeReducible_ThreeSAT_ThreeColoring
SAT → KColoring k, for 3 ≤ k	polyTimeReducible_SAT_KColoring
KColoring k → ChromaticNumber	polyTimeReducible_KColoring_ChromaticNumber
ChromaticNumber → CliqueCover	polyTimeReducible_ChromaticNumber_CliqueCover
SAT → DirHamPath	polyTimeReducible_SAT_DirHamPath
ThreeSAT → DirHamPath	polyTimeReducible_ThreeSAT_DirHamPath
SAT → DirHamCycle	polyTimeReducible_SAT_DirHamCycle
DirHamPath → HamPath	polyTimeReducible_DirHamPath_HamPath
DirHamCycle → HamCycle	polyTimeReducible_DirHamCycle_HamCycle
ThreeSAT → SubsetSum	polyTimeReducible_ThreeSAT_SubsetSum
SubsetSum → Partition	polyTimeReducible_SubsetSum_Partition
SubsetSum → Knapsack	polyTimeReducible_SubsetSum_Knapsack
SubsetSum → JobSequencing	polyTimeReducible_SubsetSum_JobSequencing
Partition → MaxCut	polyTimeReducible_Partition_MaxCut
SubsetSum → ZeroOneIP	polyTimeReducible_SubsetSum_ZeroOneIP
ThreeSAT → ZeroOneIP	polyTimeReducible_ThreeSAT_ZeroOneIP
HamCycle → TSP	polyTimeReducible_HamCycle_TSP

Main definitions

• Cslib.Complexity.PolyTimeReducible.
• Cslib.Complexity.PolyTimeHard, Cslib.Complexity.PolyTimeComplete: hardness and completeness for a class.
• Cslib.Complexity.NPHard, Cslib.Complexity.NPComplete.
• Cslib.Complexity.coNPHard, Cslib.Complexity.coNPComplete.

Main results

• Cslib.Complexity.P_subset_NP, Cslib.Complexity.P_subset_coNP: P is contained in NP and in coNP.
• Cslib.Complexity.NPComplete.P_eq_NP_of_mem_P, Cslib.Complexity.NPComplete.mem_P_iff: an NP-complete problem is in P exactly when P = NP for every encoding.
• Cslib.Complexity.NPComplete.mem_P_iff_mem_P: two NP-complete problems are both in P or both outside it.
• Cslib.Complexity.PolyTimeReducible.refl, Cslib.Complexity.PolyTimeReducible.trans: polynomial-time reducibility is a preorder.
• Cslib.Complexity.PolyTimeReducible.mem_P: P is closed under polynomial-time reductions.
• Cslib.Complexity.PolyTimeHard.trans, Cslib.Complexity.NPHard.trans, Cslib.Complexity.coNPHard.trans: hardness transfers along polynomial-time reductions.
• Cslib.Complexity.PolyTimeReducible.compl: a reduction between problems is one between their complements.
• Cslib.Complexity.PolyTimeHard.compl, Cslib.Complexity.PolyTimeComplete.compl: complements of hard and complete problems.
• Cslib.Complexity.NPHard.compl, Cslib.Complexity.coNPHard.compl, Cslib.Complexity.NPComplete.compl, Cslib.Complexity.coNPComplete.compl: complements exchange hardness and completeness for NP and coNP.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach

def Cslib.Complexity.PolyTimeReducible {α : Type u_1} {β : Type u_2} (encA : α ↪ List Bool) (encB : β ↪ List Bool) (A : Set α) (B : Set β) : Prop

A reduces to B in polynomial time: some f, computable in polynomial time with respect to encA and encB, satisfies a ∈ A ↔ f a ∈ B. This is ManyOneReducibleBy for the maps computable in polynomial time (polyTimeReducible_iff_manyOneReducibleBy).

Construct a proof as ⟨f, by fun_prop, h⟩, where h proves the membership equivalence for every source instance. Write f with certified Boolean, list and arithmetic operations, including decide of connectives, (in)equalities and list membership; unfold local definitions so fun_prop can see them. Cost and correctness are separate obligations: automation does not prove h. See the checked graph-complement example in CslibFrontierTests.NPCompleteness.

theorem Cslib.Complexity.polyTimeReducible_iff_manyOneReducibleBy {α : Type u_1} {β : Type u_2} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {A : Set α} {B : Set β} : PolyTimeReducible encA encB A B ↔ ManyOneReducibleBy (fun (x : α → β) => Turing.MultiTapeTM.ComputableInPolyTime x encA encB) A B

Polynomial-time reducibility is many-one reducibility by the maps computable in polynomial time.

def Cslib.Complexity.PolyTimeHard {β : Type u_2} (C : {α : Type} → (α ↪ List Bool) → Set (Set α)) (encB : β ↪ List Bool) (B : Set β) : Prop

B is hard for the class C under polynomial-time many-one reductions: every problem in C, with any encoding of its instances, reduces to B. This is HardUnder for PolyTimeReducible.

def Cslib.Complexity.PolyTimeComplete {β : Type} (C : {α : Type} → (α ↪ List Bool) → Set (Set α)) (encB : β ↪ List Bool) (B : Set β) : Prop

B is complete for the class C under polynomial-time many-one reductions: it is in C and every problem in C reduces to it. This is CompleteUnder for PolyTimeReducible (polyTimeComplete_iff_completeUnder), with its second conjunct stated as PolyTimeHard.

theorem Cslib.Complexity.polyTimeHard_iff_hardUnder {β : Type u_2} {C : {α : Type} → (α ↪ List Bool) → Set (Set α)} {encB : β ↪ List Bool} {B : Set β} : PolyTimeHard (fun {α : Type} => C) encB B ↔ HardUnder (fun {α : Type} (enc : α ↪ List Bool) => PolyTimeReducible enc encB) C B

Polynomial-time hardness is hardness under PolyTimeReducible.

theorem Cslib.Complexity.polyTimeComplete_iff_completeUnder {β : Type} {C : {α : Type} → (α ↪ List Bool) → Set (Set α)} {encB : β ↪ List Bool} {B : Set β} : PolyTimeComplete (fun {α : Type} => C) encB B ↔ CompleteUnder (fun {α : Type} (enc : α ↪ List Bool) => PolyTimeReducible enc encB) C encB B

Polynomial-time completeness is completeness under PolyTimeReducible.

@[reducible, inline]

abbrev Cslib.Complexity.NPHard {β : Type u_2} (encB : β ↪ List Bool) (B : Set β) : Prop

Every problem in NP, with any encoding of its instances, reduces to B.

@[reducible, inline]

abbrev Cslib.Complexity.NPComplete {β : Type} (encB : β ↪ List Bool) (B : Set β) : Prop

B is in NP and every problem in NP reduces to it.

@[reducible, inline]

abbrev Cslib.Complexity.coNPHard {β : Type u_2} (encB : β ↪ List Bool) (B : Set β) : Prop

Every problem in coNP, with any encoding of its instances, reduces to B.

@[reducible, inline]

abbrev Cslib.Complexity.coNPComplete {β : Type} (encB : β ↪ List Bool) (B : Set β) : Prop

B is in coNP and every problem in coNP reduces to it.

theorem Cslib.Complexity.polyTimeHard_NP_iff {β : Type u_2} {encB : β ↪ List Bool} {B : Set β} : PolyTimeHard (@NP) encB B ↔ NPHard encB B

Hardness for the class NP is NPHard.

theorem Cslib.Complexity.polyTimeComplete_NP_iff {β : Type} {encB : β ↪ List Bool} {B : Set β} : PolyTimeComplete (@NP) encB B ↔ NPComplete encB B

Completeness for the class NP is NPComplete.

theorem Cslib.Complexity.polyTimeHard_coNP_iff {β : Type u_2} {encB : β ↪ List Bool} {B : Set β} : PolyTimeHard (@coNP) encB B ↔ coNPHard encB B

Hardness for the class coNP is coNPHard.

theorem Cslib.Complexity.polyTimeComplete_coNP_iff {β : Type} {encB : β ↪ List Bool} {B : Set β} : PolyTimeComplete (@coNP) encB B ↔ coNPComplete encB B

Completeness for the class coNP is coNPComplete.

theorem Cslib.Complexity.PolyTimeReducible.refl {α : Type u_1} (encA : α ↪ List Bool) (A : Set α) : PolyTimeReducible encA encA A A

Every problem reduces to itself in polynomial time by the identity function.

theorem Cslib.Complexity.PolyTimeReducible.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} {A : Set α} {B : Set β} {C : Set γ} (hAB : PolyTimeReducible encA encB A B) (hBC : PolyTimeReducible encB encC B C) : PolyTimeReducible encA encC A C

Polynomial-time many-one reductions compose.

theorem Cslib.Complexity.PolyTimeReducible.mem_P {α : Type u_1} {β : Type u_2} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {A : Set α} {B : Set β} (hAB : PolyTimeReducible encA encB A B) (hB : B ∈ P encB) : A ∈ P encA

P is closed under polynomial-time reductions.

theorem Cslib.Complexity.PolyTimeReducible.compl {α : Type u_1} {β : Type u_2} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {A : Set α} {B : Set β} (h : PolyTimeReducible encA encB A B) : PolyTimeReducible encA encB Aᶜ Bᶜ

A reduction from A to B is also a reduction from Aᶜ to Bᶜ.

theorem Cslib.Complexity.PolyTimeReducible.mem_compl {α : Type u_1} {β : Type u_2} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {A : Set α} {B : Set β} {C : Set (Set α)} {D : Set (Set β)} (hCD : ∀ {A : Set α} {B : Set β}, PolyTimeReducible encA encB A B → B ∈ D → A ∈ C) (h : PolyTimeReducible encA encB A B) (hB : Bᶜ ∈ D) : Aᶜ ∈ C

If polynomial-time reductions preserve membership from D to C, they also preserve membership in the complement classes {B | Bᶜ ∈ D} and {A | Aᶜ ∈ C}.

theorem Cslib.Complexity.PolyTimeReducible.mappingReducible {α : Type u_1} {β : Type u_2} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {A : Set α} {B : Set β} (h : PolyTimeReducible encA encB A B) : Turing.MultiTapeTM.MappingReducible encA encB A B

A polynomial-time reduction is a mapping reduction.

theorem Cslib.Complexity.PolyTimeHard.trans {β : Type u_2} {γ : Type u_3} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} {B : Set β} {C : Set γ} {𝒞 : {α : Type} → (α ↪ List Bool) → Set (Set α)} (hB : PolyTimeHard (fun {α : Type} => 𝒞) encB B) (hBC : PolyTimeReducible encB encC B C) : PolyTimeHard (fun {α : Type} => 𝒞) encC C

Hardness transfers along a polynomial-time reduction.

theorem Cslib.Complexity.PolyTimeHard.compl {β : Type u_2} {encB : β ↪ List Bool} {B : Set β} {𝒞 𝒟 : {α : Type} → (α ↪ List Bool) → Set (Set α)} (h𝒟𝒞 : ∀ {α : Type} (enc : α ↪ List Bool), ∀ A ∈ 𝒟 enc, Aᶜ ∈ 𝒞 enc) (hB : PolyTimeHard (fun {α : Type} => 𝒞) encB B) : PolyTimeHard (fun {α : Type} => 𝒟) encB Bᶜ

If the complement of every problem in 𝒟 is in 𝒞, the complement of a 𝒞-hard problem is 𝒟-hard.

theorem Cslib.Complexity.PolyTimeComplete.compl {𝒞 𝒟 : {α : Type} → (α ↪ List Bool) → Set (Set α)} {β : Type} {encB : β ↪ List Bool} {B : Set β} (h𝒟𝒞 : ∀ {α : Type} (enc : α ↪ List Bool) (A : Set α), A ∈ 𝒟 enc ↔ Aᶜ ∈ 𝒞 enc) (hB : PolyTimeComplete (fun {α : Type} => 𝒞) encB B) : PolyTimeComplete (fun {α : Type} => 𝒟) encB Bᶜ

If the problems in 𝒟 are exactly the complements of the problems in 𝒞, the complement of a 𝒞-complete problem is 𝒟-complete.

theorem Cslib.Complexity.NPHard.trans {α : Type u_1} {β : Type u_2} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {A : Set α} {B : Set β} (hA : NPHard encA A) (hAB : PolyTimeReducible encA encB A B) : NPHard encB B

NP-hardness transfers along a polynomial-time reduction.

theorem Cslib.Complexity.coNPHard.trans {α : Type u_1} {β : Type u_2} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {A : Set α} {B : Set β} (hA : coNPHard encA A) (hAB : PolyTimeReducible encA encB A B) : coNPHard encB B

coNP-hardness transfers along a polynomial-time reduction.

theorem Cslib.Complexity.NPHard.compl {β : Type u_2} {encB : β ↪ List Bool} {B : Set β} (h : NPHard encB B) : coNPHard encB Bᶜ

The complement of an NP-hard problem is coNP-hard.

theorem Cslib.Complexity.coNPHard.compl {β : Type u_2} {encB : β ↪ List Bool} {B : Set β} (h : coNPHard encB B) : NPHard encB Bᶜ

The complement of a coNP-hard problem is NP-hard.

theorem Cslib.Complexity.NPComplete.compl {β : Type} {encB : β ↪ List Bool} {B : Set β} (h : NPComplete encB B) : coNPComplete encB Bᶜ

The complement of an NP-complete problem is coNP-complete.

theorem Cslib.Complexity.coNPComplete.compl {β : Type} {encB : β ↪ List Bool} {B : Set β} (h : coNPComplete encB B) : NPComplete encB Bᶜ

The complement of a coNP-complete problem is NP-complete.

P and NP-complete problems

theorem Cslib.Complexity.P_subset_NP {α : Type} {enc : α ↪ List Bool} : P enc ⊆ NP enc

P ⊆ NP: a decider is a verifier ignoring its certificate.

theorem Cslib.Complexity.P_subset_coNP {α : Type} {enc : α ↪ List Bool} : P enc ⊆ coNP enc

P ⊆ coNP: P is closed under complement.

theorem Cslib.Complexity.NPComplete.P_eq_NP_of_mem_P {β : Type} {encB : β ↪ List Bool} {B : Set β} (hB : NPComplete encB B) (h : B ∈ P encB) {α : Type} (enc : α ↪ List Bool) : P enc = NP enc

An NP-complete problem in P gives P = NP, for every encoding of instances: every problem in NP reduces to it, and P is closed under polynomial-time reductions.

theorem Cslib.Complexity.NPComplete.mem_P_iff {β : Type} {encB : β ↪ List Bool} {B : Set β} (hB : NPComplete encB B) : B ∈ P encB ↔ ∀ {α : Type} (enc : α ↪ List Bool), P enc = NP enc

An NP-complete problem is in P exactly when P = NP, for every encoding of instances.

theorem Cslib.Complexity.NPComplete.mem_P_iff_mem_P {β γ : Type} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} {B : Set β} {C : Set γ} (hB : NPComplete encB B) (hC : NPComplete encC C) : B ∈ P encB ↔ C ∈ P encC

Two NP-complete problems are both in P or both outside it.