Isolation with parities

The randomized step of Toda's theorem Toda, [Arora and Barak, Section 17.4] [AB09]: an existential quantifier over the strings x of length M, applied to a predicate given by the parities of numbers c x of witnesses, becomes, with high probability, the parity of a single number of witnesses.

The Valiant–Vazirani test (Cslib.Complexity.Toda.hashesToZero) reads k random parity equations A x = b from a seed and tests whether x satisfies them; on bit strings it is the affine hash Cslib.BitString.LinearHash.affineHash of the seed's coefficients and offsets hitting 0 (Cslib.Complexity.Toda.hashesToZero_ofFn_iff). For a nonempty set S of strings of length M, with k = log₂ #S + 2 equations, exactly one element of S passes the test for at least 3 / 16 of the seeds of length B ≥ (M + 2) (M + 1) (Cslib.Complexity.Toda.three_mul_two_pow_le_card_filter_card_eq_one), by the Valiant–Vazirani lemma Cslib.Probability.IsPairwiseIndependentHash.three_sixteenths_le_dens_filter_card_filter_eq_one.

A trial sums the numbers c x over the strings x passing the test of some level k with some seed; its parity is the parity of the number of x with c x odd that pass the test (Finset.odd_sum_iff_odd_card_odd). The trials are combined by the parity form of a disjunction: 1 + ∏ⱼ (1 + cⱼ) is odd exactly when some cⱼ is (Cslib.BitString.odd_one_add_prod_one_add). Running 4 (E + 1) rounds, each with one trial at every level k ≤ M + 2, the combined number is odd exactly when S is nonempty, unless some c x has the wrong parity or every round fails to isolate an element of S (Cslib.Complexity.Toda.two_pow_mul_card_filter_not_odd_iff_le). With c x depending on inner random bits r and wrong for a 2 ^ (-(E + M + 1)) fraction of them for each x, the first failure has probability at most 2 ^ M * 2 ^ (-(E + M + 1)), the second at most (13 / 16) ^ (4 (E + 1)) ≤ 2 ^ (-(E + 1)), so the result is wrong with probability at most 2 ^ (-E).

Main definitions

• Cslib.Complexity.Toda.hashesToZero: the Valiant–Vazirani test on words.

Main results

• Cslib.Complexity.Toda.hashesToZero_ofFn_iff: the test is the affine hash hitting 0.
• Cslib.Complexity.Toda.three_mul_two_pow_le_card_filter_card_eq_one: isolation with probability at least 3 / 16.
• Cslib.Complexity.Toda.two_pow_mul_card_filter_not_odd_iff_le: the isolation step errs with probability at most 2 ^ (-E).

References

• S. Toda, PP is as hard as the polynomial-time hierarchy
• L. G. Valiant, V. V. Vazirani, NP is as easy as detecting unique solutions
• S. Arora, B. Barak, Computational Complexity: A Modern Approach

The Valiant–Vazirani test

def Cslib.Complexity.Toda.hashesToZero (k : ℕ) (seed w : List Bool) : Bool

The Valiant–Vazirani test: w satisfies the k parity equations read from seed, whose coefficients are k rows of w.length bits and whose offsets are the next k bits, missing bits being false.

theorem Cslib.Complexity.Toda.computableInPolyTime_hashesToZero {γ : Type} {input : γ ↪ List Bool} {k : γ → ℕ} {seed w : γ → List Bool} (hk : Turing.MultiTapeTM.ComputableInPolyTime k input Turing.MultiTapeTM.encUnary) (hseed : Turing.MultiTapeTM.ComputableInPolyTime seed input Turing.MultiTapeTM.encBits) (hw : Turing.MultiTapeTM.ComputableInPolyTime w input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => hashesToZero (k x) (seed x) (w x)) input Turing.MultiTapeTM.encBool

The test is polynomial-time, with all its arguments computed.

theorem Cslib.Complexity.Toda.hashesToZero_ofFn_iff {k M : ℕ} (seed : List Bool) (x : BitString M) : hashesToZero k seed (List.ofFn x) = true ↔ BitString.LinearHash.affineHash (ValiantVazirani.matrix k M seed, ValiantVazirani.offset k M seed) x = 0

On a bit string, the test is the affine hash of the coefficients and offsets read from the seed hitting 0.

theorem Cslib.Complexity.Toda.three_mul_two_pow_le_card_filter_card_eq_one {M B : ℕ} {S : Finset (BitString M)} (hS : S.Nonempty) (hB : (Nat.log 2 S.card + 2) * M + (Nat.log 2 S.card + 2) ≤ B) : 3 * 2 ^ B ≤ 16 * {σ : Fin B → Bool | {x ∈ S | hashesToZero (Nat.log 2 S.card + 2) (List.ofFn σ) (List.ofFn x) = true}.card = 1}.card

Isolation with probability 3 / 16: for a nonempty set S of strings of length M, with k = log₂ #S + 2 equations, exactly one element of S passes the test for at least 3 / 16 of the seeds of any length B ≥ k M + k.

The isolation step

theorem Cslib.Complexity.Toda.two_pow_mul_card_filter_not_odd_iff_le {R M E e' B : ℕ} (c : (Fin R → Bool) → (Fin M → Bool) → ℕ) (S : Finset (Fin M → Bool)) (hc : ∀ (x : Fin M → Bool), 2 ^ e' * {r : Fin R → Bool | ¬(Odd (c r x) ↔ x ∈ S)}.card ≤ 2 ^ R) (he : E + M + 1 ≤ e') (hB : (M + 2) * (M + 1) ≤ B) : 2 ^ E * {p : (Fin R → Bool) × (Fin (4 * (E + 1) * (M + 3)) → BitString B) | ¬(Odd (1 + ∏ j : Fin (4 * (E + 1) * (M + 3)), (1 + ∑ x : Fin M → Bool with hashesToZero (↑j % (M + 3)) (List.ofFn (p.2 j)) (List.ofFn x) = true, c p.1 x)) ↔ S.Nonempty)}.card ≤ 2 ^ R * 2 ^ (4 * (E + 1) * (M + 3) * B)

The isolation step errs with probability at most 2 ^ (-E). Let c r x be numbers whose parity says whether x ∈ S, except for at most a 2 ^ (-e') fraction of the random strings r of length R, for each string x of length M, where e' ≥ E + M + 1. Draw seeds of B ≥ (M + 2) (M + 1) bits for T = 4 (E + 1) (M + 3) trials, the trial j testing at level j % (M + 3). Then 1 + ∏ⱼ (1 + ∑ c r x), the inner sum over the x passing trial j, is odd exactly when S is nonempty, except for at most a 2 ^ (-E) fraction of the random strings and seeds.