Deterministic reductions of promise problems and gap problems

Hardness of approximation is stated through gap problems Arora and Barak, Chapter 11. For a maximization objective val, the gap problem gapMax val c s is the promise problem whose yes-instances have value at least c and whose no-instances have value at most s, below c. When this gap problem is NP-hard, the maximization problem is NP-hard to approximate within every ratio better than s / c: an algorithm estimating val from below within such a ratio would tell the two kinds of instances apart.

Reductions between promise problems are the polynomial-time many-one reductions of Cslib.Complexity.PolyTimeReducible, required to map yes-instances to yes-instances and no-instances to no-instances; on decision problems they are exactly those reductions (PromiseProblem.polyTimeReducible_ofSet_iff). Between gap problems they are the gap-preserving reductions used to transfer inapproximability from one problem to another. A promise problem is NP-hard when every problem in NP reduces to it; for decision problems this is Cslib.Complexity.NPHard (PromiseProblem.npHard_ofSet_iff). An NP-hard promise problem solved in polynomial time gives P = NP (PromiseProblem.NPHard.P_eq_NP_of_mem_PromiseP).

Reductions of promise problems are Karp reductions in the sense of Goldreich's survey [Gol06]: one function serves for every instance in the promise. This is stronger than asking every problem separating the yes-instances from the no-instances to be NP-hard, which PromiseProblem.NPHard.npHard_of_subset derives.

Probabilistic promise classes are defined with their decision specializations: PromiseBPP in CslibFrontier.Computability.Complexity.Classes.BPP, and PromiseRP and PromiseCoRP in CslibFrontier.Computability.Complexity.Classes.RP. Their PPT characterizations live in CslibFrontier.Computability.Complexity.Classes.Promise.Probabilistic, and randomized one-sided reductions (RPReducible, RPReducibleWithError) live in CslibFrontier.Computability.Complexity.Classes.Promise.Randomized.

Main definitions

• Cslib.Complexity.PromiseProblem.PolyTimeReducible: polynomial-time reductions of promise problems, which between gap problems are the gap-preserving reductions.
• Cslib.Complexity.PromiseProblem.NPHard: every problem in NP reduces to the promise problem.
• Cslib.Complexity.PromiseProblem.gapMax, Cslib.Complexity.PromiseProblem.gapMin: the gap problems of a maximization and of a minimization objective.
• Cslib.Complexity.PromiseProblem.restrict: a promise problem restricted to a set of instances.

Main results

• Cslib.Complexity.PromiseProblem.polyTimeReducible_ofSet_iff, Cslib.Complexity.PromiseProblem.npHard_ofSet_iff: on decision problems, the notions are Cslib.Complexity.PolyTimeReducible and Cslib.Complexity.NPHard.
• Cslib.Complexity.PromiseProblem.PolyTimeReducible.refl, Cslib.Complexity.PromiseProblem.PolyTimeReducible.trans, Cslib.Complexity.PromiseProblem.PolyTimeReducible.of_subset, Cslib.Complexity.PromiseProblem.NPHard.trans, Cslib.Complexity.PromiseProblem.NPHard.mono: reflexivity, composition and monotonicity of promise reductions and NP-hardness.
• Cslib.Complexity.PromiseProblem.PolyTimeReducible.mem_PromiseP, Cslib.Complexity.PromiseProblem.PolyTimeReducible.mem_PromiseNP, Cslib.Complexity.PromiseProblem.PolyTimeReducible.exists_polyTimeReducible: closure of PromiseP and PromiseNP under deterministic reductions.
• Cslib.Complexity.PromiseProblem.npHard_of_polyTimeReducible_SAT: a reduction from SAT proves NP-hardness, by the Cook–Levin theorem.
• Cslib.Complexity.PromiseProblem.NPHard.npHard_of_subset, Cslib.Complexity.PromiseProblem.NPHard.NP_subset_P_of_mem_PromiseP, Cslib.Complexity.PromiseProblem.NPHard.P_eq_NP_of_mem_PromiseP, Cslib.Complexity.PromiseProblem.NPHard.notMem_PromiseP: consequences of NP-hardness for separating languages and P vs NP.
• Cslib.Complexity.PromiseProblem.mem_no_gapMax_of_lt, Cslib.Complexity.PromiseProblem.mem_no_gapMin_of_lt: characterization of no-instances of gap problems when the soundness and completeness thresholds are strictly separated.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Chapter 11
• S. Even, A. Selman, Y. Yacobi, The complexity of promise problems with applications to public-key cryptography
• O. Goldreich, On promise problems: a survey

Reductions

def Cslib.Complexity.PromiseProblem.PolyTimeReducible {α : Type u_1} {β : Type u_2} (encA : α ↪ List Bool) (encB : β ↪ List Bool) (X : PromiseProblem α) (Y : PromiseProblem β) : Prop

A polynomial-time reduction of promise problems from X to Y: a function computable in polynomial time with respect to encA and encB mapping the yes-instances of X to yes-instances of Y and its no-instances to no-instances of Y. Instances outside the promise of X may go anywhere. Between gap problems these are the gap-preserving reductions.

theorem Cslib.Complexity.PromiseProblem.polyTimeReducible_ofSet_iff {α : Type u_1} {β : Type u_2} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {A : Set α} {B : Set β} : PolyTimeReducible encA encB (ofSet A) (ofSet B) ↔ Complexity.PolyTimeReducible encA encB A B

On decision problems, reductions of promise problems are polynomial-time reductions.

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

Every promise problem reduces to itself.

theorem Cslib.Complexity.PromiseProblem.PolyTimeReducible.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} {X : PromiseProblem α} {Y : PromiseProblem β} {Z : PromiseProblem γ} (hXY : PolyTimeReducible encA encB X Y) (hYZ : PolyTimeReducible encB encC Y Z) : PolyTimeReducible encA encC X Z

Reductions of promise problems compose.

theorem Cslib.Complexity.PromiseProblem.PolyTimeReducible.of_subset {β : Type u_2} {encB : β ↪ List Bool} {Y Y' : PromiseProblem β} (hyes : Y.yes ⊆ Y'.yes) (hno : Y.no ⊆ Y'.no) : PolyTimeReducible encB encB Y Y'

A promise problem reduces, by the identity, to any problem with more yes-instances and more no-instances: enlarging the promise can only make a problem harder.

theorem Cslib.Complexity.PromiseProblem.PolyTimeReducible.mem_PromiseP {α : Type u_1} {β : Type u_2} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {X : PromiseProblem α} {Y : PromiseProblem β} (h : PolyTimeReducible encA encB X Y) (hY : Y ∈ PromiseP encB) : X ∈ PromiseP encA

PromiseP is closed under reductions.

theorem Cslib.Complexity.PromiseProblem.PolyTimeReducible.exists_polyTimeReducible {α : Type u_1} {β : Type u_2} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {X : PromiseProblem α} {Y : PromiseProblem β} (h : PolyTimeReducible encA encB X Y) {B : Set β} (hyes : Y.yes ⊆ B) (hno : Disjoint B Y.no) : ∃ (A : Set α), X.yes ⊆ A ∧ Disjoint A X.no ∧ Complexity.PolyTimeReducible encA encB A B

A reduction of promise problems restricts to a polynomial-time reduction between the problems that separate them: for every problem B containing the yes-instances of Y and no no-instance, its preimage separates X and reduces to B.

theorem Cslib.Complexity.PromiseProblem.PolyTimeReducible.mem_PromiseNP {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {X : PromiseProblem α} {Y : PromiseProblem β} (h : PolyTimeReducible encA encB X Y) (hY : Y ∈ PromiseNP encB) : X ∈ PromiseNP encA

PromiseNP is closed under polynomial-time reductions.

NP-hardness

def Cslib.Complexity.PromiseProblem.NPHard {β : Type u_2} (encB : β ↪ List Bool) (Y : PromiseProblem β) : Prop

A promise problem is NP-hard when every problem in NP, with any encoding of its instances, reduces to it: some polynomial-time function maps its members to yes-instances and its non-members to no-instances. This is HardUnder for PolyTimeReducible from ofSet.

theorem Cslib.Complexity.PromiseProblem.npHard_iff_hardUnder {β : Type u_2} {encB : β ↪ List Bool} {Y : PromiseProblem β} : NPHard encB Y ↔ HardUnder (fun {α : Type} (enc : α ↪ List Bool) (A : Set α) (Y : PromiseProblem β) => PolyTimeReducible enc encB (ofSet A) Y) (@NP) Y

NP-hardness of a promise problem is hardness for NP under PolyTimeReducible from ofSet.

theorem Cslib.Complexity.PromiseProblem.npHard_ofSet_iff {β : Type u_2} {encB : β ↪ List Bool} {B : Set β} : NPHard encB (ofSet B) ↔ Complexity.NPHard encB B

On decision problems, NP-hardness as a promise problem is Cslib.Complexity.NPHard.

theorem Cslib.Complexity.PromiseProblem.NPHard.trans {α : Type u_1} {β : Type u_2} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {X : PromiseProblem α} {Y : PromiseProblem β} (hX : NPHard encA X) (h : PolyTimeReducible encA encB X Y) : NPHard encB Y

NP-hardness transfers along reductions.

theorem Cslib.Complexity.PromiseProblem.NPHard.mono {β : Type u_2} {encB : β ↪ List Bool} {Y Y' : PromiseProblem β} (hY : NPHard encB Y) (hyes : Y.yes ⊆ Y'.yes) (hno : Y.no ⊆ Y'.no) : NPHard encB Y'

Enlarging the promise preserves NP-hardness.

theorem Cslib.Complexity.PromiseProblem.npHard_of_polyTimeReducible_SAT {β : Type u_2} {encB : β ↪ List Bool} {Y : PromiseProblem β} (h : PolyTimeReducible encCNF encB (ofSet SAT) Y) : NPHard encB Y

A reduction from SAT proves NP-hardness, by the Cook–Levin theorem.

theorem Cslib.Complexity.PromiseProblem.NPHard.npHard_of_subset {β : Type u_2} {encB : β ↪ List Bool} {Y : PromiseProblem β} (hY : NPHard encB Y) {B : Set β} (hyes : Y.yes ⊆ B) (hno : Disjoint B Y.no) : Complexity.NPHard encB B

Every problem separating the yes-instances of an NP-hard promise problem from its no-instances is NP-hard.

theorem Cslib.Complexity.PromiseProblem.NPHard.NP_subset_P_of_mem_PromiseP {β : Type u_2} {encB : β ↪ List Bool} {Y : PromiseProblem β} (hY : NPHard encB Y) (h : Y ∈ PromiseP encB) {α : Type} (enc : α ↪ List Bool) : NP enc ⊆ P enc

If an NP-hard promise problem is solved in polynomial time, then NP ⊆ P for every encoding of instances.

theorem Cslib.Complexity.PromiseProblem.NPHard.P_eq_NP_of_mem_PromiseP {β : Type u_2} {encB : β ↪ List Bool} {Y : PromiseProblem β} (hY : NPHard encB Y) (h : Y ∈ PromiseP encB) {α : Type} (enc : α ↪ List Bool) : P enc = NP enc

An NP-hard promise problem solved in polynomial time gives P = NP, for every encoding of instances.

theorem Cslib.Complexity.PromiseProblem.NPHard.notMem_PromiseP {β : Type u_2} {encB : β ↪ List Bool} {Y : PromiseProblem β} (hY : NPHard encB Y) {α : Type} {enc : α ↪ List Bool} (h : P enc ≠ NP enc) : Y ∉ PromiseP encB

If P ≠ NP for some encoding, no NP-hard promise problem is solved in polynomial time.

Gap problems

def Cslib.Complexity.PromiseProblem.gapMax {α : Type u_1} (val c s : α → ℝ) : PromiseProblem α

The gap problem of a maximization objective val, with completeness threshold c and soundness threshold s: the yes-instances have value at least c, the no-instances value at most s, below c. The thresholds may depend on the instance; an instance with c x ≤ s x is not a no-instance, so that the two sets are disjoint.

@[simp]

theorem Cslib.Complexity.PromiseProblem.mem_yes_gapMax {α : Type u_1} {val c s : α → ℝ} {x : α} : x ∈ (gapMax val c s).yes ↔ c x ≤ val x

@[simp]

theorem Cslib.Complexity.PromiseProblem.mem_no_gapMax {α : Type u_1} {val c s : α → ℝ} {x : α} : x ∈ (gapMax val c s).no ↔ val x ≤ s x ∧ s x < c x

theorem Cslib.Complexity.PromiseProblem.mem_no_gapMax_of_lt {α : Type u_1} {val c s : α → ℝ} {x : α} (h : s x < c x) : x ∈ (gapMax val c s).no ↔ val x ≤ s x

With a strictly smaller soundness threshold, the no-instances are those of value at most s.

def Cslib.Complexity.PromiseProblem.gapMin {α : Type u_1} (val c s : α → ℝ) : PromiseProblem α

The gap problem of a minimization objective val, with completeness threshold c and soundness threshold s: the yes-instances have value at most c, the no-instances value at least s, above c. The thresholds may depend on the instance; an instance with s x ≤ c x is not a no-instance, so that the two sets are disjoint.

@[simp]

theorem Cslib.Complexity.PromiseProblem.mem_yes_gapMin {α : Type u_1} {val c s : α → ℝ} {x : α} : x ∈ (gapMin val c s).yes ↔ val x ≤ c x

@[simp]

theorem Cslib.Complexity.PromiseProblem.mem_no_gapMin {α : Type u_1} {val c s : α → ℝ} {x : α} : x ∈ (gapMin val c s).no ↔ s x ≤ val x ∧ c x < s x

theorem Cslib.Complexity.PromiseProblem.mem_no_gapMin_of_lt {α : Type u_1} {val c s : α → ℝ} {x : α} (h : c x < s x) : x ∈ (gapMin val c s).no ↔ s x ≤ val x

With a strictly larger soundness threshold, the no-instances are those of value at least s.

def Cslib.Complexity.PromiseProblem.restrict {α : Type u_1} (Q : PromiseProblem α) (S : Set α) : PromiseProblem α

The promise problem Q with its promise restricted to the instances in S.

@[simp]

theorem Cslib.Complexity.PromiseProblem.yes_restrict {α : Type u_1} (Q : PromiseProblem α) (S : Set α) : (Q.restrict S).yes = Q.yes ∩ S

@[simp]

theorem Cslib.Complexity.PromiseProblem.no_restrict {α : Type u_1} (Q : PromiseProblem α) (S : Set α) : (Q.restrict S).no = Q.no ∩ S