Vertex pairs in encoding order to The vertex pairs are listed without repetition
DefinitionVertex pairs in encoding order#✓fully proved
For a natural number \(n\), the list of all pairs \((i, j)\) of natural numbers with \(i < j < n\), ordered by \(i\) ascending and, for each \(i\), by \(j\) descending from \(n - 1\) to \(i + 1\).
def pairs (n : ℕ) : List (ℕ × ℕ) :=
(List.range n).flatMap fun i => ((List.range n).reverse.filter (i < ·)).map (i, ·)Used by 51
k) is NP-hard · Vertex covers of size \(k\) match subset sums hitting the target · Sublists of the reduction's numbers as vertex and pair sets · Vertex covers in terms of the pair bits · Reduction from VERTEX-COVER to SUBSET-SUM · Numbers of the SUBSET-SUM reduction · Target of the SUBSET-SUM reduction · 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 · A vertex number in base 4 · Touch bits from the pair walk of a vertex · 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 · SUBSET-SUM is NP-hardDefinitionAdjacency bit of a vertex pair#✓fully proved
Let \(n\), \(i\), \(j\) be natural numbers and \(b\) a list of bits. List the pairs \((i', j')\) with \(i' < j' < n\) in encoding order (\(i'\) ascending and, for each \(i'\), \(j'\) descending) and match the \(t\)-th pair with the \(t\)-th bit of \(b\), for as many positions as both lists have. The adjacency bit of \(\{i, j\}\) is the bit matched with \((\min(i, j), \max(i, j))\), and false when that pair has no matched bit (for instance when \(i = j\), when \(\max(i, j) \ge n\), or when \(b\) is too short).
def adjBits (n : ℕ) (bits : List Bool) (i j : ℕ) : Bool :=
(((pairs n).zip bits).lookup (min i j, max i j)).getD falsedef pairs (n : ℕ) : List (ℕ × ℕ) :=
(List.range n).flatMap fun i => ((List.range n).reverse.filter (i < ·)).map (i, ·)CSLibExt/Computability/Complexity/Karp/Clique.lean:50
Uses 1 · Used by 14
DefinitionThe graph encoded by pair bits#✓fully proved
List the pairs \((i, j)\) of natural numbers with \(i < j < n\) by \(i\) ascending and, for each \(i\), by \(j\) descending, and give the \(t\)-th pair the \(t\)-th bit of a list of bits. The simple graph on the vertex set \(\{0, \dots, n - 1\}\) given by the list makes two vertices \(i < j\) adjacent when the bit of \((i, j)\) is true; a pair left without a bit because the list is too short is not an edge, and bits beyond the last pair are ignored.
def toGraph (n : ℕ) (bits : List Bool) : SimpleGraph (Fin n) where
Adj i j := i ≠ j ∧ adjBits n bits i j = true
symm := ⟨fun i j h => ⟨h.1.symm, by rw [adjBits, min_comm, max_comm]; exact h.2⟩⟩
loopless := ⟨fun i h => h.1 rfl⟩def adjBits (n : ℕ) (bits : List Bool) (i j : ℕ) : Bool :=
(((pairs n).zip bits).lookup (min i j, max i j)).getD falseCSLibExt/Computability/Complexity/Karp/Clique.lean:54
Uses 2 · Used by 15
k) is NP-hard · Vertex covers of size \(k\) match subset sums hitting the target · Vertex covers in terms of the pair bits · SUBSET-SUM is NP-hardDefinitionEncoding of a graph instance#✓fully proved
For natural numbers \(k\), \(n\) and a list of bits \(b\), the encoding is \(1^k\,0\,1^n\,0\,b\), writing \(1\) for true and \(0\) for false: \(k\) ones, a zero, \(n\) ones, a zero, and then \(b\). Here \(k\) is the target size and \(b\) lists the pair bits of a graph on \(n\) vertices.
def encodeKG (k n : ℕ) (bits : List Bool) : List Bool :=
List.replicate k true ++ false :: (List.replicate n true ++ false :: bits)Used by 18
k) is NP-hard · SUBSET-SUM is NP-hardDefinitionDecoding a graph instance#✓fully proved
Writing \(1\) for true and \(0\) for false, a bit string of the form \(1^k\,0\,1^n\,0\,b\) with natural numbers \(k\), \(n\) and a list of bits \(b\) decodes to the triple \((k, n, b)\). A bit string with fewer than two zeros does not decode.
def decodeKG (x : List Bool) : Option (ℕ × ℕ × List Bool) := do
let (k, r) ← readUnaryLength x
let (n, bits) ← readUnaryLength r
pure (k, n, bits)def readUnaryLength : List Bool → Option (Nat × List Bool)
| [] => none
| false :: rest => some (0, rest)
| true :: rest => (readUnaryLength rest).map fun result => (result.1 + 1, result.2)CSLibExt/Computability/CookLevin.lean:46
Uses 1 · Used by 12
k) is NP-hard · Reduction from VERTEX-COVER to SUBSET-SUM · SUBSET-SUM is NP-hardDefinitionFixed no-instance#✓fully proved
The bit string \(1\,0\,0\) (writing \(1\) for true and \(0\) for false), which encodes \(k = 1\) together with the graph with no vertices (\(n = 0\) and no pair bits).
A graph with no vertices has no clique, independent set or vertex cover of exactly one vertex, so this string lies in none of CLIQUE, INDEPENDENT-SET and VERTEX-COVER.
def noKG : List Bool := encodeKG 1 0 []def encodeKG (k n : ℕ) (bits : List Bool) : List Bool :=
List.replicate k true ++ false :: (List.replicate n true ++ false :: bits)CSLibExt/Computability/Complexity/Karp/Clique.lean:64
Uses 1 · Used by 10
k) is NP-hardDefinitionLanguage of graph instances with a property#✓fully proved
Let \(P\) be a property of a natural number \(n\), a natural number \(k\) and a simple graph on \(\{0, \dots, n-1\}\). The decision problem accepts a bit string \(x\) exactly when, writing \(1\) for true and \(0\) for false, \(x = 1^k\,0\,1^n\,0\,b\) for some natural numbers \(k\), \(n\) and a list of bits \(b\) with one entry for each pair \(i < j < n\), such that \(P\) holds of \(n\), \(k\) and the graph on \(\{0, \dots, n-1\}\) given by \(b\). In that graph, distinct \(i\) and \(j\) are adjacent when the bit of the pair \(\{i, j\}\) is true, the pairs being listed with \(i\) ascending and, for each \(i\), \(j\) descending.
noncomputable def kgDec (P : ∀ n : ℕ, ℕ → SimpleGraph (Fin n) → Prop) :
MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
decide (∃ k n bits, encodeKG k n bits = x ∧ bits.length = (pairs n).length ∧
P n k (toGraph n bits))abbrev DecisionProblem := List Bool → BoolMathlibExt/Computability/Complexity.lean:170
def encodeKG (k n : ℕ) (bits : List Bool) : List Bool :=
List.replicate k true ++ false :: (List.replicate n true ++ false :: bits)CSLibExt/Computability/Complexity/Karp/Clique.lean:64
def pairs (n : ℕ) : List (ℕ × ℕ) :=
(List.range n).flatMap fun i => ((List.range n).reverse.filter (i < ·)).map (i, ·)CSLibExt/Computability/Complexity/Karp/Clique.lean:50
def toGraph (n : ℕ) (bits : List Bool) : SimpleGraph (Fin n) where
Adj i j := i ≠ j ∧ adjBits n bits i j = true
symm := ⟨fun i j h => ⟨h.1.symm, by rw [adjBits, min_comm, max_comm]; exact h.2⟩⟩
loopless := ⟨fun i h => h.1 rfl⟩CSLibExt/Computability/Complexity/Karp/Clique.lean:58
Uses 4 · Used by 9
k) is NP-hard · SUBSET-SUM is NP-hardDefinitionCLIQUE#✓fully proved
The decision problem CLIQUE accepts a bit string \(x\) exactly when, writing \(1\) for true and \(0\) for false, \(x = 1^k\,0\,1^n\,0\,b\) for some natural numbers \(k\), \(n\) and a list of bits \(b\) with one entry for each pair \(i < j < n\), such that the graph on \(\{0, \dots, n-1\}\) given by \(b\) has a clique of exactly \(k\) vertices. In that graph, distinct \(i\) and \(j\) are adjacent when the bit of the pair \(\{i, j\}\) is true, the pairs being listed with \(i\) ascending and, for each \(i\), \(j\) descending.
noncomputable def cliqueDec : MetaMathlibExt.ComplexityTheory.DecisionProblem :=
kgDec fun _ k G => ∃ s, G.IsNClique k sabbrev DecisionProblem := List Bool → BoolMathlibExt/Computability/Complexity.lean:170
noncomputable def kgDec (P : ∀ n : ℕ, ℕ → SimpleGraph (Fin n) → Prop) :
MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
decide (∃ k n bits, encodeKG k n bits = x ∧ bits.length = (pairs n).length ∧
P n k (toGraph n bits))CSLibExt/Computability/Complexity/Karp/Clique.lean:78
Uses 2 · Used by 6
DefinitionINDEPENDENT-SET#✓fully proved
The decision problem INDEPENDENT-SET accepts a bit string \(x\) exactly when, writing \(1\) for true and \(0\) for false, \(x = 1^k\,0\,1^n\,0\,b\) for some natural numbers \(k\), \(n\) and a list of bits \(b\) with one entry for each pair \(i < j < n\), such that the graph on \(\{0, \dots, n-1\}\) given by \(b\) has an independent set of exactly \(k\) vertices. In that graph, distinct \(i\) and \(j\) are adjacent when the bit of the pair \(\{i, j\}\) is true, the pairs being listed with \(i\) ascending and, for each \(i\), \(j\) descending.
noncomputable def indSetDec : MetaMathlibExt.ComplexityTheory.DecisionProblem :=
kgDec fun _ k G => ∃ s, G.IsNIndepSet k sabbrev DecisionProblem := List Bool → BoolMathlibExt/Computability/Complexity.lean:170
noncomputable def kgDec (P : ∀ n : ℕ, ℕ → SimpleGraph (Fin n) → Prop) :
MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
decide (∃ k n bits, encodeKG k n bits = x ∧ bits.length = (pairs n).length ∧
P n k (toGraph n bits))CSLibExt/Computability/Complexity/Karp/Clique.lean:78
Uses 2 · Used by 6
DefinitionThe VERTEX-COVER problem#✓fully proved
The decision problem that accepts a bit string exactly when it encodes an instance \((k, G)\), where \(G\) is a simple graph on \(n\) vertices, and \(G\) has a vertex cover of exactly \(k\) vertices. The encoding is \(k\) ones, a zero, \(n\) ones, a zero, then one bit for each pair \((i, j)\) with \(i < j < n\), listed by \(i\) ascending and, for each \(i\), by \(j\) descending, a true bit meaning that \(i\) and \(j\) are adjacent; a string with any other number of pair bits is rejected.
This is Sipser's \(k\)-node vertex cover; for \(k \le n\) it is the same as a cover of at most \(k\) vertices.
noncomputable def vertexCoverDec : MetaMathlibExt.ComplexityTheory.DecisionProblem :=
kgDec fun n k G => ∃ s : Finset (Fin n), s.card = k ∧ G.IsVertexCover (s : Set (Fin n))abbrev DecisionProblem := List Bool → BoolMathlibExt/Computability/Complexity.lean:170
noncomputable def kgDec (P : ∀ n : ℕ, ℕ → SimpleGraph (Fin n) → Prop) :
MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
decide (∃ k n bits, encodeKG k n bits = x ∧ bits.length = (pairs n).length ∧
P n k (toGraph n bits))CSLibExt/Computability/Complexity/Karp/Clique.lean:78
Uses 2 · Used by 5
DefinitionLiteral occurrences of a CNF formula#✓fully proved
For a CNF formula \(\varphi\) with clauses \(C_0, \dots, C_{m-1}\), the list of triples \((i, x, b)\), one for each literal \((x, b)\) of each clause \(C_i\), where \(x\) is the variable index and \(b\) the polarity. The triples are listed clause by clause in order of \(i\), and within a clause in the order of its literals.
def occs (φ : CNF) : List (ℕ × ℕ × Bool) :=
φ.zipIdx.flatMap fun p => p.1.map fun l => (p.2, l.1, l.2)abbrev CNF := List CNFClauseCSLibExt/Logics/Propositional/CNF/Basic.lean:33
Uses 2 · Used by 10
DefinitionAdjacency of literal occurrences in Karp's clique graph#✓fully proved
A literal occurrence is a triple \((c, x, b)\) of a clause index \(c\), a variable index \(x\) and a polarity \(b\). Two occurrences \((c, x, b)\) and \((c', x', b')\) are adjacent when \(c \ne c'\) and they are not complementary, that is, it is not the case that \(x = x'\) and \(b \ne b'\).
Used by 9
DefinitionAdjacency bits of Karp's clique graph#✓fully proved
For a CNF formula \(\varphi\), list its literal occurrences \(o_0, \dots, o_{m-1}\) in formula order, each recorded by its clause index, its variable and its polarity. The result has one bit for each pair \((i, j)\) with \(i < j < m\), the pairs taken in encoding order (\(i\) ascending and, for each \(i\), \(j\) descending). The bit of \((i, j)\) is true exactly when \(o_i\) and \(o_j\) lie in different clauses and are not complementary, that is, are not occurrences of the same variable with opposite polarities.
def cliqueBits (φ : CNF) : List Bool :=
(pairs (occs φ).length).map fun p => occAdj ((occs φ).getD p.1 (0, 0, false))
((occs φ).getD p.2 (0, 0, false))abbrev CNF := List CNFClauseCSLibExt/Logics/Propositional/CNF/Basic.lean:33
def pairs (n : ℕ) : List (ℕ × ℕ) :=
(List.range n).flatMap fun i => ((List.range n).reverse.filter (i < ·)).map (i, ·)CSLibExt/Computability/Complexity/Karp/Clique.lean:50
def occs (φ : CNF) : List (ℕ × ℕ × Bool) :=
φ.zipIdx.flatMap fun p => p.1.map fun l => (p.2, l.1, l.2)CSLibExt/Computability/Complexity/Karp/Clique.lean:97
def occAdj (o o' : ℕ × ℕ × Bool) : Bool :=
o.1 != o'.1 && !(o.2.1 == o'.2.1 && o.2.2 != o'.2.2)CSLibExt/Computability/Complexity/Karp/Clique.lean:101
Uses 4 · Used by 6
DefinitionKarp's CLIQUE instance of a CNF formula#✓fully proved
For a CNF formula \(\varphi\) with \(m\) clauses and \(N\) literal occurrences, the bit string encoding the instance \((m, G)\): \(m\) ones, a zero, \(N\) ones, a zero, then one adjacency bit for each pair \((i, j)\) with \(i < j < N\), listed by \(i\) ascending and, for each \(i\), by \(j\) descending, a true bit meaning that \(i\) and \(j\) are adjacent. The graph \(G\) has the literal occurrences of \(\varphi\), in order, as its vertices \(0, \dots, N - 1\), and two occurrences are adjacent when they lie in different clauses and are not complementary (the same variable with opposite polarities).
def toClique (φ : CNF) : List Bool := encodeKG φ.length (occs φ).length (cliqueBits φ)abbrev CNF := List CNFClauseCSLibExt/Logics/Propositional/CNF/Basic.lean:33
def encodeKG (k n : ℕ) (bits : List Bool) : List Bool :=
List.replicate k true ++ false :: (List.replicate n true ++ false :: bits)CSLibExt/Computability/Complexity/Karp/Clique.lean:64
def occs (φ : CNF) : List (ℕ × ℕ × Bool) :=
φ.zipIdx.flatMap fun p => p.1.map fun l => (p.2, l.1, l.2)CSLibExt/Computability/Complexity/Karp/Clique.lean:97
def cliqueBits (φ : CNF) : List Bool :=
(pairs (occs φ).length).map fun p => occAdj ((occs φ).getD p.1 (0, 0, false))
((occs φ).getD p.2 (0, 0, false))CSLibExt/Computability/Complexity/Karp/Clique.lean:105
Uses 5 · Used by 5
DefinitionKarp's SAT-to-CLIQUE map on bit strings#✓fully proved
The map on bit strings that decodes its input as a CNF formula \(\varphi\) (rejecting missing or trailing bits) and returns Karp's CLIQUE instance of \(\varphi\); an input that does not decode is sent to the fixed no-instance \(k = 1\) on the graph with no vertices.
def reduceClique (x : List Bool) : List Bool :=
match decodeCNF x with
| some φ => toClique φ
| none => noKGdef decodeCNF (input : List Bool) : Option CNF := do
let (φ, rest) ← decodeCNFAux input
if rest.isEmpty then some φ else noneCSLibExt/Computability/CookLevin.lean:108
def toClique (φ : CNF) : List Bool := encodeKG φ.length (occs φ).length (cliqueBits φ)CSLibExt/Computability/Complexity/Karp/Clique.lean:110
def noKG : List Bool := encodeKG 1 0 []CSLibExt/Computability/Complexity/Karp/Clique.lean:74
Uses 4 · Used by 2
DefinitionComplementing map from CLIQUE to INDEPENDENT-SET instances#✓fully proved
Writing \(1\) for true and \(0\) for false, the map sends a bit string \(1^k\,0\,1^n\,0\,b\) to \(1^k\,0\,1^n\,0\,\bar b\), where \(\bar b\) is \(b\) with every bit complemented. A bit string with fewer than two zeros goes to the fixed no-instance \(1\,0\,0\).
def flipKG (x : List Bool) : List Bool :=
match decodeKG x with
| some (k, n, bits) => encodeKG k n (bits.map not)
| none => noKGdef decodeKG (x : List Bool) : Option (ℕ × ℕ × List Bool) := do
let (k, r) ← readUnaryLength x
let (n, bits) ← readUnaryLength r
pure (k, n, bits)CSLibExt/Computability/Complexity/Karp/Clique.lean:68
def encodeKG (k n : ℕ) (bits : List Bool) : List Bool :=
List.replicate k true ++ false :: (List.replicate n true ++ false :: bits)CSLibExt/Computability/Complexity/Karp/Clique.lean:64
def noKG : List Bool := encodeKG 1 0 []CSLibExt/Computability/Complexity/Karp/Clique.lean:74
DefinitionMap from INDEPENDENT-SET to VERTEX-COVER instances#✓fully proved
Writing \(1\) for true and \(0\) for false, the map sends a bit string \(1^k\,0\,1^n\,0\,b\) with \(k \le n\) to \(1^{n-k}\,0\,1^n\,0\,b\). Every other bit string, namely one of this form with \(k > n\) or one with fewer than two zeros, goes to the fixed no-instance \(1\,0\,0\).
def isToVc (x : List Bool) : List Bool :=
match decodeKG x with
| some (k, n, bits) => if k ≤ n then encodeKG (n - k) n bits else noKG
| none => noKGdef decodeKG (x : List Bool) : Option (ℕ × ℕ × List Bool) := do
let (k, r) ← readUnaryLength x
let (n, bits) ← readUnaryLength r
pure (k, n, bits)CSLibExt/Computability/Complexity/Karp/Clique.lean:68
def encodeKG (k n : ℕ) (bits : List Bool) : List Bool :=
List.replicate k true ++ false :: (List.replicate n true ++ false :: bits)CSLibExt/Computability/Complexity/Karp/Clique.lean:64
def noKG : List Bool := encodeKG 1 0 []CSLibExt/Computability/Complexity/Karp/Clique.lean:74
Uses 3 · Used by 3
TheoremUnparsable input is rejected#✓fully proved
Let \(P\) be any property of a triple \((n, k, G)\), where \(n\) and \(k\) are natural numbers and \(G\) is a simple graph on the vertices \(0, 1, \dots, n - 1\). A bit string that does not begin with two unary numbers (each a run of \(1\)s ended by a \(0\)) is rejected by the language of valid instances \((k, G)\) satisfying \(P\).
theorem kgDec_of_decodeKG_eq_none {P : ∀ n : ℕ, ℕ → SimpleGraph (Fin n) → Prop}
{x : List Bool} (h : decodeKG x = none) : kgDec P x = falsedef decodeKG (x : List Bool) : Option (ℕ × ℕ × List Bool) := do
let (k, r) ← readUnaryLength x
let (n, bits) ← readUnaryLength r
pure (k, n, bits)CSLibExt/Computability/Complexity/Karp/Clique.lean:68
noncomputable def kgDec (P : ∀ n : ℕ, ℕ → SimpleGraph (Fin n) → Prop) :
MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
decide (∃ k n bits, encodeKG k n bits = x ∧ bits.length = (pairs n).length ∧
P n k (toGraph n bits))CSLibExt/Computability/Complexity/Karp/Clique.lean:78
Uses 6 · Used by 3
TheoremMembership in the vertex pairs#✓fully proved
For natural numbers \(n\), \(i\) and \(j\), the pair \((i, j)\) belongs to the list of vertex pairs in encoding order for \(n\) if and only if \(i < j\) and \(j < n\).
@[simp] theorem mem_pairs {n i j : ℕ} : (i, j) ∈ pairs n ↔ i < j ∧ j < ndef pairs (n : ℕ) : List (ℕ × ℕ) :=
(List.range n).flatMap fun i => ((List.range n).reverse.filter (i < ·)).map (i, ·)CSLibExt/Computability/Complexity/Karp/Clique.lean:50
Uses 1 · Used by 7
TheoremThe vertex pairs are listed without repetition#✓fully proved
For every natural number \(n\), the list of pairs \((i, j)\) of natural numbers with \(i < j < n\), in encoding order (\(i\) ascending and, for each \(i\), \(j\) descending from \(n - 1\) to \(i + 1\)), contains no pair twice.
theorem pairs_nodup (n : ℕ) : (pairs n).Nodupdef pairs (n : ℕ) : List (ℕ × ℕ) :=
(List.range n).flatMap fun i => ((List.range n).reverse.filter (i < ·)).map (i, ·)CSLibExt/Computability/Complexity/Karp/Clique.lean:50
Uses 1 · Used by 3
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.