Promise problems

A promise problem is a pair of disjoint sets of instances, the yes-instances and the no-instances Even, Selman and Yacobi, Goldreich. An instance in neither set is outside the promise, and an algorithm solving the problem may answer anything on it. A decision problem A : Set α is the promise problem whose yes-instances are A and whose no-instances are Aᶜ (PromiseProblem.ofSet).

A class C of decision problems lifts to promise problems through completions: promiseClass C consists of the promise problems separated by some problem in C, one that contains every yes-instance and no no-instance. PromiseP enc and PromiseNP enc are the lifts of P enc and NP enc, and they agree with Goldreich's definitions by polynomial-time algorithms and verifiers that are only constrained on the promise (mem_PromiseP_iff, mem_PromiseNP_iff). A decision problem is in a lifted class exactly when it is in the class (ofSet_mem_promiseClass), so lifting is injective, and PromiseP enc = PromiseNP enc exactly when P enc = NP enc (PromiseP_eq_PromiseNP_iff).

Main definitions

• Cslib.Complexity.PromiseProblem, with the complement Qᶜ exchanging the yes-instances and the no-instances.
• Cslib.Complexity.PromiseProblem.ofSet: a decision problem as a promise problem.
• Cslib.Complexity.PromiseProblem.SolvedBy: a Boolean function solves a promise problem.
• Cslib.Complexity.promiseClass: the lift of a class of decision problems.
• Cslib.Complexity.PromiseP, Cslib.Complexity.PromiseNP.

Main results

• Cslib.Complexity.ofSet_mem_promiseClass, Cslib.Complexity.promiseClass_inj: lifting reflects membership and equality of classes.
• Cslib.Complexity.mem_promiseClass_iff_solvedBy: the lift of a class defined by deciding functions consists of the promise problems solved by such functions.
• Cslib.Complexity.mem_PromiseP_iff, Cslib.Complexity.mem_PromiseNP_iff: Goldreich's definitions.
• Cslib.Complexity.PromiseP_eq_PromiseNP_iff: PromiseP = PromiseNP ↔ P = NP.

References

• S. Even, A. Selman, Y. Yacobi, The complexity of promise problems with applications to public-key cryptography
• O. Goldreich, On promise problems: a survey

structure Cslib.Complexity.PromiseProblem (α : Type u_1) : Type u_1

A promise problem: disjoint sets of yes-instances and no-instances. Instances in neither set are outside the promise.

• yes : Set α

  The instances on which the answer must be yes.

• no : Set α

  The instances on which the answer must be no.

• disjoint : Disjoint self.yes self.no

  No instance is both a yes-instance and a no-instance.

theorem Cslib.Complexity.PromiseProblem.ext_iff {α : Type u_1} {x y : PromiseProblem α} : x = y ↔ x.yes = y.yes ∧ x.no = y.no

theorem Cslib.Complexity.PromiseProblem.ext {α : Type u_1} {x y : PromiseProblem α} (yes : x.yes = y.yes) (no : x.no = y.no) : x = y

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

The promise: the instances that are yes-instances or no-instances.

def Cslib.Complexity.PromiseProblem.SolvedBy {α : Type u_1} (Q : PromiseProblem α) (f : α → Bool) : Prop

f solves Q when it answers true on the yes-instances and false on the no-instances; its answers outside the promise do not matter.

def Cslib.Complexity.PromiseProblem.ofSet {α : Type u_1} (A : Set α) : PromiseProblem α

A decision problem as a promise problem: every instance is in the promise.

@[instance_reducible]

instance Cslib.Complexity.PromiseProblem.instCompl {α : Type u_1} : Compl (PromiseProblem α)

The complement of a promise problem exchanges its yes-instances and its no-instances.

@[simp]

theorem Cslib.Complexity.PromiseProblem.yes_compl {α : Type u_1} {Q : PromiseProblem α} : Qᶜ.yes = Q.no

@[simp]

theorem Cslib.Complexity.PromiseProblem.no_compl {α : Type u_1} {Q : PromiseProblem α} : Qᶜ.no = Q.yes

@[simp]

theorem Cslib.Complexity.PromiseProblem.compl_compl {α : Type u_1} {Q : PromiseProblem α} : Qᶜᶜ = Q

@[simp]

theorem Cslib.Complexity.PromiseProblem.yes_ofSet {α : Type u_1} {A : Set α} : (ofSet A).yes = A

@[simp]

theorem Cslib.Complexity.PromiseProblem.no_ofSet {α : Type u_1} {A : Set α} : (ofSet A).no = Aᶜ

@[simp]

theorem Cslib.Complexity.PromiseProblem.promise_ofSet {α : Type u_1} {A : Set α} : (ofSet A).promise = Set.univ

theorem Cslib.Complexity.PromiseProblem.ofSet_compl {α : Type u_1} {A : Set α} : ofSet Aᶜ = (ofSet A)ᶜ

theorem Cslib.Complexity.PromiseProblem.solvedBy_compl {α : Type u_1} {Q : PromiseProblem α} {f : α → Bool} : Qᶜ.SolvedBy f ↔ Q.SolvedBy fun (a : α) => !f a

A function solves the complement of a promise problem when its negation solves the problem.

theorem Cslib.Complexity.PromiseProblem.solvedBy_ofSet {α : Type u_1} {A : Set α} {f : α → Bool} : (ofSet A).SolvedBy f ↔ ∀ (a : α), a ∈ A ↔ f a = true

A function solves a decision problem when it decides it.

Lifting classes of decision problems

def Cslib.Complexity.promiseClass {α : Type u_1} (C : Set (Set α)) : Set (PromiseProblem α)

The lift of a class C of decision problems to promise problems: the promise problems separated by a problem in C, which contains every yes-instance and no no-instance.

theorem Cslib.Complexity.mem_promiseClass {α : Type u_1} {C : Set (Set α)} {Q : PromiseProblem α} : Q ∈ promiseClass C ↔ ∃ A ∈ C, Q.yes ⊆ A ∧ Disjoint A Q.no

theorem Cslib.Complexity.promiseClass_mono {α : Type u_1} : Monotone promiseClass

@[simp]

theorem Cslib.Complexity.ofSet_mem_promiseClass {α : Type u_1} {C : Set (Set α)} {A : Set α} : PromiseProblem.ofSet A ∈ promiseClass C ↔ A ∈ C

A decision problem is in the lift of a class exactly when it is in the class.

theorem Cslib.Complexity.promiseClass_subset_promiseClass_iff {α : Type u_1} {C D : Set (Set α)} : promiseClass C ⊆ promiseClass D ↔ C ⊆ D

theorem Cslib.Complexity.promiseClass_injective {α : Type u_1} : Function.Injective promiseClass

theorem Cslib.Complexity.promiseClass_inj {α : Type u_1} {C D : Set (Set α)} : promiseClass C = promiseClass D ↔ C = D

Two classes of decision problems have the same lift to promise problems exactly when they are equal.

theorem Cslib.Complexity.compl_mem_promiseClass {α : Type u_1} {C : Set (Set α)} {Q : PromiseProblem α} (hC : ∀ A ∈ C, Aᶜ ∈ C) (hQ : Q ∈ promiseClass C) : Qᶜ ∈ promiseClass C

If a class is closed under complement, so is its lift.

theorem Cslib.Complexity.mem_promiseClass_iff_solvedBy {α : Type u_1} {C : Set (Set α)} {Q : PromiseProblem α} {Good : (α → Bool) → Prop} (hC : ∀ (A : Set α), A ∈ C ↔ ∃ (f : α → Bool), Good f ∧ ∀ (a : α), a ∈ A ↔ f a = true) : Q ∈ promiseClass C ↔ ∃ (f : α → Bool), Good f ∧ Q.SolvedBy f

If the problems in C are those decided by the functions satisfying Good, then the lift of C consists of the promise problems solved by such functions.

Promise-P and promise-NP

def Cslib.Complexity.PromiseP {α : Type u_1} (enc : α ↪ List Bool) : Set (PromiseProblem α)

The promise problems solved by polynomial-time algorithms, with respect to the encoding enc of instances: the lift of P enc Goldreich.

theorem Cslib.Complexity.mem_PromiseP_iff {α : Type u_1} {enc : α ↪ List Bool} {Q : PromiseProblem α} : Q ∈ PromiseP enc ↔ ∃ (f : α → Bool), Turing.MultiTapeTM.ComputableInPolyTime f enc Turing.MultiTapeTM.encBool ∧ Q.SolvedBy f

Goldreich's definition of promise-P: a promise problem is in PromiseP when a polynomial-time function solves it.

@[simp]

theorem Cslib.Complexity.ofSet_mem_PromiseP {α : Type u_1} {enc : α ↪ List Bool} {A : Set α} : PromiseProblem.ofSet A ∈ PromiseP enc ↔ A ∈ P enc

def Cslib.Complexity.PromiseNP {α : Type} (enc : α ↪ List Bool) : Set (PromiseProblem α)

The promise problems with polynomial-time verifiers, with respect to the encoding enc of instances: the lift of NP enc Goldreich.

theorem Cslib.Complexity.mem_PromiseNP_iff {α : Type} {enc : α ↪ List Bool} {Q : PromiseProblem α} : Q ∈ PromiseNP enc ↔ ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool), Turing.MultiTapeTM.ComputableInPolyTime V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool ∧ (∀ a ∈ Q.yes, ∃ (w : List Bool), w.length = Polynomial.eval (enc a).length p ∧ V (a, w) = true) ∧ ∀ a ∈ Q.no, ∀ (w : List Bool), w.length = Polynomial.eval (enc a).length p → V (a, w) = false

Goldreich's definition of promise-NP: a promise problem is in PromiseNP when a polynomial-time verifier accepts some certificate for every yes-instance and none for any no-instance.

@[simp]

theorem Cslib.Complexity.ofSet_mem_PromiseNP {α : Type} {enc : α ↪ List Bool} {A : Set α} : PromiseProblem.ofSet A ∈ PromiseNP enc ↔ A ∈ NP enc

theorem Cslib.Complexity.PromiseP_eq_PromiseNP_iff {α : Type} {enc : α ↪ List Bool} : PromiseP enc = PromiseNP enc ↔ P enc = NP enc

PromiseP = PromiseNP ↔ P = NP.