Label after the move phase of the KG-map machine to SAT ≤ CLIQUE is polynomial-time

DefinitionLabel after the move phase of the KG-map machine#✓fully proved

The map from the modes of the KG-map machine to its labels that sends the flip mode to the label output the pair bits and the vertex-cover mode to the subtraction label. The machine goes to this label after moving the pair bits.

def Mode.next : Mode → Lab
  | .flip => .outY
  | .vc => .sub

Uses 2 · Used by 3

Statement usesLabels of the KG-map machine · Modes of the CLIQUE/VERTEX-COVER reduction machine

Used byMoving the pair bits onto stack \(Y\) · The KG-map machine · Correctness and running time of the KG-map machine

DefinitionCounter of the first output number of the KG-map machine#✓fully proved

The map from the modes of the KG-map machine to its stacks that sends the flip mode to the counter \(A\) and the vertex-cover mode to the counter \(D\).

This is the counter the machine drains last, as the first number of its output: \(A\) holds \(k\), and in the vertex-cover mode \(D\) holds \(n - k\) by then.

def Mode.ctr : Mode → K
  | .flip => .A
  | .vc => .D

Uses 2 · Used by 3

Statement usesStacks of the CLIQUE to VERTEX-COVER reduction machine · Modes of the CLIQUE/VERTEX-COVER reduction machine

Used byOutput phase of the KG-map machine · The KG-map machine · Number output of the clique reduction machine

DefinitionThe KG-map machine#✓fully proved

For a mode \(m\) (flip or vc), the KG-map machine \(M_m\) is the multi-stack machine with stacks \(X\), \(A\), \(B\), \(D\), \(Y\) of symbols and an output stack \(O\) of bits, whose labels act as follows; the counters \(A\), \(B\), \(D\) use a fixed unit symbol.

• Read \(k\): if \(X\) is empty, go to the failure label. Otherwise pop \(X\); if the popped symbol is the input bit \(\mathrm{bit}(\mathit{true})\), push a unit onto \(A\) and repeat, else go to read \(n\).
• Read \(n\): if \(X\) is empty, go to the failure label. Otherwise pop \(X\); if the popped symbol is \(\mathrm{bit}(\mathit{true})\), push a unit onto \(B\) and onto \(D\) and repeat, else go to move.
• Move: if \(X\) is empty, go to output pair bits (flip) or subtract (vc). Otherwise pop \(X\), push \(\mathrm{val}(b)\) onto \(Y\), where \(b\) is true exactly when the popped symbol was \(\mathrm{bit}(\mathit{true})\), and repeat.
• Subtract: pop \(A\). If \(A\) was empty, go to output pair bits. Otherwise pop \(D\); if \(D\) was nonempty repeat, else go to the failure label.
• Output pair bits: if \(Y\) is empty, push false onto \(O\) and go to output \(n\). Otherwise pop \(Y\), push \(\beta_m(b)\) onto \(O\), where \(b\) is true exactly when the popped symbol was \(\mathrm{val}(\mathit{true})\) and \(\beta_m\) is negation for flip and the identity for vc, and repeat.
• Output \(n\): pop \(B\); if \(B\) was nonempty, push true onto \(O\) and repeat, else go to separator.
• Separator: push false onto \(O\) and go to output last number.
• Output last number: as output \(n\), but popping the counter of \(m\) (\(A\) for flip, \(D\) for vc) and going to the halting label when it is empty.
• Failure: push the bits true, false, false of the fixed no-instance (the encoding of \(k = 1\) on the empty graph) onto \(O\) so that \(O\) starts with them, and go to the halting label.
• Halting label: halt.

Cslib.Complexity.Karp.KGMap.prog · 21 lines

def prog (m : Mode) : Lab → TM2.Stmt Γ Lab Bool
  | .rdK => .peek .X (fun _ o => o.isNone) <| .branch id (.goto fun _ => .bad) <|
      .pop .X (fun _ o => isT o) <| .branch id
        (.push .A (fun _ => U) (.goto fun _ => .rdK)) (.goto fun _ => .rdN)
  | .rdN => .peek .X (fun _ o => o.isNone) <| .branch id (.goto fun _ => .bad) <|
      .pop .X (fun _ o => isT o) <| .branch id
        (.push .B (fun _ => U) <| .push .D (fun _ => U) <| .goto fun _ => .rdN)
        (.goto fun _ => .mv)
  | .mv => .peek .X (fun _ o => o.isNone) <| .branch id (.goto fun _ => m.next) <|
      .pop .X (fun _ o => isT o) <| .push .Y (fun s => Sym.val s) <| .goto fun _ => .mv
  | .sub => .pop .A (fun _ o => o.isSome) <| .branch id
      (.pop .D (fun _ o => o.isSome) <| .branch id (.goto fun _ => .sub) (.goto fun _ => .bad))
      (.goto fun _ => .outY)
  | .outY => .peek .Y (fun _ o => o.isNone) <| .branch id
      (.push .O (fun _ => false) (.goto fun _ => .outB)) <|
      .pop .Y (fun _ o => isV o) <| .push .O (fun s => m.fb s) <| .goto fun _ => .outY
  | .outB => xfer .B [⟨.O, true⟩] .outB .sep
  | .sep => emit .O [false] .outK
  | .outK => xfer m.ctr [⟨.O, true⟩] .outK .done
  | .bad => emitR .O noKG .done
  | .done => .halt

Uses 16 · Used by 14

Statement usesStacks of the CLIQUE to VERTEX-COVER reduction machine · Labels of the KG-map machine · Modes of the CLIQUE/VERTEX-COVER reduction machine · Counter of the first output number of the KG-map machine · Pair-bit transform of each mode · Label after the move phase of the KG-map machine · Counter unit symbol of the clique reduction machine · Test for the input bit true · Test for the moved bit true · Stack alphabets of the clique reduction machine · Fixed no-instance · Stack alphabet of the SAT verifier · Flag bit of a machine state · Pushing a constant list · Prepending a constant list · Counter transfer loop

Used byCLIQUE ≤ INDEPENDENT-SET is polynomial-time · INDEPENDENT-SET ≤ VERTEX-COVER is polynomial-time · The CLIQUE-to-INDEPENDENT-SET and INDEPENDENT-SET-to-VERTEX-COVER map as a host component · Moving the pair bits onto stack \(Y\) · Output phase of the KG-map machine · Output loop for the pair bits of the KG-map machine · Unterminated first unary number in the KG-map machine · Reading the first unary number in the KG-map machine · Unterminated second unary number in the KG-map machine · Reading the second unary number in the KG-map machine · Correctness and running time of the KG-map machine · Failed subtraction in the KG-map machine · Subtraction loop of the clique reduction machine · Number output of the clique reduction machine

DefinitionStart label of the KG-map machine#✓fully proved

The KG-map machine starts at the label read \(k\).

def start : Lab := .rdK

Uses 1 · Used by 3

Statement usesLabels of the KG-map machine

Used byCLIQUE ≤ INDEPENDENT-SET is polynomial-time · INDEPENDENT-SET ≤ VERTEX-COVER is polynomial-time · Correctness and running time of the KG-map machine

TheoremReading the first unary number in the KG-map machine#✓fully proved

Let \(m\) be a mode, \(k\) and \(i\) natural numbers and \(r\) a list of bits. Consider a configuration of the KG-map machine \(M_m\) at the label read \(k\), with any internal bit, in which stack \(X\) holds the input symbols \(\mathrm{bit}(b)\) for the bits \(b\) of the list of \(k\) trues, a false and then \(r\), top first, and stack \(A\) holds \(i\) copies of the unit symbol. Then in exactly \(k + 1\) steps \(M_m\) reaches the label read \(n\) with \(X\) holding \(\mathrm{bit}(b)\) for the bits \(b\) of \(r\), \(A\) holding \(i + k\) copies of the unit symbol, and every stack other than \(X\) and \(A\) unchanged.

theorem rdK_some (k : ℕ) : ∀ (i : ℕ) (v : Bool) (St : ∀ k, List (Γ k)) (r : List Bool),
    St .X = (List.replicate k true ++ false :: r).map Sym.bit → St .A = cnt U i →
    ∃ v' S', Run (prog m) (k + 1) ⟨some .rdK, v, St⟩ ⟨some .rdN, v', S'⟩ ∧
      S' .X = r.map Sym.bit ∧ S' .A = cnt U (i + k) ∧ ∀ j, j ≠ .X → j ≠ .A → S' j = St j

Uses 11 · Used by 1

Statement usesStacks of the CLIQUE to VERTEX-COVER reduction machine · Labels of the KG-map machine · Modes of the CLIQUE/VERTEX-COVER reduction machine · Counter unit symbol of the clique reduction machine · The KG-map machine · Stack alphabets of the clique reduction machine · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine · Unary counter

Proof usesTest for the input bit true · A single step executes the statement at the current label

Used byCorrectness and running time of the KG-map machine

TheoremUnterminated first unary number in the KG-map machine#✓fully proved

Let \(m\) be a mode and \(r\) a list of bits on which reading a unary length prefix fails (this happens exactly when \(r\) contains no false). From any configuration of the KG-map machine \(M_m\) at the label read \(k\), with any internal bit, in which stack \(X\) holds the input symbols \(\mathrm{bit}(b)\) for the bits \(b\) of \(r\), top first, \(M_m\) reaches the failure label in exactly \(|r| + 1\) steps, with every stack other than \(X\) and \(A\) unchanged.

theorem rdK_none : ∀ (r : List Bool), readUnaryLength r = none →
    ∀ (v : Bool) (St : ∀ k, List (Γ k)), St .X = r.map Sym.bit →
      ∃ v' S', Run (prog m) (r.length + 1) ⟨some .rdK, v, St⟩ ⟨some .bad, v', S'⟩ ∧
        ∀ j, j ≠ .X → j ≠ .A → S' j = St j

Uses 11 · Used by 1

Statement usesStacks of the CLIQUE to VERTEX-COVER reduction machine · Labels of the KG-map machine · Modes of the CLIQUE/VERTEX-COVER reduction machine · The KG-map machine · Stack alphabets of the clique reduction machine · Stack alphabet of the SAT verifier · Reading a unary length prefix · Exact-length runs of a TM2 machine

Proof usesCounter unit symbol of the clique reduction machine · Test for the input bit true · A single step executes the statement at the current label

Used byCorrectness and running time of the KG-map machine

TheoremReading the second unary number in the KG-map machine#✓fully proved

Let \(m\) be a mode, \(n\) and \(i\) natural numbers and \(r\) a list of bits. Consider a configuration of the KG-map machine \(M_m\) at the label read \(n\), with any internal bit, in which stack \(X\) holds the input symbols \(\mathrm{bit}(b)\) for the bits \(b\) of the list of \(n\) trues, a false and then \(r\), top first, and stacks \(B\) and \(D\) each hold \(i\) copies of the unit symbol. Then in exactly \(n + 1\) steps \(M_m\) reaches the label move with \(X\) holding \(\mathrm{bit}(b)\) for the bits \(b\) of \(r\), \(B\) and \(D\) each holding \(i + n\) copies of the unit symbol, and every stack other than \(X\), \(B\) and \(D\) unchanged.

theorem rdN_some (n : ℕ) : ∀ (i : ℕ) (v : Bool) (St : ∀ k, List (Γ k)) (r : List Bool),
    St .X = (List.replicate n true ++ false :: r).map Sym.bit → St .B = cnt U i →
    St .D = cnt U i →
    ∃ v' S', Run (prog m) (n + 1) ⟨some .rdN, v, St⟩ ⟨some .mv, v', S'⟩ ∧
      S' .X = r.map Sym.bit ∧ S' .B = cnt U (i + n) ∧ S' .D = cnt U (i + n) ∧
      ∀ j, j ≠ .X → j ≠ .B → j ≠ .D → S' j = St j

Uses 11 · Used by 1

Statement usesStacks of the CLIQUE to VERTEX-COVER reduction machine · Labels of the KG-map machine · Modes of the CLIQUE/VERTEX-COVER reduction machine · Counter unit symbol of the clique reduction machine · The KG-map machine · Stack alphabets of the clique reduction machine · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine · Unary counter

Proof usesTest for the input bit true · A single step executes the statement at the current label

Used byCorrectness and running time of the KG-map machine

TheoremUnterminated second unary number in the KG-map machine#✓fully proved

Let \(m\) be a mode and \(r\) a list of bits on which reading a unary length prefix fails (this happens exactly when \(r\) contains no false). From any configuration of the KG-map machine \(M_m\) at the label read \(n\), with any internal bit, in which stack \(X\) holds the input symbols \(\mathrm{bit}(b)\) for the bits \(b\) of \(r\), top first, \(M_m\) reaches the failure label in exactly \(|r| + 1\) steps, with every stack other than \(X\), \(B\) and \(D\) unchanged.

theorem rdN_none : ∀ (r : List Bool), readUnaryLength r = none →
    ∀ (v : Bool) (St : ∀ k, List (Γ k)), St .X = r.map Sym.bit →
      ∃ v' S', Run (prog m) (r.length + 1) ⟨some .rdN, v, St⟩ ⟨some .bad, v', S'⟩ ∧
        ∀ j, j ≠ .X → j ≠ .B → j ≠ .D → S' j = St j

Uses 11 · Used by 1

Statement usesStacks of the CLIQUE to VERTEX-COVER reduction machine · Labels of the KG-map machine · Modes of the CLIQUE/VERTEX-COVER reduction machine · The KG-map machine · Stack alphabets of the clique reduction machine · Stack alphabet of the SAT verifier · Reading a unary length prefix · Exact-length runs of a TM2 machine

Proof usesCounter unit symbol of the clique reduction machine · Test for the input bit true · A single step executes the statement at the current label

Used byCorrectness and running time of the KG-map machine

TheoremMoving the pair bits onto stack \(Y\)#✓fully proved

Fix a mode \(m\) of the CLIQUE/VERTEX-COVER reduction machine, a list of bits \(r\) and a list of symbols \(y\). Start the machine for \(m\) at the label for moving the pair bits, with any internal state and any stacks such that stack \(X\) holds \(r\) as the symbols \(\mathrm{bit}(b)\) and stack \(Y\) holds \(y\). Then after exactly \(|r| + 1\) steps it is at the label that follows moving the pair bits in mode \(m\), with some internal state and stacks in which \(Y\) holds the symbols \(\mathrm{val}(b)\) for the bits \(b\) of \(r\), in reverse order, on top of \(y\), and every stack other than \(X\) and \(Y\) is unchanged.

theorem mv_run (r : List Bool) : ∀ (v : Bool) (St : ∀ k, List (Γ k)) (ys : List Sym),
    St .X = r.map Sym.bit → St .Y = ys →
    ∃ v' S', Run (prog m) (r.length + 1) ⟨some .mv, v, St⟩ ⟨some m.next, v', S'⟩ ∧
      S' .Y = (r.map Sym.val).reverse ++ ys ∧ ∀ j, j ≠ .X → j ≠ .Y → S' j = St j

Uses 10 · Used by 1

Statement usesStacks of the CLIQUE to VERTEX-COVER reduction machine · Labels of the KG-map machine · Modes of the CLIQUE/VERTEX-COVER reduction machine · Label after the move phase of the KG-map machine · The KG-map machine · Stack alphabets of the clique reduction machine · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine

Proof usesTest for the input bit true · A single step executes the statement at the current label

Used byCorrectness and running time of the KG-map machine

TheoremSubtraction loop of the clique reduction machine#✓fully proved

Let \(m\) be a mode of the machine, let \(k \le n\) be natural numbers, and let \(S\) be stack contents in which the counter stack \(A\) holds \(U^k\) (\(k\) copies of the unit symbol \(U\)) and the counter stack \(D\) holds \(U^n\). Then for every Boolean local state \(v\) there are a local state \(v'\) and stack contents \(S'\) such that the machine of mode \(m\) runs in exactly \(k + 1\) steps from label \(\mathsf{sub}\) with local state \(v\) and stacks \(S\) to label \(\mathsf{outY}\) with local state \(v'\) and stacks \(S'\), the stack \(D\) of \(S'\) holds \(U^{n-k}\), and every stack other than \(A\) and \(D\) has the same contents in \(S'\) as in \(S\).

theorem sub_le (k : ℕ) : ∀ (n : ℕ) (v : Bool) (St : ∀ k, List (Γ k)), k ≤ n →
    St .A = cnt U k → St .D = cnt U n →
    ∃ v' S', Run (prog m) (k + 1) ⟨some .sub, v, St⟩ ⟨some .outY, v', S'⟩ ∧
      S' .D = cnt U (n - k) ∧ ∀ j, j ≠ .A → j ≠ .D → S' j = St j

Uses 10 · Used by 1

Statement usesStacks of the CLIQUE to VERTEX-COVER reduction machine · Labels of the KG-map machine · Modes of the CLIQUE/VERTEX-COVER reduction machine · Counter unit symbol of the clique reduction machine · The KG-map machine · Stack alphabets of the clique reduction machine · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine · Unary counter

Proof usesA single step executes the statement at the current label

Used byCorrectness and running time of the KG-map machine

TheoremFailed subtraction in the KG-map machine#✓fully proved

Let \(m\) be a mode and \(n < k\) natural numbers. From any configuration of the KG-map machine \(M_m\) at the label subtract, with any internal bit, in which stack \(A\) holds \(k\) copies of the unit symbol and stack \(D\) holds \(n\) copies, \(M_m\) reaches the failure label in exactly \(n + 1\) steps, with every stack other than \(A\) and \(D\) unchanged.

theorem sub_gt (n : ℕ) : ∀ (k : ℕ) (v : Bool) (St : ∀ k, List (Γ k)), n < k →
    St .A = cnt U k → St .D = cnt U n →
    ∃ v' S', Run (prog m) (n + 1) ⟨some .sub, v, St⟩ ⟨some .bad, v', S'⟩ ∧
      ∀ j, j ≠ .A → j ≠ .D → S' j = St j

Uses 10 · Used by 1

Statement usesStacks of the CLIQUE to VERTEX-COVER reduction machine · Labels of the KG-map machine · Modes of the CLIQUE/VERTEX-COVER reduction machine · Counter unit symbol of the clique reduction machine · The KG-map machine · Stack alphabets of the clique reduction machine · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine · Unary counter

Proof usesA single step executes the statement at the current label

Used byCorrectness and running time of the KG-map machine

TheoremOutput loop for the pair bits of the KG-map machine#✓fully proved

Let \(m\) be a mode and \(y\) and \(o\) lists of bits. Consider a configuration of the KG-map machine \(M_m\) at the label output pair bits, with any internal bit, in which stack \(Y\) holds the symbols \(\mathrm{val}(b)\) for the bits \(b\) of \(y\), the first bit of \(y\) on top, and the output stack \(O\) holds \(o\). Then in exactly \(|y| + 1\) steps \(M_m\) reaches the label output \(n\) with \(O\) equal, top first, to false, then the reverse of \(\beta_m(y)\), then \(o\), where \(\beta_m\) negates every bit for flip and leaves the bits unchanged for vc; every stack other than \(Y\) and \(O\) is unchanged.

theorem outY_run (ys : List Bool) : ∀ (v : Bool) (St : ∀ k, List (Γ k)) (o : List Bool),
    St .Y = ys.map Sym.val → St .O = o →
    ∃ v' S', Run (prog m) (ys.length + 1) ⟨some .outY, v, St⟩ ⟨some .outB, v', S'⟩ ∧
      S' .O = false :: ((ys.map m.fb).reverse ++ o) ∧ ∀ j, j ≠ .Y → j ≠ .O → S' j = St j

Uses 10 · Used by 1

Statement usesStacks of the CLIQUE to VERTEX-COVER reduction machine · Labels of the KG-map machine · Modes of the CLIQUE/VERTEX-COVER reduction machine · Pair-bit transform of each mode · The KG-map machine · Stack alphabets of the clique reduction machine · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine

Proof usesTest for the moved bit true · A single step executes the statement at the current label

Used byOutput phase of the KG-map machine

TheoremNumber output of the clique reduction machine#✓fully proved

Let \(m\) be a mode of the machine and \(C\) its final counter stack (\(A\) for the flip mode, \(D\) for the vertex-cover mode). Let \(n, c\) be natural numbers, \(u\) a symbol of the alphabet of \(C\), and \(S\) stack contents in which the stack \(B\) holds \(U^n\) (\(n\) copies of the unit symbol \(U\)) and \(C\) holds \(u^c\). Then for every Boolean local state \(v\) there are a local state \(v'\) and stack contents \(S'\) such that the machine of mode \(m\) runs in exactly \(n + c + 3\) steps from label \(\mathsf{outB}\) with local state \(v\) and stacks \(S\) to label \(\mathsf{done}\) with local state \(v'\) and stacks \(S'\), and the output stack \(O\) of \(S'\) holds, from the top, \(c\) copies of \(\mathrm{true}\), then \(\mathrm{false}\), then \(n\) copies of \(\mathrm{true}\), then the contents of \(O\) in \(S\).

theorem tail_run (n c : ℕ) (u : Γ m.ctr) (v : Bool) (St : ∀ k, List (Γ k))
    (hB : St .B = cnt U n) (hC : St m.ctr = cnt u c) :
    ∃ v' S', Run (prog m) (n + c + 3) ⟨some .outB, v, St⟩ ⟨some .done, v', S'⟩ ∧
      S' .O = List.replicate c true ++ false :: (List.replicate n true ++ St .O)

Uses 16 · Used by 1

Statement usesStacks of the CLIQUE to VERTEX-COVER reduction machine · Labels of the KG-map machine · Modes of the CLIQUE/VERTEX-COVER reduction machine · Counter of the first output number of the KG-map machine · Counter unit symbol of the clique reduction machine · The KG-map machine · Stack alphabets of the clique reduction machine · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine · Unary counter

Proof usesFlag bit of a machine state · A single step executes the statement at the current label · Adding units to target stacks · Pushing a constant list · Pushing a list of symbols onto one stack · Running a counter transfer

Used byOutput phase of the KG-map machine

TheoremOutput phase of the KG-map machine#✓fully proved

Let \(m\) be a mode, \(r\) a list of bits and \(n\) and \(c\) natural numbers. Consider a configuration of the KG-map machine \(M_m\) at the label output pair bits, with any internal bit, in which stack \(Y\) holds the symbols \(\mathrm{val}(b)\) for the bits \(b\) of \(r\) in reverse order (the last bit of \(r\) on top), stack \(B\) holds \(n\) copies of the unit symbol, the counter of \(m\) (\(A\) for flip, \(D\) for vc) holds \(c\) copies of some symbol, and the output stack \(O\) is empty. Then in exactly \(|r| + n + c + 4\) steps \(M_m\) reaches the halting label with \(O\) equal, top first, to the encoding of the instance with numbers \(c\) and \(n\) and pair bits \(\beta_m(r)\): \(c\) trues, a false, \(n\) trues, a false, then \(\beta_m(r)\), where \(\beta_m\) negates every bit for flip and leaves the bits unchanged for vc.

theorem out_run (r : List Bool) (n c : ℕ) (u : Γ m.ctr) (v : Bool) (St : ∀ k, List (Γ k))
    (hY : St .Y = (r.map Sym.val).reverse) (hB : St .B = cnt U n) (hC : St m.ctr = cnt u c)
    (hO : St .O = []) :
    ∃ v' S', Run (prog m) (r.length + n + c + 4) ⟨some .outY, v, St⟩ ⟨some .done, v', S'⟩ ∧
      S' .O = encodeKG c n (r.map m.fb)

Uses 14 · Used by 1

Statement usesStacks of the CLIQUE to VERTEX-COVER reduction machine · Labels of the KG-map machine · Modes of the CLIQUE/VERTEX-COVER reduction machine · Counter of the first output number of the KG-map machine · Pair-bit transform of each mode · Counter unit symbol of the clique reduction machine · The KG-map machine · Stack alphabets of the clique reduction machine · Encoding of a graph instance · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine · Unary counter

Proof usesOutput loop for the pair bits of the KG-map machine · Number output of the clique reduction machine

Used byCorrectness and running time of the KG-map machine

TheoremCorrectness and running time of the KG-map machine#✓fully proved

Let \(m\) be a mode and \(x\) a list of bits, and let \(F_m\) be the clique-to-independent-set map on bit strings for flip and the independent-set-to-vertex-cover map for vc. From any configuration of the KG-map machine \(M_m\) at its start label, with any internal bit, in which stack \(X\) holds the input symbols \(\mathrm{bit}(b)\) for the bits \(b\) of \(x\), top first, and every other stack is empty, \(M_m\) reaches the halting label in at most \(3(|x| + 1)\) steps with the output stack \(O\) equal to \(F_m(x)\), top first.

theorem run (m : Mode) (x : List Bool) (v : Bool) (St : ∀ k, List (Γ k))
    (hX : St .X = x.map Sym.bit) (h0 : ∀ k, k ≠ .X → St k = []) :
    ∃ v' S', RunLe (prog m) (3 * (x.length + 1)) ⟨some start, v, St⟩ ⟨some .done, v', S'⟩ ∧
      S' .O = m.f x

Uses 29 · Used by 2

Statement usesStacks of the CLIQUE to VERTEX-COVER reduction machine · Labels of the KG-map machine · Modes of the CLIQUE/VERTEX-COVER reduction machine · Reduction computed in each mode · The KG-map machine · Start label of the KG-map machine · Stack alphabets of the clique reduction machine · Stack alphabet of the SAT verifier · Runs within a step budget

Proof usesPair-bit transform of each mode · Label after the move phase of the KG-map machine · Counter unit symbol of the clique reduction machine · Moving the pair bits onto stack \(Y\) · Output phase of the KG-map machine · Unterminated first unary number in the KG-map machine · Reading the first unary number in the KG-map machine · Unterminated second unary number in the KG-map machine · Reading the second unary number in the KG-map machine · Failed subtraction in the KG-map machine · Subtraction loop of the clique reduction machine · Encoding of a graph instance · Fixed no-instance · Reading a unary length prefix · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Unary counter · Pushing a constant list · Prepending a constant list · Pushing a list of symbols onto one stack

Used byCLIQUE ≤ INDEPENDENT-SET is polynomial-time · INDEPENDENT-SET ≤ VERTEX-COVER is polynomial-time

AbbreviationThe CLIQUE-to-INDEPENDENT-SET and INDEPENDENT-SET-to-VERTEX-COVER map as a host component#✓fully proved

The CLIQUE-to-INDEPENDENT-SET and INDEPENDENT-SET-to-VERTEX-COVER map as a host component. For a mode \(m\), standing for the reduction from CLIQUE to INDEPENDENT-SET or the one from INDEPENDENT-SET to VERTEX-COVER, this is the host component whose stacks (listed as \(X, O, A, B, D, Y\)), stack alphabets, labels and program are those of the Turing machine that computes the reduction of mode \(m\).

abbrev kgMapComp (m : KGMap.Mode) : Host.Comp where
  K := KGMap.K
  Γ := KGMap.Γ
  L := KGMap.Lab
  prog := KGMap.prog m
  ks := [.X, .O, .A, .B, .D, .Y]
  ks_nodup := by decide
  mem_ks k := by cases k <;> decide

Uses 7 · Used by 2

Statement usesComponent machine · Stacks of the CLIQUE to VERTEX-COVER reduction machine · Labels of the KG-map machine · Modes of the CLIQUE/VERTEX-COVER reduction machine · The KG-map machine · Stack alphabets of the clique reduction machine · Stack alphabet of the SAT verifier

Used byCLIQUE ≤ INDEPENDENT-SET is polynomial-time · INDEPENDENT-SET ≤ VERTEX-COVER is polynomial-time

TheoremCLIQUE ≤ INDEPENDENT-SET is polynomial-time#✓fully proved

The map on bit strings that sends \(1^k 0 1^n 0 b\), for natural numbers \(k\) and \(n\) and a bit string \(b\), to \(1^k 0 1^n 0 \bar b\), where \(\bar b\) is \(b\) with every bit complemented, and sends every string not of this form to the string \(100\), is computable in polynomial time.

theorem isPolyTime_flipKG : IsPolyTime flipKG

Uses 24 · Used by 1

Statement usesComplementing map from CLIQUE to INDEPENDENT-SET instances · 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 · Polynomial-time computable functions

Proof usesComponent machine · Reduction host, canonical form · Stacks of the CLIQUE to VERTEX-COVER reduction machine · Labels of the KG-map machine · Modes of the CLIQUE/VERTEX-COVER reduction machine · Reduction computed in each mode · The KG-map machine · Correctness and running time of the KG-map machine · Start label of the KG-map machine · Stack alphabets of the clique reduction machine · The CLIQUE-to-INDEPENDENT-SET and INDEPENDENT-SET-to-VERTEX-COVER map as a host component · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine · Runs within a step budget

Used byINDEPENDENT-SET is NP-hard

TheoremINDEPENDENT-SET ≤ VERTEX-COVER is polynomial-time#✓fully proved

The map on bit strings that sends \(1^k 0 1^n 0 b\), for natural numbers \(k \le n\) and a bit string \(b\), to \(1^{n-k} 0 1^n 0 b\), and sends every other string (including \(1^k 0 1^n 0 b\) with \(k > n\)) to the string \(100\), is computable in polynomial time.

theorem isPolyTime_isToVc : IsPolyTime isToVc

Uses 24 · Used by 1

Statement usesMap from INDEPENDENT-SET to VERTEX-COVER instances · 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 · Polynomial-time computable functions

Proof usesComponent machine · Reduction host, canonical form · Stacks of the CLIQUE to VERTEX-COVER reduction machine · Labels of the KG-map machine · Modes of the CLIQUE/VERTEX-COVER reduction machine · Reduction computed in each mode · The KG-map machine · Correctness and running time of the KG-map machine · Start label of the KG-map machine · Stack alphabets of the clique reduction machine · The CLIQUE-to-INDEPENDENT-SET and INDEPENDENT-SET-to-VERTEX-COVER map as a host component · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine · Runs within a step budget

Used byVERTEX-COVER (exact size k) is NP-hard

AbbreviationThe CLIQUE emitter#✓fully proved

The emitter given by the CLIQUE emitter machine, run from its start label to its exit label, with token stack \(T\) and output stack \(O\). Its output on a CNF formula \(\varphi\) is Karp's CLIQUE instance of \(\varphi\), its output on undecodable input is the string \(100\), and its step bound on \(m\) tokens is \(8(m + 1)^3\). Let \(\varphi\) be a CNF formula with \(m\) tokens. Started with the tokens of \(\varphi\) on \(T\), last token on top, and all other stacks empty, the machine reaches its exit label within \(8(m + 1)^3\) steps, with Karp's CLIQUE instance of \(\varphi\) on \(O\), first bit on top.

Cslib.Complexity.Karp.emitClique · 21 lines

abbrev emitClique : Emitter where
  K := EmitClique.K
  Γ := EmitClique.Γ
  L := EmitClique.Lab
  prog := EmitClique.prog
  start := EmitClique.start
  done := .done
  start_ne_done := by decide
  prog_done := rfl
  cT := .T
  cO := .O
  cT_ne_cO := by decide
  iT := Equiv.refl _
  eO := Equiv.refl _
  g := toClique
  noOut := noKG
  B n := 8 * (n + 1) ^ 3
  B_mono a b h := by dsimp only; gcongr
  run φ v St hT hO h0 := by
    obtain ⟨v', S', r, h⟩ := EmitClique.run φ [] v St (by simpa using hT) hO h0
    exact ⟨v', S', r, by simpa using h⟩

Uses 13 · Used by 1

Statement usesStacks of the SAT-to-CLIQUE emitter · Labels of the SAT-to-CLIQUE emitter · The CLIQUE emitter machine · The CLIQUE emitter computes Karp's instance in cubic time · Start label of the CLIQUE emitter · Stack alphabets of the CLIQUE emitter · Emitter · Fixed no-instance · Karp's CLIQUE instance of a CNF formula · Stack alphabet of the SAT verifier · Token sequence of a CNF formula · CNF formula · Runs within a step budget

Used bySAT ≤ CLIQUE is polynomial-time

TheoremSAT ≤ CLIQUE is polynomial-time#✓fully proved

Let \(f\) be the map on bit strings that sends the binary code of a CNF formula \(\varphi\) to the encoding of Karp's CLIQUE instance \((k, G)\) of \(\varphi\), and sends every string that is not the code of a CNF formula to the string \(100\). Here \(G\) has one vertex per literal occurrence in \(\varphi\), two occurrences are adjacent when they lie in different clauses and are not complementary, and \(k\) is the number of clauses of \(\varphi\). Then \(f\) is computable in polynomial time.

theorem isPolyTime_reduceClique : IsPolyTime reduceClique

Uses 22 · Used by 1

Statement usesKarp's SAT-to-CLIQUE map on bit strings · 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 · Polynomial-time computable functions

Proof usesStacks of the SAT-to-CLIQUE emitter · Labels of the SAT-to-CLIQUE emitter · Stack alphabets of the CLIQUE emitter · Emitter · Emitter reductions out of SAT are polynomial-time · Output of an emitter on a bit string · The CLIQUE emitter · Fixed no-instance · Karp's CLIQUE instance of a CNF formula · Stack alphabet of the SAT verifier · Decoding a complete length-prefixed CNF formula · CNF formula

Used byCLIQUE is NP-hard

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.