Complexity of the permanent

DefinitionPermanent of an encoded 0-1 matrix#✓fully proved

For a bitstring \(x\): if \(x\) decodes, under the canonical bitstring encoding, to a pair \((n, e)\) of a natural number \(n\) and a list \(e = (e_0, \dots, e_{n^2 - 1})\) of \(n^2\) natural numbers each at most \(1\), the value at \(x\) is the permanent \(\sum_{\sigma} \prod_{i=0}^{n-1} e_{in + \sigma(i)}\) of the \(n \times n\) matrix with row-major entries \(e\), where \(\sigma\) ranges over the permutations of \(\{0, \dots, n - 1\}\); otherwise the value is \(0\).

noncomputable def permOf (x : List Bool) : ℕ :=
  match MetaMathlibExt.BitstringEncoding.bitDecode (α := ℕ × List ℕ) x with
  | some (n, entries) =>
    if entries.length = n * n ∧ ∀ e ∈ entries, e ≤ 1 then
      (Finset.univ : Finset (Equiv.Perm (Fin n))).sum (fun σ =>
        (Finset.univ : Finset (Fin n)).prod
          (fun i => entries.getD (i.val * n + (σ i).val) 0))
    else 0
  | none => 0

Uses 8 · Used by 1

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

Used byJerrum-Sinclair-Vigoda: FPRAS for the permanent

TheoremJerrum-Sinclair-Vigoda: FPRAS for the permanent#●ready to prove

For a bitstring \(x\), let \(\operatorname{perm}(x)\) be the permanent of the 0-1 matrix encoded by \(x\): if \(x\) decodes, under the canonical bitstring encoding, to a pair \((k, e)\) of a natural number \(k\) and a list \(e\) of \(k^2\) natural numbers each at most \(1\), then \(\operatorname{perm}(x)\) is the permanent of the \(k \times k\) matrix with row-major entries \(e\), and otherwise \(\operatorname{perm}(x) = 0\). There are a polynomial \(p\) with natural-number coefficients and a polynomial-time computable function \(E\) from triples of bitstrings to natural numbers such that for all bitstrings \(x\) and \(w\) with \(n = |w| \ge 1\) (the precision, given in unary), at least two thirds of the bitstrings \(r\) of length \(p(|x| + n)\) satisfy \(|E(x, r, w) - \operatorname{perm}(x)| \le \operatorname{perm}(x) / n\).

public theorem_wanted jerrum_sinclair_vigoda_permanent :
    ∃ p : Polynomial ℕ, ∃ Est : List Bool × List Bool × List Bool → ℕ,
      IsPolyTime Est ∧ ∀ (x : List Bool) (prec : List Bool), 1 ≤ prec.length →
        3 * Set.ncard {r : Fin (p.eval (x.length + prec.length)) → Bool |
          |(Est (x, List.ofFn r, prec) : ℚ) - (permOf x : ℚ)| ≤
            (permOf x : ℚ) / (prec.length : ℚ)} ≥
          2 * 2 ^ (p.eval (x.length + prec.length))

Sources

• M. Jerrum, A. Sinclair, and E. Vigoda, "A polynomial-time approximation algorithm for the permanent of a matrix with nonnegative entries", Journal of the ACM 51 (2004), 671-697 (STOC 2001); M. Jerrum and A. Sinclair, "Approximating the permanent", SIAM Journal on Computing 18 (1989), 1149-1178 (precursor with restricted guarantees).

Uses 10

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 · Permanent of an encoded 0-1 matrix · Polynomial-time computable functions

DefinitionPermanent of an encoded 0-1 matrix#✓fully proved

For a bitstring \(x\) that decodes to a pair \((n, e)\) of a natural number \(n\) and a list \(e = (e_0, \dots, e_{m-1})\) of natural numbers with \(m = n^2\) and every \(e_j \le 1\), the value at \(x\) is the permanent \(\sum_{\sigma} \prod_{i < n} e_{in + \sigma(i)}\) of the \(n \times n\) matrix with entries \(e\) in row-major order, the sum running over all permutations \(\sigma\) of \(\{0, \dots, n - 1\}\). For every other bitstring the value is \(0\).

noncomputable def permFun (x : List Bool) : ℕ :=
  match MetaMathlibExt.BitstringEncoding.bitDecode (α := ℕ × List ℕ) x with
  | some (n, entries) =>
    if entries.length = n * n ∧ ∀ e ∈ entries, e ≤ 1 then
      (Finset.univ : Finset (Equiv.Perm (Fin n))).sum (fun σ =>
        (Finset.univ : Finset (Fin n)).prod
          (fun i => entries.getD (i.val * n + (σ i).val) 0))
    else 0
  | none => 0

Uses 8 · Used by 1

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

Used byThe permanent is #P-complete (Valiant)

TheoremThe permanent is #P-complete (Valiant)#●ready to prove

The function that sends a bitstring encoding a square 0-1 matrix to its permanent, and every other bitstring to \(0\), is \(\#P\)-complete.

public theorem_wanted permanent_sharpP_complete :
    SharpPComplete permFun

Sources

• L. G. Valiant, "The complexity of computing the permanent", Theoretical Computer Science 8 (1979), 189-201.

Uses 2

Statement uses\(\#P\)-complete functions · Permanent of an encoded 0-1 matrix

2 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.