Bit-string encoding of SUBSET-SUM instances to Value of the empty bit list

DefinitionBit-string encoding of SUBSET-SUM instances#✓fully proved

The instance with numbers \(a_1, \dots, a_r\) and target \(t\) is encoded as the block of \(t\) followed by the blocks of \(a_1, \dots, a_r\) in order. The block of a number is its binary expansion, least significant bit first and empty for the number \(0\), made self-delimiting by writing each bit \(c\) as \(1c\) and appending a final \(0\).

def encodeSS (as : List ℕ) (t : ℕ) : List Bool :=
  delimit (encodeNat t) ++ as.flatMap fun a => delimit (encodeNat a)

Uses 1 · Used by 18

Statement usesSelf-delimiting form of a bitstring

Used byPadding reduction has linear output length · Correctness of the encoded SUBSET-SUM to PARTITION reduction · Encoded SUBSET-SUM to PARTITION map has linear output length · Encoded reduction from PARTITION to SUBSET-SUM · Correctness of the encoded PARTITION to SUBSET-SUM reduction · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Quadratic run of the padding machine on canonical instances · Raw-input PARTITION membership machine runs in quadratic time · Canonical PARTITION membership transducer runs in quadratic time · PARTITION membership instance has linear bitlength · Fixed no-instance of SUBSET-SUM · Reduction from VERTEX-COVER to SUBSET-SUM · The SUBSET-SUM problem · The fixed no-instance of SUBSET-SUM · Decoding a SUBSET-SUM instance inverts its encoding · Run of the VERTEX-COVER to SUBSET-SUM machine · SUBSET-SUM is characterized by its verifier · SUBSET-SUM is NP-hard

DefinitionThe SUBSET-SUM problem#✓fully proved

The decision problem that accepts a bit string \(x\) exactly when \(x\) encodes a SUBSET-SUM instance with a list of numbers \(a_1, \dots, a_r\) and a target \(t\) such that some sublist of \(a_1, \dots, a_r\) sums to \(t\). A sublist keeps some of the entries in their order, so a number may be used as often as it occurs in the list.

noncomputable def subsetSumDec : MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  decide (∃ as t, encodeSS as t = x ∧ ∃ l : List ℕ, l.Sublist as ∧ l.sum = t)

Uses 2 · Used by 10

Statement usesBit-string encoding of SUBSET-SUM instances · Decision problems

Used byBinary-coded PARTITION is in NP · PARTITION is NP-complete · Correctness of the encoded SUBSET-SUM to PARTITION reduction · Correctness of the encoded PARTITION to SUBSET-SUM reduction · Polynomial-time reduction from SUBSET-SUM to PARTITION · The fixed no-instance of SUBSET-SUM · SUBSET-SUM is characterized by its verifier · SUBSET-SUM is in NP · SUBSET-SUM is NP-complete · SUBSET-SUM is NP-hard

DefinitionPlace value of a vertex pair in the SUBSET-SUM reduction#✓fully proved

The place value of pair number \(q\) is \(4^q\). The numbers of the reduction from VERTEX-COVER to SUBSET-SUM are written in base \(4\), with the digit at position \(q\) belonging to pair \(q\).

def pairDigit (q : ℕ) : ℕ := 4 ^ q

Used by 8

Used byEdge numbers of the SUBSET-SUM reduction · Target of the SUBSET-SUM reduction · The target in base 4 · A subset sum of the reduction's numbers in base 4 · Vertex numbers of the SUBSET-SUM reduction · A vertex number in base 4 · Subset-sum emitter: one vertex number · Run of the VERTEX-COVER to SUBSET-SUM machine

DefinitionPairs touching a vertex#✓fully proved

Let \(p_0, \dots, p_{m-1}\) be the vertex pairs \((i, j)\) with \(i < j < n\) in encoding order (rows \(i\) ascending, within a row \(j\) descending). For a list \(b\) of pair bits, a vertex \(v\) and an index \(q\), the test is true when bit \(b_q\) is set and \(v\) is one of the two entries of \(p_q\). An index past the end of \(b\) counts as an unset bit, and for \(q \ge m\) the pair \(p_q\) is taken to be \((0, 0)\).

def touches (n : ℕ) (bits : List Bool) (v q : ℕ) : Bool :=
  bits.getD q false && (((pairs n).getD q (0, 0)).1 == v || ((pairs n).getD q (0, 0)).2 == v)

Uses 1 · Used by 7

Statement usesVertex pairs in encoding order

Used byVertex covers of size \(k\) match subset sums hitting the target · Vertices of a set touching a vertex pair · A subset sum of the reduction's numbers in base 4 · Vertex numbers of the SUBSET-SUM reduction · A vertex number in base 4 · Touch bits from the pair walk of a vertex · Subset-sum emitter: one vertex number

DefinitionVertex numbers of the SUBSET-SUM reduction#✓fully proved

Let \(p_0, \dots, p_{m-1}\) be the vertex pairs \((i, j)\) with \(i < j < n\) in encoding order (rows \(i\) ascending, within a row \(j\) descending), and let \(b\) be a list of pair bits. The number of a vertex \(v\) is \(4^m + \sum 4^q\), the sum over the indices \(q < m\) such that bit \(b_q\) is set and \(v\) is an entry of \(p_q\), where an index past the end of \(b\) counts as unset. In base \(4\) it has digit \(1\) at position \(m\) and at each such \(q\), and \(0\) elsewhere.

def vtxNum (n : ℕ) (bits : List Bool) (v : ℕ) : ℕ :=
  4 ^ (pairs n).length +
    (((List.range (pairs n).length).filter fun q => touches n bits v q).map pairDigit).sum

Uses 3 · Used by 8

Statement usesPlace value of a vertex pair in the SUBSET-SUM reduction · Vertex pairs in encoding order · Pairs touching a vertex

Used byVertex covers of size \(k\) match subset sums hitting the target · Sublists of the reduction's numbers as vertex and pair sets · Numbers of the SUBSET-SUM reduction · A subset sum of the reduction's numbers in base 4 · A vertex number in base 4 · Subset-sum emitter: one vertex number · Run of the vertex-number phase of the subset-sum emitter · Run of the VERTEX-COVER to SUBSET-SUM machine

DefinitionEdge numbers of the SUBSET-SUM reduction#✓fully proved

Given a list \(b\) of pair bits and a pair index \(q\), the number of pair \(q\) is \(4^q\) if bit \(b_q\) is set and \(0\) otherwise; an index past the end of \(b\) counts as an unset bit.

def edgeNum (bits : List Bool) (q : ℕ) : ℕ := if bits.getD q false then pairDigit q else 0

Uses 1 · Used by 5

Statement usesPlace value of a vertex pair in the SUBSET-SUM reduction

Used byVertex covers of size \(k\) match subset sums hitting the target · Sublists of the reduction's numbers as vertex and pair sets · Numbers of the SUBSET-SUM reduction · A subset sum of the reduction's numbers in base 4 · Run of the VERTEX-COVER to SUBSET-SUM machine

DefinitionTarget of the SUBSET-SUM reduction#✓fully proved

Let \(m = n(n-1)/2\) be the number of vertex pairs \((i, j)\) with \(i < j < n\), and let \(b\) be a list of pair bits. For \(k \in \mathbb{N}\) the target is \(k \cdot 4^m + \sum 2 \cdot 4^q\), the sum over the indices \(q < m\) such that bit \(b_q\) is set (an index past the end of \(b\) counts as unset). So the quotient of the target by \(4^m\) is \(k\), and its base-\(4\) digit at position \(q < m\) is \(2\) when \(b_q\) is set and \(0\) otherwise.

def ssTarget (k n : ℕ) (bits : List Bool) : ℕ :=
  k * 4 ^ (pairs n).length +
    (((List.range (pairs n).length).filter fun q => bits.getD q false).map
      fun q => 2 * pairDigit q).sum

Uses 2 · Used by 5

Statement usesPlace value of a vertex pair in the SUBSET-SUM reduction · Vertex pairs in encoding order

Used byVertex covers of size \(k\) match subset sums hitting the target · Reduction from VERTEX-COVER to SUBSET-SUM · The target in base 4 · Run of the VERTEX-COVER to SUBSET-SUM machine · SUBSET-SUM is NP-hard

DefinitionNumbers of the SUBSET-SUM reduction#✓fully proved

For \(n\) vertices and a list \(b\) of pair bits, with \(m = n(n-1)/2\) vertex pairs, the numbers of the instance are the vertex numbers of \(v = 0, \dots, n - 1\), in this order, followed by the edge numbers of the pairs \(q = 0, \dots, m - 1\), in this order.

def ssNums (n : ℕ) (bits : List Bool) : List ℕ :=
  (List.range n).map (vtxNum n bits) ++ (List.range (pairs n).length).map (edgeNum bits)

Uses 3 · Used by 5

Statement usesEdge numbers of the SUBSET-SUM reduction · Vertex pairs in encoding order · Vertex numbers of the SUBSET-SUM reduction

Used byVertex covers of size \(k\) match subset sums hitting the target · Sublists of the reduction's numbers as vertex and pair sets · Reduction from VERTEX-COVER to SUBSET-SUM · Run of the VERTEX-COVER to SUBSET-SUM machine · SUBSET-SUM is NP-hard

DefinitionFixed no-instance of SUBSET-SUM#✓fully proved

The encoding of the SUBSET-SUM instance with no numbers and target \(1\). It is a no-instance, because the only sublist of the empty list sums to \(0\).

def noSS : List Bool := encodeSS [] 1

Uses 1 · Used by 9

Statement usesBit-string encoding of SUBSET-SUM instances

Used byProgram of the raw-input PARTITION membership machine · Encoded reduction from PARTITION to SUBSET-SUM · Correctness of the encoded PARTITION to SUBSET-SUM reduction · Raw-input PARTITION membership machine runs in quadratic time · Reduction from VERTEX-COVER to SUBSET-SUM · The fixed no-instance of SUBSET-SUM · The subset-sum emitter machine · Run of the VERTEX-COVER to SUBSET-SUM machine · SUBSET-SUM is NP-hard

DefinitionReduction from VERTEX-COVER to SUBSET-SUM#✓fully proved

The map on bit strings reads \(x\) as \(k\) ones, a zero, \(n\) ones, a zero and a remaining list \(b\) of pair bits. If this parse succeeds and \(b\) has exactly \(n(n-1)/2\) bits, one per vertex pair, then \(x\) is sent to the encoding of the SUBSET-SUM instance whose numbers are the numbers of the reduction for \(n\) and \(b\) and whose target is the target for \(k\), \(n\) and \(b\). Otherwise \(x\) is sent to the fixed no-instance with no numbers and target \(1\).

def reduceSS (x : List Bool) : List Bool :=
  match decodeKG x with
  | some (k, n, bits) =>
      if bits.length = (pairs n).length then encodeSS (ssNums n bits) (ssTarget k n bits)
      else noSS
  | none => noSS

Uses 6 · Used by 3

Statement usesDecoding a graph instance · Bit-string encoding of SUBSET-SUM instances · Fixed no-instance of SUBSET-SUM · Vertex pairs in encoding order · Numbers of the SUBSET-SUM reduction · Target of the SUBSET-SUM reduction

Used byRun of the VERTEX-COVER to SUBSET-SUM machine · The VERTEX-COVER to SUBSET-SUM reduction is polynomial-time · SUBSET-SUM is NP-hard

TheoremThe fixed no-instance of SUBSET-SUM#✓fully proved

The encoded SUBSET-SUM instance with no numbers and target \(1\) is a no-instance: the SUBSET-SUM decision problem returns false on it.

theorem subsetSumDec_noSS : subsetSumDec noSS = false

Uses 5 · Used by 2

Statement usesFixed no-instance of SUBSET-SUM · The SUBSET-SUM problem

Proof usesBit-string encoding of SUBSET-SUM instances · Self-delimiting form of a bitstring · Parsing one self-delimiting block

Used byCorrectness of the encoded PARTITION to SUBSET-SUM reduction · SUBSET-SUM is NP-hard

TheoremBase-4 expansions with digits below \(4\) are unique#✓fully proved

Let \(m, A, B \in \mathbb{N}\) and let \(d, e : \mathbb{N} \to \mathbb{N}\) satisfy \(d(q) < 4\) and \(e(q) < 4\) for every \(q < m\). Then \(A \cdot 4^m + \sum_{q < m} d(q) \, 4^q = B \cdot 4^m + \sum_{q < m} e(q) \, 4^q\) holds if and only if \(A = B\) and \(d(q) = e(q)\) for every \(q < m\).

theorem add_sum_digits_eq_iff {m A B : ℕ} {d e : ℕ → ℕ} (hd : ∀ q < m, d q < 4)
    (he : ∀ q < m, e q < 4) :
    A * 4 ^ m + ∑ q ∈ Finset.range m, d q * 4 ^ q =
        B * 4 ^ m + ∑ q ∈ Finset.range m, e q * 4 ^ q ↔
      A = B ∧ ∀ q < m, d q = e q

Used by 1

Used byVertex covers of size \(k\) match subset sums hitting the target

TheoremSublists of the reduction's numbers as vertex and pair sets#✓fully proved

Let \(n, t \in \mathbb{N}\), let \(b\) be a list of booleans, and let \(m\) be the length of the list of vertex pairs \((i, j)\), \(i < j < n\). Write \(x_v\) for the vertex number of \(v\) and \(y_q\) for the pair number of \(q\) defined from \(n\) and \(b\). Some sublist (a subsequence, not necessarily contiguous) of the reduction's numbers for \(n\) and \(b\) sums to \(t\) if and only if there are finite sets \(S\) of vertices \(v < n\) and \(F\) of pair indices \(q < m\) with \(\sum_{v \in S} x_v + \sum_{q \in F} y_q = t\).

theorem exists_sublist_ssNums_iff {n t : ℕ} {bits : List Bool} :
    (∃ l : List ℕ, l.Sublist (ssNums n bits) ∧ l.sum = t) ↔
      ∃ S ⊆ Finset.range n, ∃ F ⊆ Finset.range (pairs n).length,
        ∑ v ∈ S, vtxNum n bits v + ∑ q ∈ F, edgeNum bits q = t

Uses 4 · Used by 1

Statement usesEdge numbers of the SUBSET-SUM reduction · Vertex pairs in encoding order · Numbers of the SUBSET-SUM reduction · Vertex numbers of the SUBSET-SUM reduction

Used byVertex covers of size \(k\) match subset sums hitting the target

TheoremA vertex number in base 4#✓fully proved

Let \(n, v \in \mathbb{N}\), let \(b\) be a list of booleans, and let \(m\) be the length of the list of vertex pairs \((i, j)\), \(i < j < n\). The vertex number of \(v\) defined from \(n\) and \(b\) equals \(4^m + \sum_{q < m} t_q 4^q\), where \(t_q = 1\) if entry \(q\) of \(b\) (counting from \(0\)) is true and \(v\) is an endpoint of the \(q\)-th pair, and \(t_q = 0\) otherwise.

theorem vtxNum_eq (n : ℕ) (bits : List Bool) (v : ℕ) :
    vtxNum n bits v = 4 ^ (pairs n).length +
      ∑ q ∈ Finset.range (pairs n).length, (if touches n bits v q then 1 else 0) * 4 ^ q

Uses 4 · Used by 1

Statement usesVertex pairs in encoding order · Pairs touching a vertex · Vertex numbers of the SUBSET-SUM reduction

Proof usesPlace value of a vertex pair in the SUBSET-SUM reduction

Used byA subset sum of the reduction's numbers in base 4

TheoremThe target in base 4#✓fully proved

Let \(k, n \in \mathbb{N}\), let \(b\) be a list of booleans, and let \(m\) be the length of the list of vertex pairs \((i, j)\), \(i < j < n\). The reduction's target for \(k\), \(n\) and \(b\) equals \(k \cdot 4^m + \sum_{q < m} c_q 4^q\), where \(c_q = 2\) if entry \(q\) of \(b\) (counting from \(0\)) is true and \(c_q = 0\) otherwise, in particular when \(b\) has no entry \(q\).

theorem ssTarget_eq (k n : ℕ) (bits : List Bool) :
    ssTarget k n bits = k * 4 ^ (pairs n).length +
      ∑ q ∈ Finset.range (pairs n).length, (if bits.getD q false then 2 else 0) * 4 ^ q

Uses 3 · Used by 1

Statement usesVertex pairs in encoding order · Target of the SUBSET-SUM reduction

Proof usesPlace value of a vertex pair in the SUBSET-SUM reduction

Used byVertex covers of size \(k\) match subset sums hitting the target

TheoremA subset sum of the reduction's numbers in base 4#✓fully proved

Let \(n \in \mathbb{N}\), let \(b\) be a list of booleans, let \(m\) be the length of the list of vertex pairs \((i, j)\), \(i < j < n\), and let \(S\) and \(F\) be finite sets of natural numbers with every element of \(F\) below \(m\). Write \(x_v\) for the vertex number of \(v\) and \(y_q\) for the pair number of \(q\) defined from \(n\) and \(b\). For \(q < m\) let \(t_{v,q} = 1\) if entry \(q\) of \(b\) (counting from \(0\)) is true and \(v\) is an endpoint of the \(q\)-th pair, and \(t_{v,q} = 0\) otherwise; let \(f_q = 1\) if \(q \in F\) and entry \(q\) of \(b\) is true, and \(f_q = 0\) otherwise. An absent entry counts as false. Then \(\sum_{v \in S} x_v + \sum_{q \in F} y_q = |S| \cdot 4^m + \sum_{q < m} \left(\sum_{v \in S} t_{v,q} + f_q\right) 4^q\).

theorem sum_vtxNum_add_sum_edgeNum {n : ℕ} {bits : List Bool} {S F : Finset ℕ}
    (hF : F ⊆ Finset.range (pairs n).length) :
    ∑ v ∈ S, vtxNum n bits v + ∑ q ∈ F, edgeNum bits q =
      S.card * 4 ^ (pairs n).length + ∑ q ∈ Finset.range (pairs n).length,
        ((∑ v ∈ S, if touches n bits v q then 1 else 0) +
          if q ∈ F ∧ bits.getD q false then 1 else 0) * 4 ^ q

Uses 6 · Used by 1

Statement usesEdge numbers of the SUBSET-SUM reduction · Vertex pairs in encoding order · Pairs touching a vertex · Vertex numbers of the SUBSET-SUM reduction

Proof usesPlace value of a vertex pair in the SUBSET-SUM reduction · A vertex number in base 4

Used byVertex covers of size \(k\) match subset sums hitting the target

TheoremVertices of a set touching a vertex pair#✓fully proved

Let \(n\) be a natural number, let \(p_0, \dots, p_{m-1}\) be the vertex pairs in encoding order for \(n\), let \(b\) be a list of pair bits, let \(q < m\) with \(p_q = (i, j)\), and let \(S\) be a finite set of natural numbers. Write \([P]\) for \(1\) if \(P\) holds and \(0\) otherwise. Then the number of \(v \in S\) for which the test whether pair \(q\) touches \(v\) under \(b\) is true equals \([i \in S] + [j \in S]\) if the bit \(b_q\) is set, and \(0\) otherwise (an index past the end of \(b\) counts as an unset bit).

theorem sum_touches_eq {n : ℕ} {bits : List Bool} {q : ℕ} (hq : q < (pairs n).length)
    (S : Finset ℕ) :
    (∑ v ∈ S, if touches n bits v q then 1 else 0) =
      if bits.getD q false then
        (if (pairs n)[q].1 ∈ S then 1 else 0) + if (pairs n)[q].2 ∈ S then 1 else 0
      else 0

Uses 3 · Used by 1

Statement usesVertex pairs in encoding order · Pairs touching a vertex

Proof usesMembership in the vertex pairs

Used byVertex covers of size \(k\) match subset sums hitting the target

TheoremVertex covers in terms of the pair bits#✓fully proved

Let \(n \in \mathbb{N}\), let \(b\) be a list of booleans with one entry for each pair in the list of vertex pairs \((i, j)\), \(i < j < n\), and let \(G\) be the graph on the vertices \(0, \dots, n - 1\) encoded by the pair bits \(b\). Let \(s\) be a finite set of vertices of \(G\) and \(S\) a finite set of natural numbers such that each vertex \(i\) lies in \(s\) exactly when \(i \in S\). Then \(s\) is a vertex cover of \(G\) if and only if, for every index \(q\) (counting from \(0\)) of the pair list whose entry in \(b\) is true, the \(q\)-th pair \((i_q, j_q)\) satisfies \(i_q \in S\) or \(j_q \in S\).

theorem isVertexCover_toGraph_iff {n : ℕ} {bits : List Bool}
    (h : bits.length = (pairs n).length) {s : Finset (Fin n)} {S : Finset ℕ}
    (hsS : ∀ i : Fin n, i ∈ s ↔ i.val ∈ S) :
    (toGraph n bits).IsVertexCover (s : Set (Fin n)) ↔
      ∀ q (hq : q < (pairs n).length), bits.getD q false = true →
        (pairs n)[q].1 ∈ S ∨ (pairs n)[q].2 ∈ S

Uses 6 · Used by 1

Statement usesVertex pairs in encoding order · The graph encoded by pair bits

Proof usesAdjacency bit of a vertex pair · Pair bits are read off by position · Membership in the vertex pairs · The vertex pairs are listed without repetition

Used byVertex covers of size \(k\) match subset sums hitting the target

TheoremVertex covers of size \(k\) match subset sums hitting the target#✓fully proved

Let \(k, n \in \mathbb{N}\) and let \(b\) be a list of booleans with one entry for each pair in the list of vertex pairs \((i, j)\), \(i < j < n\). Let \(G\) be the graph on the vertices \(0, \dots, n - 1\) encoded by the pair bits \(b\). Then \(G\) has a vertex cover with exactly \(k\) vertices if and only if some sublist (a subsequence, not necessarily contiguous) of the reduction's numbers for \(n\) and \(b\) sums to the reduction's target for \(k\), \(n\) and \(b\).

theorem exists_cover_iff_exists_sublist {k n : ℕ} {bits : List Bool}
    (h : bits.length = (pairs n).length) :
    (∃ s : Finset (Fin n), s.card = k ∧ (toGraph n bits).IsVertexCover (s : Set (Fin n))) ↔
      ∃ l : List ℕ, l.Sublist (ssNums n bits) ∧ l.sum = ssTarget k n bits

Uses 13 · Used by 1

Statement usesVertex pairs in encoding order · Numbers of the SUBSET-SUM reduction · Target of the SUBSET-SUM reduction · The graph encoded by pair bits

Proof usesBase-4 expansions with digits below \(4\) are unique · Edge numbers of the SUBSET-SUM reduction · Sublists of the reduction's numbers as vertex and pair sets · Vertex covers in terms of the pair bits · The target in base 4 · Vertices of a set touching a vertex pair · A subset sum of the reduction's numbers in base 4 · Pairs touching a vertex · Vertex numbers of the SUBSET-SUM reduction

Used bySUBSET-SUM is NP-hard

TheoremValue of the empty bit list#✓fully proved

The empty bit list, read as a binary number least significant bit first, has value \(0\).

@[simp] theorem bitsVal_nil : bitsVal [] = 0

Uses 1

Statement usesValue of a little-endian bit list

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.