Valiant–Vazirani theorem

DefinitionSAT with a unary variable count as a decision problem#✓fully proved

A bitstring \(x\) is a yes-instance exactly when bitstring decoding of \(x\), as a pair of a list of booleans and a CNF formula, succeeds and returns a pair \((u, \varphi)\) such that, writing \(m\) for the length of \(u\), every variable occurring in \(\varphi\) is less than \(m\) and some assignment of booleans to the variables \(0, \dots, m - 1\) satisfies \(\varphi\) once it is extended by assigning false to every variable \(v \ge m\).

noncomputable def satDec' :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := List Bool × Cslib.Logic.PL.CNF) x with
  | some i => decide (∀ clause ∈ i.2, ∀ l ∈ clause, l.1 < i.1.length) ∧
      decide (∃ a : Fin i.1.length → Bool,
        Cslib.Logic.PL.CNF.Satisfies
          (fun v => if h : v < i.1.length then a ⟨v, h⟩ else false) i.2)
  | none => false

Uses 12 · Used by 1

Statement usesCNF formula · Satisfaction of a CNF formula · CNF clause · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Decision problems

Used byValiant-Vazirani: SAT reduces to UniqueSAT

DefinitionUniqueSAT with a unary variable count as a decision problem#✓fully proved

A bitstring \(x\) is a yes-instance exactly when bitstring decoding of \(x\), as a pair of a list of booleans and a CNF formula, succeeds and returns a pair \((u, \varphi)\) such that, writing \(m\) for the length of \(u\), every variable occurring in \(\varphi\) is less than \(m\) and exactly one assignment of booleans to the variables \(0, \dots, m - 1\) satisfies \(\varphi\) once it is extended by assigning false to every variable \(v \ge m\).

noncomputable def uniqueSatDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := List Bool × Cslib.Logic.PL.CNF) x with
  | some i => decide (∀ clause ∈ i.2, ∀ l ∈ clause, l.1 < i.1.length) ∧
      decide (∃! a : Fin i.1.length → Bool,
        Cslib.Logic.PL.CNF.Satisfies
          (fun v => if h : v < i.1.length then a ⟨v, h⟩ else false) i.2)
  | none => false

Uses 12 · Used by 1

Statement usesCNF formula · Satisfaction of a CNF formula · CNF clause · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Decision problems

Used byValiant-Vazirani: SAT reduces to UniqueSAT

TheoremValiant-Vazirani: SAT reduces to UniqueSAT#●ready to prove

There are a polynomial \(p\) with natural-number coefficients and a polynomial-time computable function \(R\) from pairs of bitstrings to bitstrings such that, for every bitstring \(x\) of length \(n\): if \(x\) is not in SAT, then for every bitstring \(r\) of length \(p(n)\) the bitstring \(R(x, r)\) is in neither SAT nor UniqueSAT; and if \(x\) is in SAT, then the number \(N\) of bitstrings \(r\) of length \(p(n)\) for which \(R(x, r)\) is in UniqueSAT satisfies \(8(n + 1) N \ge 2^{p(n)}\).

Here SAT and UniqueSAT are the bitstring decision problems for CNF formulas with the variable count given in unary.

public theorem_wanted valiant_vazirani :
    ∃ p : Polynomial ℕ, ∃ red : List Bool × List Bool → List Bool, IsPolyTime red ∧
      ∀ x : List Bool, let n := x.length
        (satDec' x = false →
          ∀ r : List Bool, r.length = p.eval n →
            satDec' (red (x, r)) = false ∧ uniqueSatDec (red (x, r)) = false) ∧
        (satDec' x = true →
          8 * (n + 1) * Set.ncard {r : Fin (p.eval n) → Bool |
            uniqueSatDec (red (x, List.ofFn r)) = true} ≥ 2 ^ (p.eval n))

Sources

• L. G. Valiant and V. V. Vazirani, "NP is as easy as detecting unique solutions", Theoretical Computer Science 47 (1986), 85-93 (STOC 1985).

Uses 11

Statement usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · SAT with a unary variable count as a decision problem · UniqueSAT with a unary variable count as a decision problem · Polynomial-time computable functions

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.