Search to decision: FPSearch = FNP exactly when P = NP

Every search problem in FNP reduces to a decision problem in NP Papadimitriou, Section 10.3, Arora and Barak, Section 2.5: its prefix problem (Cslib.Complexity.prefixSearch) asks, given an instance a and a word u, whether some solution of a begins with u. A decision procedure D for it finds solutions bit by bit (Cslib.Complexity.prefixSearchRun): starting from the empty word, stop when the current word is a solution, and otherwise extend it by false when D says that a solution begins with the extension, and by true otherwise. As long as some solution begins with the current word, this stays true, and the word grows by one bit at every step until it is a solution; since solutions are no longer than p (enc a).length, that many steps suffice (Cslib.Complexity.rel_prefixSearchRun).

Hence if NP ⊆ P for the encoding of pairs of instances and words, every FNP relation is in FPSearch (Cslib.Complexity.FNP_subset_FPSearch_of_NP_subset_P), and with Cslib.Complexity.NP_subset_P_of_FNP_subset_FPSearch, FNP ⊆ FPSearch for every encoding exactly when NP ⊆ P for every encoding (Cslib.Complexity.FNP_subset_FPSearch_iff). Through the Cook–Levin theorem this happens exactly when SAT ∈ P (Cslib.Complexity.FNP_subset_FPSearch_iff_SAT_mem_P).

For SAT itself the self-reduction of Complexity.Computability.Complexity.Classes.NP.SelfReduction finds satisfying assignments directly: the search problem Cslib.Complexity.SAT.searchRel of assignment certificates is in FPSearch exactly when SAT ∈ P (Cslib.Complexity.SAT.searchRel_mem_FPSearch_iff).

Main definitions

• Cslib.Complexity.prefixSearch: the prefix problem of a search problem.
• Cslib.Complexity.prefixSearchStep, Cslib.Complexity.prefixSearchRun: search through prefixes.
• Cslib.Complexity.SAT.searchRel: the search problem of satisfying assignments.

Main results

• Cslib.Complexity.prefixSearch_mem_FNP: the prefix problem of an FNP relation is in FNP, so its domain is in NP.
• Cslib.Complexity.rel_prefixSearchRun: with a correct decision procedure for the prefix problem, the search through prefixes finds a solution of every instance that has one.
• Cslib.Complexity.FNP_subset_FPSearch_of_NP_subset_P, Cslib.Complexity.FNP_subset_FPSearch_iff, Cslib.Complexity.FNP_subset_FPSearch_iff_SAT_mem_P.
• Cslib.Complexity.SAT.searchRel_mem_FNP, Cslib.Complexity.SAT.searchDomain_searchRel, Cslib.Complexity.SAT.searchRel_mem_FPSearch_iff.

References

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

The prefix problem

def Cslib.Complexity.prefixSearch {α : Type} (R : α → List Bool → Prop) (x : α × List Bool) (v : List Bool) : Prop

The prefix problem of R: the solutions of a pair (a, u) are the words v such that u ++ v is a solution of a. Its domain consists of the pairs (a, u) such that some solution of a begins with u.

theorem Cslib.Complexity.prefixSearch_mem_FNP {α : Type} {enc : α ↪ List Bool} {R : α → List Bool → Prop} (hR : R ∈ FNP enc) : prefixSearch R ∈ FNP (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits)

The prefix problem of an FNP relation is in FNP.

Search through prefixes

def Cslib.Complexity.prefixSearchStep {α : Type} (V D : α × List Bool → Bool) (a : α) (u : List Bool) : List Bool

One step of the search through prefixes, with V deciding solutions and D deciding the prefix problem: keep a solution, and otherwise extend the word by false if D accepts the extension, and by true if not.

def Cslib.Complexity.prefixSearchRun {α : Type} (V D : α × List Bool → Bool) (n : α → ℕ) (a : α) : List Bool

The search through prefixes for n a steps, starting from the empty word.

theorem Cslib.Complexity.rel_prefixSearchRun {α : Type} {R : α → List Bool → Prop} {V D : α × List Bool → Bool} (hV : ∀ (a : α) (w : List Bool), R a w ↔ V (a, w) = true) (hD : ∀ (a : α) (u : List Bool), D (a, u) = true ↔ ∃ (v : List Bool), R a (u ++ v)) {n : α → ℕ} (hn : ∀ (a : α) (w : List Bool), R a w → w.length ≤ n a) {a : α} (ha : a ∈ searchDomain R) : R a (prefixSearchRun V D n a)

Search through prefixes is correct. If the solutions of a are no longer than n a, and a has a solution, the search through prefixes for n a steps finds one.

FPSearch = FNP exactly when P = NP

theorem Cslib.Complexity.FNP_subset_FPSearch_of_NP_subset_P {α : Type} {enc : α ↪ List Bool} (h : NP (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) ⊆ P (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits)) : FNP enc ⊆ FPSearch enc

Search reduces to decision: if the NP problems on pairs of instances and words are in P, every FNP relation is in FPSearch. The solver decides the prefix problem, searches through prefixes, and checks the result.

theorem Cslib.Complexity.FNP_subset_FPSearch_iff : (∀ {α : Type} (enc : α ↪ List Bool), FNP enc ⊆ FPSearch enc) ↔ ∀ {α : Type} (enc : α ↪ List Bool), NP enc ⊆ P enc

FPSearch = FNP exactly when P = NP, both for every encoding of instances.

theorem Cslib.Complexity.FNP_subset_FPSearch_iff_SAT_mem_P : (∀ {α : Type} (enc : α ↪ List Bool), FNP enc ⊆ FPSearch enc) ↔ SAT ∈ P encCNF

FPSearch = FNP exactly when SAT ∈ P, by the Cook–Levin theorem.

SAT

def Cslib.Complexity.SAT.searchRel (φ : Logic.PL.CNF ℕ) (w : List Bool) : Prop

The search problem of SAT: certificates for SAT.verifier, listing the values of the variables in order of first occurrence, that are no longer than the encoded formula.

theorem Cslib.Complexity.SAT.searchRel_mem_FNP : searchRel ∈ FNP encCNF

The search problem of SAT is in FNP.

theorem Cslib.Complexity.SAT.searchDomain_searchRel : searchDomain searchRel = SAT

The formulas with a solution in SAT.searchRel are the satisfiable ones.

theorem Cslib.Complexity.SAT.searchRel_mem_FPSearch_iff : searchRel ∈ FPSearch encCNF ↔ SAT ∈ P encCNF

Search to decision for SAT: satisfying assignments are found in polynomial time exactly when SAT ∈ P.