The Valiant–Vazirani theorem

Valiant and Vazirani showed that deciding satisfiability reduces in randomized polynomial time to deciding it on formulas with at most one satisfying assignment [Valiant and Vazirani] [VV86], Arora and Barak, Section 17.4.

The randomized isolation reduction ValiantVazirani.reduce and its amplification bound ValiantVazirani.two_pow_le_two_mul_card_exists_row are developed in CslibFrontier.Computability.Complexity.Classes.ValiantVazirani.Reduction and re-exported here.

The class form

RPWithOracle A enc is RP relative to the oracle language A: Cslib.Complexity.RP with ComputableInPolyTime replaced by Cslib.Complexity.ComputableInPolyTimeWithOracle A, as PWithOracle relativizes P. For an oracle that is a promise problem, RPWithPromiseOracle Q encQ enc asks for one algorithm that is correct against every language solving Q, whose answers outside the promise are arbitrary. Every problem in NP lies in RP relative to PromiseUSAT (NP_subset_RPWithPromiseOracle_PromiseUSAT): after the Cook–Levin reduction, the algorithm runs the Valiant–Vazirani reduction on 11 (N + 3) independent blocks of random bits, where N bounds the number of variable occurrences, asks the oracle about each reduced formula (queryAny), and accepts when it answers yes once. On a no-instance every reduced formula is unsatisfiable, so the oracle answers no; on a yes-instance some reduced formula is uniquely satisfiable except with probability at most (1 - 3 / (32 (N + 3))) ^ (11 (N + 3)) ≤ 1 / 2 (ValiantVazirani.two_pow_le_two_mul_card_exists_row, from the repeated-trials bound Fintype.half_le_dens_filter_exists_apply_mem). In particular NP ⊆ RP^USAT (NP_subset_RPWithOracle_USAT); this form is weak, since USAT as a language is coNP-hard, and the promise version carries the Valiant–Vazirani content.

Main definitions

• Cslib.Complexity.RPWithOracle, Cslib.Complexity.RPWithPromiseOracle: RP relative to an oracle language and to a promise problem.
• Cslib.Complexity.queryAny: ask every word of a list.

Main results

• Cslib.Complexity.computableInPolyTimeWithOracle_any_mem: asking a list of words.
• Cslib.Complexity.NP_subset_RPWithPromiseOracle_PromiseUSAT: NP ⊆ RP^PromiseUSAT.
• Cslib.Complexity.NP_subset_RPWithOracle_USAT: NP ⊆ RP^USAT.

References

• L. G. Valiant, V. V. Vazirani, NP is as easy as detecting unique solutions
• S. Arora, B. Barak, Computational Complexity: A Modern Approach

Randomized polynomial time relative to an oracle

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

The problems decided with one-sided error by polynomial-time machines with oracle A reading polynomially long random strings: Cslib.Complexity.RP with ComputableInPolyTime replaced by ComputableInPolyTimeWithOracle A, as PWithOracle relativizes P.

theorem Cslib.Complexity.mem_RPWithOracle {α : Type} {A : Set (List Bool)} {enc : α ↪ List Bool} {L : Set α} : L ∈ RPWithOracle A enc ↔ ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool), ComputableInPolyTimeWithOracle A V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool ∧ DecidesWithOneSidedError enc p V L

theorem Cslib.Complexity.RP_subset_RPWithOracle {α : Type} (A : Set (List Bool)) (enc : α ↪ List Bool) : RP enc ⊆ RPWithOracle A enc

Every problem in RP is in RP relative to every oracle.

theorem Cslib.Complexity.RPWithOracle_subset_NPWithOracle {α : Type} (A : Set (List Bool)) (enc : α ↪ List Bool) : RPWithOracle A enc ⊆ NPWithOracle A enc

RP relative to an oracle lies inside NP relative to the same oracle: an accepted random string is a certificate.

def Cslib.Complexity.RPWithPromiseOracle {α β : Type} (Q : PromiseProblem β) (encQ : β ↪ List Bool) (enc : α ↪ List Bool) : Set (Set α)

The problems decided with one-sided error by a single polynomial-time oracle algorithm against every oracle language that solves the promise problem Q under the encoding encQ: RP relative to a promise problem. The algorithm is fixed before the oracle, and the oracle's answers outside the promise are arbitrary.

theorem Cslib.Complexity.RP_subset_RPWithPromiseOracle {α β : Type} (Q : PromiseProblem β) (encQ : β ↪ List Bool) (enc : α ↪ List Bool) : RP enc ⊆ RPWithPromiseOracle Q encQ enc

Every problem in RP is in RP relative to every promise problem: its algorithm makes no request.

theorem Cslib.Complexity.RPWithPromiseOracle_subset_RPWithOracle {α β : Type} {Q : PromiseProblem β} {encQ : β ↪ List Bool} {A : Set (List Bool)} (hA : Q.SolvedBy fun (b : β) => decide (encQ b ∈ A)) (enc : α ↪ List Bool) : RPWithPromiseOracle Q encQ enc ⊆ RPWithOracle A enc

RP relative to a promise problem lies inside RP relative to every oracle language solving the promise problem.

Asking every word of a list

def Cslib.Complexity.queryAnyStep (s : List (List Bool) × Bool) : WordQueryComp Unit (List (List Bool) × Bool)

One step of queryAny: ask the first remaining word, and record whether its reply begins with true.

def Cslib.Complexity.queryAny (words : List (List Bool)) : WordQueryComp Unit Bool

Ask the oracle every word of the list, in order, and accept when some reply begins with true.

theorem Cslib.Complexity.interpret_queryAny (A : Set (List Bool)) (words : List (List Bool)) : OracleComp.interpret (languageOracle A) (queryAny words) = words.any fun (word : List Bool) => decide (word ∈ A)

Against a language oracle, queryAny accepts exactly when some word is in the language.

theorem Cslib.Complexity.computableInPolyTimeWithOracle_any_mem (A : Set (List Bool)) : ComputableInPolyTimeWithOracle A (fun (words : List (List Bool)) => words.any fun (word : List Bool) => decide (word ∈ A)) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

Whether some word of a list is in A is computable in polynomial time relative to A.

NP is in RP relative to PromiseUSAT

theorem Cslib.Complexity.NP_subset_RPWithPromiseOracle_PromiseUSAT {α : Type} (enc : α ↪ List Bool) : NP enc ⊆ RPWithPromiseOracle PromiseUSAT encCNF enc

Valiant–Vazirani: NP ⊆ RP^PromiseUSAT. Every problem in NP is decided with one-sided error by one polynomial-time oracle algorithm against every language solving PromiseUSAT. The algorithm reduces the instance to SAT by the Cook–Levin theorem, runs the Valiant–Vazirani reduction on 11 (N + 3) independent blocks of (N + 2) ^ 2 random bits, where N bounds the number of variable occurrences, asks the oracle about each reduced formula, and accepts when it answers yes once. On a no-instance every reduced formula is unsatisfiable, so the oracle always answers no.

theorem Cslib.Complexity.NP_subset_RPWithOracle_of_solvedBy {α : Type} {A : Set (List Bool)} (hA : PromiseUSAT.SolvedBy fun (φ : Logic.PL.CNF ℕ) => decide (encCNF φ ∈ A)) (enc : α ↪ List Bool) : NP enc ⊆ RPWithOracle A enc

NP ⊆ RP^A for every language A solving PromiseUSAT.

theorem Cslib.Complexity.NP_subset_RPWithOracle_USAT {α : Type} (enc : α ↪ List Bool) : NP enc ⊆ RPWithOracle (⇑encCNF '' USAT) enc

NP ⊆ RP^USAT, with the encodings of the uniquely satisfiable formulas as oracle. This form is weak: USAT as a language is coNP-hard, so even P relative to it contains NP. The Valiant–Vazirani content is the promise version NP_subset_RPWithPromiseOracle_PromiseUSAT, whose algorithm only relies on the oracle's answers on uniquely satisfiable and unsatisfiable formulas.