Karp–Luby algorithm for DNF counting

DefinitionSatisfaction of a DNF formula#✓fully proved

A DNF formula is a list of terms, each a list of literals \((v, b)\) of a natural number \(v\) (the variable) and a boolean \(b\) (the polarity). An assignment \(a\) of booleans to the natural numbers satisfies the formula when some term of it has \(a(v) = b\) for every literal \((v, b)\) of that term.

def dnfSat (assign : ℕ → Bool) (φ : List (List (ℕ × Bool))) : Prop :=
  ∃ term ∈ φ, ∀ p ∈ term, assign p.1 = p.2

Used by 1

Used byNumber of satisfying assignments of an encoded DNF formula

DefinitionNumber of satisfying assignments of an encoded DNF formula#✓fully proved

For a bitstring \(x\): if \(x\) decodes, under the canonical bitstring encoding, to a pair \((u, \varphi)\) of a bitstring \(u\) of length \(m\) and a DNF formula \(\varphi\) all of whose literals have variables less than \(m\), the value at \(x\) is the number of assignments of booleans to the variables \(0, \dots, m - 1\) that satisfy \(\varphi\); otherwise the value is \(0\).

noncomputable def dnfCountOf (x : List Bool) : ℕ :=
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := List Bool × List (List (ℕ × Bool))) x with
  | some (u, φ) =>
    if ∀ clause ∈ φ, ∀ l ∈ clause, l.1 < u.length then
      Set.ncard {a : Fin u.length → Bool |
        dnfSat (fun v => if h : v < u.length then a ⟨v, h⟩ else false) φ}
    else 0
  | none => 0

Uses 9 · 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 · Satisfaction of a DNF formula

Used byKarp-Luby: FPRAS for DNF counting

TheoremKarp-Luby: FPRAS for DNF counting#●ready to prove

For a bitstring \(x\), let \(N(x)\) be the number of satisfying assignments of the DNF formula encoded by \(x\): if \(x\) decodes, under the canonical bitstring encoding, to a pair \((u, \varphi)\) of a bitstring \(u\) of length \(m\) and a DNF formula \(\varphi\) whose variables are all less than \(m\), then \(N(x)\) is the number of assignments of booleans to the variables \(0, \dots, m - 1\) that satisfy \(\varphi\), and otherwise \(N(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) - N(x)| \le N(x) / n\).

public theorem_wanted karp_luby_dnf_counting :
    ∃ 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) : ℚ) - (dnfCountOf x : ℚ)| ≤
            (dnfCountOf x : ℚ) / (prec.length : ℚ)} ≥
          2 * 2 ^ (p.eval (x.length + prec.length))

Sources

• R. M. Karp and M. Luby, "Monte-Carlo algorithms for enumeration and reliability problems", Proceedings of the Twenty-Fourth Annual Symposium on Foundations of Computer Science (FOCS 1983), 56-64.

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 · Number of satisfying assignments of an encoded DNF formula · Polynomial-time computable functions

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.