The Valiant–Vazirani randomized isolation reduction

ValiantVazirani.reduce (φ, r) adds to φ some number k of random parity equations A x + b = 0 over the n = φ.vars.length occurrences x of its variables [Valiant and Vazirani] [VV86], Arora and Barak, Section 17.4. The number k is read in binary from the first hashBits φ bits of r, so that every k ≤ n + 2 has probability 2 ^ (-hashBits φ) ≥ 1 / (2 (n + 3)); the rows of A and the offsets b are read from the remaining bits, missing bits being false. Each equation is written in conjunctive normal form with auxiliary variables carrying its prefix parities, with two or four clauses per term, so the auxiliary variables are determined by the original ones. The variables are then renumbered by the injective Cslib.Complexity.splitVarToNat.

Main definitions

• Cslib.Complexity.ValiantVazirani.hashCNF: random parity equations in conjunctive normal form.
• Cslib.Complexity.ValiantVazirani.reduce: the Valiant–Vazirani reduction.
• Cslib.Complexity.ValiantVazirani.randomBits: the number of random bits it reads.

Main results

• Cslib.Complexity.ValiantVazirani.computableInPolyTime_reduce: polynomial time.
• Cslib.Complexity.ValiantVazirani.reduce_mem_UNSAT: soundness.
• Cslib.Complexity.ValiantVazirani.three_mul_two_pow_le_card_filter_card_filter_eq_one: the Valiant–Vazirani lemma for affine seeds, in integers.
• Cslib.Complexity.ValiantVazirani.three_mul_two_pow_le_card_reduce_mem_USAT, Cslib.Complexity.ValiantVazirani.three_div_le_dens_reduce_mem_USAT: success probability Ω(1 / n).
• Cslib.Complexity.ValiantVazirani.two_pow_le_two_mul_card_exists_row: amplification by independent rows.

References

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

Parity equations in conjunctive normal form

@[reducible, inline]

abbrev Cslib.Complexity.ValiantVazirani.Var : Type

The variables of the reduced formula before renumbering: inl v is a variable of the original formula, and inr (i, j) carries the parity of the first j terms of the i-th equation.

def Cslib.Complexity.ValiantVazirani.encVar : Var ↪ List Bool

The encoding of the variables of the reduced formula: original variables in binary, auxiliary indices in unary.

def Cslib.Complexity.ValiantVazirani.stepClauses (bit : Bool) (next prev x : Var) : Logic.PL.CNF Var

Clauses forcing next = prev ^^ (bit && x).

def Cslib.Complexity.ValiantVazirani.rowClauses (vars : List ℕ) (i : ℕ) (row : List Bool) (offset : Bool) : Logic.PL.CNF Var

Clauses forcing the i-th parity equation: the auxiliary variables inr (i, j) start at offset, the j-th one adds row[j] && vars[j], and the last one is false. Together they force offset ^^ ⨁ j, (row[j] && vars[j]) = false.

def Cslib.Complexity.ValiantVazirani.hashCNF (vars : List ℕ) (k : ℕ) (w : List Bool) : Logic.PL.CNF Var

The k parity equations read from the word w: the i-th equation has the i-th row of vars.length bits of w as coefficients, and offset bit k * vars.length + i of w. Missing bits are false.

def Cslib.Complexity.ValiantVazirani.hashBits (φ : Logic.PL.CNF ℕ) : ℕ

The number of random bits selecting the number of equations.

def Cslib.Complexity.ValiantVazirani.reduceWith (φ : Logic.PL.CNF ℕ) (k : ℕ) (w : List Bool) : Logic.PL.CNF ℕ

φ together with k random parity equations read from w, renumbered into ℕ.

def Cslib.Complexity.ValiantVazirani.reduce (x : Logic.PL.CNF ℕ × List Bool) : Logic.PL.CNF ℕ

The Valiant–Vazirani reduction. The first hashBits φ random bits, read in binary, give the number k of parity equations; the remaining bits give their coefficients and offsets.

Polynomial time

theorem Cslib.Complexity.ValiantVazirani.computableInPolyTime_stepClauses : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Bool × Var × Var × Var) => stepClauses p.1 p.2.1 p.2.2.1 p.2.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBool (Turing.MultiTapeTM.encPair encVar (Turing.MultiTapeTM.encPair encVar encVar))) (Logic.PL.encCNFOver encVar)

Building the clauses of one step is polynomial-time.

theorem Cslib.Complexity.ValiantVazirani.computableInPolyTime_rowClauses : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List ℕ × ℕ × List Bool × Bool) => rowClauses p.1 p.2.1 p.2.2.1 p.2.2.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool))) (Logic.PL.encCNFOver encVar)

Building the clauses of one equation is polynomial-time.

theorem Cslib.Complexity.ValiantVazirani.computableInPolyTime_hashCNF : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List ℕ × ℕ × List Bool) => hashCNF p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits)) (Logic.PL.encCNFOver encVar)

Building all equations is polynomial-time, with the number of equations in unary.

theorem Cslib.Complexity.ValiantVazirani.computableInPolyTime_reduce : Turing.MultiTapeTM.ComputableInPolyTime reduce (Turing.MultiTapeTM.encPair encCNF Turing.MultiTapeTM.encBits) encCNF

The Valiant–Vazirani reduction is polynomial-time, on the framed encoding of the formula followed by the raw random bits.

Semantics of the parity equations

theorem Cslib.Complexity.ValiantVazirani.eval_stepClauses (σ : Var → Bool) (bit : Bool) (next prev x : Var) : Logic.PL.CNF.eval σ (stepClauses bit next prev x) = true ↔ σ next = (σ prev ^^ bit && σ x)

The clauses of a step hold exactly when next = prev ^^ (bit && x).

def Cslib.Complexity.ValiantVazirani.matrix (k width : ℕ) (w : List Bool) : Fin k → BitString width

The coefficient matrix read from w by hashCNF: k rows of width bits. Missing bits are false.

def Cslib.Complexity.ValiantVazirani.offset (k width : ℕ) (w : List Bool) : BitString k

The offsets read from w by hashCNF, after the coefficient matrix. Missing bits are false.

def Cslib.Complexity.ValiantVazirani.point (vars : List ℕ) (σ : ℕ → Bool) : BitString vars.length

The variables vars read off an assignment of the original variables.

def Cslib.Complexity.ValiantVazirani.auxValue (vars : List ℕ) (k : ℕ) (w : List Bool) (σ : ℕ → Bool) (i : Fin k) (j : ℕ) : Bool

The value of the auxiliary variable inr (i, j) forced by an assignment σ of the original variables: the offset plus the first j terms of the i-th equation.

Variables of the reduced formula

Soundness and isolation

theorem Cslib.Complexity.ValiantVazirani.satisfiable_of_satisfiable_reduceWith {φ : Logic.PL.CNF ℕ} {k : ℕ} {w : List Bool} (h : (reduceWith φ k w).Satisfiable) : φ.Satisfiable

Soundness. A satisfying assignment of the reduced formula restricts to one of φ: the equations only add constraints.

theorem Cslib.Complexity.ValiantVazirani.reduce_mem_UNSAT {φ : Logic.PL.CNF ℕ} (hφ : φ ∈ UNSAT) (r : List Bool) : reduce (φ, r) ∈ UNSAT

Soundness of the reduction: if φ is unsatisfiable, then so is the reduced formula, for every random word.

noncomputable def Cslib.Complexity.ValiantVazirani.solutions (φ : Logic.PL.CNF ℕ) : Finset (BitString φ.vars.length)

The satisfying assignments of φ, read off at the occurrences of its variables.

theorem Cslib.Complexity.ValiantVazirani.mem_solutions {φ : Logic.PL.CNF ℕ} {x : BitString φ.vars.length} : x ∈ solutions φ ↔ ∃ (σ : ℕ → Bool), Logic.PL.CNF.eval σ φ = true ∧ point φ.vars σ = x

theorem Cslib.Complexity.ValiantVazirani.auxValue_congr {vars : List ℕ} {k : ℕ} {w : List Bool} {σ τ : ℕ → Bool} (h : point vars σ = point vars τ) (i : Fin k) (j : ℕ) : auxValue vars k w σ i j = auxValue vars k w τ i j

The forced auxiliary values only depend on the original variables among vars.

def Cslib.Complexity.ValiantVazirani.Isolates (φ : Logic.PL.CNF ℕ) {k : ℕ} (p : (Fin k → BitString φ.vars.length) × BitString k) : Prop

The equations with seed p isolate a solution of φ: exactly one solution hashes to zero.

theorem Cslib.Complexity.ValiantVazirani.reduceWith_mem_USAT {φ : Logic.PL.CNF ℕ} {k : ℕ} {w : List Bool} (h : Isolates φ (matrix k φ.vars.length w, offset k φ.vars.length w)) : reduceWith φ k w ∈ USAT

Isolation gives unique satisfiability. If exactly one satisfying assignment of φ hashes to zero under the equations read from w, then φ with these equations is uniquely satisfiable: the auxiliary variables are determined by the original ones.

The success probability

theorem Cslib.Complexity.ValiantVazirani.solutions_nonempty {φ : Logic.PL.CNF ℕ} (hφ : φ.Satisfiable) : (solutions φ).Nonempty

A satisfiable formula has a solution.

theorem Cslib.Complexity.ValiantVazirani.three_mul_two_pow_le_card_filter_card_filter_eq_one {M : ℕ} {S : Finset (BitString M)} (hS : S.Nonempty) : 3 * 2 ^ ((Nat.log 2 S.card + 2) * M + (Nat.log 2 S.card + 2)) ≤ 16 * {p : (Fin (Nat.log 2 S.card + 2) → BitString M) × BitString (Nat.log 2 S.card + 2) | {x ∈ S | BitString.LinearHash.affineHash p x = 0}.card = 1}.card

The Valiant–Vazirani lemma in integers: for a nonempty set S of bit strings of length M, with k = log₂ #S + 2 random equations, exactly one element of S satisfies them for at least 3 / 16 of the 2 ^ (k M + k) affine seeds.

Counting random words

theorem Cslib.Complexity.ValiantVazirani.take_ofFn {m a : ℕ} (h : a ≤ m) (r : Fin m → Bool) : List.take a (List.ofFn r) = List.ofFn fun (i : Fin a) => r (Fin.castLE h i)

A prefix of a word given by its bits.

theorem Cslib.Complexity.ValiantVazirani.drop_ofFn {m a : ℕ} (h : a ≤ m) (r : Fin m → Bool) : List.drop a (List.ofFn r) = List.ofFn fun (j : Fin (m - a)) => r ⟨a + ↑j, ⋯⟩

A suffix of a word given by its bits.

theorem Cslib.Complexity.ValiantVazirani.matrix_take (k width : ℕ) (w : List Bool) : matrix k width (List.take (k * width + k) w) = matrix k width w

The coefficients only read the first k * width + k bits.

theorem Cslib.Complexity.ValiantVazirani.offset_take (k width : ℕ) (w : List Bool) : offset k width (List.take (k * width + k) w) = offset k width w

The offsets only read the first k * width + k bits.

theorem Cslib.Complexity.ValiantVazirani.card_filter_seed {k width : ℕ} (U : (Fin k → BitString width) × BitString k → Prop) [DecidablePred U] : {v : Fin (k * width + k) → Bool | U (matrix k width (List.ofFn v), offset k width (List.ofFn v))}.card = (Finset.filter U Finset.univ).card

Reading the coefficients and offsets is a bijection from words of exactly k * width + k bits.

def Cslib.Complexity.ValiantVazirani.randomBits (φ : Logic.PL.CNF ℕ) : ℕ

The number of random bits the reduction reads on φ: hashBits φ selector bits, then the coefficients and offsets of up to φ.vars.length + 2 equations of φ.vars.length terms.

theorem Cslib.Complexity.ValiantVazirani.randomBits_le (φ : Logic.PL.CNF ℕ) : randomBits φ ≤ (φ.vars.length + 2) ^ 2

The reduction reads at most (φ.vars.length + 2) ^ 2 random bits.

theorem Cslib.Complexity.ValiantVazirani.three_mul_two_pow_le_card_reduce_mem_USAT {φ : Logic.PL.CNF ℕ} (hφ : φ ∈ SAT) {m : ℕ} (hm : randomBits φ ≤ m) : 3 * 2 ^ m ≤ 32 * (φ.vars.length + 3) * {r : Fin m → Bool | reduce (φ, List.ofFn r) ∈ USAT}.card

The Valiant–Vazirani reduction succeeds with probability Ω(1 / n). For a satisfiable formula φ with n = φ.vars.length variable occurrences and any number m ≥ randomBits φ of random bits, the reduced formula is uniquely satisfiable for at least a 3 / (32 (n + 3)) fraction of the random words of length m. Since n counts occurrences, not variables, this is Ω(1 / |φ|) in the length of the formula, weaker than the textbook bound 1 / (8 v) in the number v of variables.

theorem Cslib.Complexity.ValiantVazirani.three_div_le_dens_reduce_mem_USAT {φ : Logic.PL.CNF ℕ} (hφ : φ ∈ SAT) {m : ℕ} (hm : randomBits φ ≤ m) : 3 / (32 * (↑φ.vars.length + 3)) ≤ {r : Fin m → Bool | reduce (φ, List.ofFn r) ∈ USAT}.dens

The Valiant–Vazirani success probability as a density: for a satisfiable formula φ with n = φ.vars.length variable occurrences and m ≥ randomBits φ, a uniformly random word of length m makes the reduced formula uniquely satisfiable with probability at least 3 / (32 (n + 3)).

Amplification

theorem Cslib.Complexity.ValiantVazirani.two_pow_le_two_mul_card_exists_row {M W : ℕ} (hM : 0 < M) (good : List Bool → Prop) [DecidablePred good] (hgood : 3 * 2 ^ W ≤ 32 * M * {b : Fin W → Bool | good (List.ofFn b)}.card) : 2 ^ (11 * M * W) ≤ 2 * {r : Fin (11 * M * W) → Bool | ∃ b ∈ BitString.listRows (11 * M) W (List.ofFn r), good b}.card

Amplification by independent rows. If at least a 3 / (32 M) fraction of the words of length W are good, then among the words of 11 M rows of W bits, at least half have a good row: the repeated-trials bound Fintype.half_le_dens_filter_exists_apply_mem, transferred along the block decomposition.