Paper
Graph crawling is NP-complete
32 pages · 5 marked passages · pdflatex · download PDF · lax-117614
-
Website graphs
A website graph is a finite structure with a binary relation, the hyperlinks between pages, and three unary relations: the root pages, the target pages, and a marked set of pages whose cardinality is the crawling budget, in unary representation. This is the website of Gauquier, Manolescu and Senellart (EDBT 2026) at unit page costs, the budget being then a number of pages.
1 import Mathlib.ModelTheory.Semantics 2 import Mathlib.ModelTheory.Syntax 3 import Mathlib.Data.Fintype.Lattice 4 … module docstring, 12 lines 17 18 namespace Lax117614.WebsiteGraphs 19 20 open FirstOrder 21 22 open FirstOrder.Language Structure 23 24 /-- The relation symbols of the language. -/ 25 inductive siteGraphRel : ℕ → Type where 26 /-- `edge a b`: a hyperlink from page `a` to page `b`. -/ 27 | edge : siteGraphRel 2 28 /-- `root a`: the page `a` is the crawl's starting point. -/ 29 | root : siteGraphRel 1 30 /-- `target a`: the page `a` must be crawled. -/ 31 | target : siteGraphRel 1 32 /-- `marked a`: the page `a` belongs to the marked set carrying the 33 budget. -/ 34 | marked : siteGraphRel 1 35 deriving DecidableEq 36 37 /-- The relational language of website graphs: directed links, a root, a set 38 of target pages, and a marked set whose cardinality is the crawling budget. -/ 39 def siteGraph : FirstOrder.Language := 40 ⟨fun _ => Empty, siteGraphRel⟩ 41 42 instance instIsRelationalSiteGraph : FirstOrder.Language.IsRelational siteGraph := fun _ => 43 (inferInstance : IsEmpty Empty) 44 45 /-- `edge a b`: a hyperlink from page `a` to page `b`. -/ 46 abbrev wsEdge : siteGraph.Relations 2 := 47 .edge 48 49 /-- `root a`: the page `a` is the crawl's starting point. -/ 50 abbrev wsRoot : siteGraph.Relations 1 := 51 .root 52 53 /-- `target a`: the page `a` must be crawled. -/ 54 abbrev wsTarget : siteGraph.Relations 1 := 55 .target 56 57 /-- `marked a`: the page `a` belongs to the marked set carrying the 58 budget. -/ 59 abbrev wsMarked : siteGraph.Relations 1 := 60 .marked 61 62 section Shorthands 63 64 variable {A : Type} [siteGraph.Structure A] 65 66 /-- A hyperlink in a website graph. -/ 67 def WSEdge (a b : A) : Prop := RelMap wsEdge ![a, b] 68 69 /-- Being the root of a website graph. -/ 70 def WSRoot (a : A) : Prop := RelMap wsRoot ![a] 71 72 /-- Being a target page. -/ 73 def WSTarget (a : A) : Prop := RelMap wsTarget ![a] 74 75 /-- Belonging to the marked set carrying the budget. -/ 76 def WSMarked (a : A) : Prop := RelMap wsMarked ![a] 77 78 end Shorthands 79 80 end Lax117614.WebsiteGraphs 81 -
The graph crawling problem
A crawl of a website graph is a set of pages containing a root page and every target page, each of its pages reachable from the root by hyperlinks inside the set; this is the node set of a rooted subtree, the crawl of Gauquier, Manolescu and Senellart (EDBT 2026). A website graph has a cheap crawl when it is finite and some crawl has at most as many pages as the marked set has elements, the budget. The graph crawling problem is the decision problem on website graphs whose yes-instances are the website graphs isomorphic to one with a cheap crawl.
1 import Mathlib.SetTheory.Cardinal.Finite 2 import Mathlib.ModelTheory.Semantics 3 import Mathlib.Data.Set.Card 4 import Mathlib.Data.Set.Finite.Lemmas 5 import Lax904597.Classes 6 import Lax799700.Problems 7 import Lax117614.WebsiteGraphs 8 … module docstring, 14 lines 23 24 namespace Lax117614.GraphCrawlingProblem 25 26 open FirstOrder 27 28 open FirstOrder.Language Structure 29 30 open Lax904597.Problems Lax904597.Classes Lax799700.Problems Lax117614.WebsiteGraphs 31 32 section Reachability 33 34 variable {A : Type} 35 36 /-- The directed step available inside a chosen set: an edge whose two 37 endpoints are both chosen. -/ 38 def DiLink (Adjp : A → A → Prop) (S : A → Prop) (a b : A) : Prop := 39 S a ∧ S b ∧ Adjp a b 40 41 /-- Every member of `S` is reachable from `r` by directed steps inside `S` – 42 the shape of an `r`-rooted subtree with node set `S`, reachability being all a 43 breadth-first traversal needs to assemble the tree. -/ 44 def ReachesAllOn (Adjp : A → A → Prop) (r : A) (S : A → Prop) : Prop := 45 ∀ x, S x → Relation.ReflTransGen (DiLink Adjp S) r x 46 47 end Reachability 48 49 section Generic 50 51 variable {A : Type} 52 53 /-- Some marked root admits a crawl: a set of pages containing the root and 54 every target, entirely reachable from the root inside itself, of size (the 55 paper's total cost, at unit page costs) at most the number encoded by the 56 marked set. -/ 57 def CrawlOn (Adjp : A → A → Prop) (Rp Tp Kp : A → Prop) : Prop := 58 ∃ r, Rp r ∧ ∃ S : A → Prop, S r ∧ (∀ x, Tp x → S x) ∧ ReachesAllOn Adjp r S ∧ 59 {x | S x}.ncard ≤ {x | Kp x}.ncard 60 61 end Generic 62 63 section Problem 64 65 variable (A : Type) [siteGraph.Structure A] 66 67 /-- A website graph admits a crawl within budget: a set of pages containing 68 the marked root and every target, reachable from the root inside itself, with 69 at most as many pages as the marked set has elements. (Finiteness of the 70 universe is part of the property: cardinality thresholds are only meaningful 71 on finite structures.) -/ 72 def HasCheapCrawl : Prop := 73 Finite A ∧ CrawlOn (WSEdge (A := A)) WSRoot WSTarget WSMarked 74 75 end Problem 76 77 /-- GRAPH CRAWLING, decision variant at unit page costs: does the website 78 graph satisfy `HasCheapCrawl`? -/ 79 def GraphCrawling : DecisionProblem siteGraph := 80 DecisionProblem.ofPred HasCheapCrawl 81 82 end Lax117614.GraphCrawlingProblem 83 -
Graph crawling is NP-complete
The graph crawling problem is NP-complete, in the sense of the NP core: it is definable in existential second-order logic, and every problem of NP reduces to it by an ordered first-order reduction. This is Proposition 4 of Gauquier, Manolescu and Senellart (EDBT 2026) at unit page costs, hardness coming from Set Cover by the paper's reduction.
1 import Lax904597.Classes 2 import Lax799700.Problems 3 import Lax117614.WebsiteGraphs 4 import Lax117614.GraphCrawlingProblem 5 … module docstring, 11 lines 17 18 namespace Lax117614.GraphCrawlingNPComplete 19 20 open Lax904597.Classes Lax117614.GraphCrawlingProblem 21 22 /-- GraphCrawling is NP-complete (Proposition 4 of the paper). -/ 23 axiom graphCrawling_NP_complete : NP.Complete GraphCrawling 24 25 end Lax117614.GraphCrawlingNPComplete 26 -
Membership from the library's existential second-order definition of graph crawling; hardness from the library's ordered first-order reduction out of Set Cover, which is NP-hard by the catalog's statement for it. Both are transported to the concept's problem along the agreements.
-
Set Cover, Hitting Set, Set Packing, Exact Cover and Set Splitting
Five problems on set systems: a universe carrying two unary marks that separate the ground elements from the sets of a family, a binary incidence relation between them, and a third unary mark whose cardinality is the threshold , in unary representation. SetCover asks for at most sets covering every element, HittingSet for at most elements meeting every set, SetPacking for at least pairwise disjoint sets, ExactCover for a subfamily covering every element exactly once, and SetSplitting for a two-coloring of the elements leaving no set monochromatic. Nothing forces an element of the universe to be an element or a set, and disjointness in a packing is required of the ground elements only; both conventions are what let a first-order interpretation build a set system inside a tagged power of its input.
All five are in NP by existential second-order definitions except Hitting Set, which reduces to Set Cover by reading incidence backwards, the same interpretation reducing Set Cover to Hitting Set. Hardness comes by first-order reductions: Set Cover from Vertex Cover, Set Packing from Independent Set, Exact Cover from 1-in-SAT, Set Splitting from NAE-SAT.
- thm✓
Lax799700.SetFamily(1st statement) - thm✓
Lax799700.SetFamily(2nd statement) - thm✓
Lax799700.SetFamily(3rd statement) - thm✓
Lax799700.SetFamily(4th statement) - thm✓
Lax799700.SetFamily(5th statement) - thm✓
Lax799700.SetFamily(6th statement) - thm✓
Lax799700.SetFamily(7th statement) - thm✓
Lax799700.SetFamily(8th statement) - thm✓
Lax799700.SetFamily(9th statement) - thm✓
Lax799700.SetFamily(10th statement) - thm✓
Lax799700.SetFamily(11th statement) - thm✓
Lax799700.SetFamily(12th statement) - thm✓
Lax799700.SetFamily(13th statement) - thm✓
Lax799700.SetFamily(14th statement) - thm✓
Lax799700.SetFamily(15th statement)
1 import Mathlib.Data.Fintype.EquivFin 2 import Mathlib.Data.Set.Card 3 import Mathlib.SetTheory.Cardinal.Finite 4 import Mathlib.Logic.Equiv.Prod 5 import Mathlib.ModelTheory.Semantics 6 import Mathlib.ModelTheory.Complexity 7 import Mathlib.Tactic.FinCases 8 import Mathlib.ModelTheory.Syntax 9 import Lax904597.Classes 10 import Lax799700.Problems 11 … module docstring, 25 lines 37 38 namespace Lax799700.SetFamily 39 40 open FirstOrder 41 42 open FirstOrder.Language 43 44 /-- The relation symbols of the language. -/ 45 inductive setSystemRel : ℕ → Type where 46 /-- `elem a`: the element `a` belongs to the ground set. -/ 47 | elem : setSystemRel 1 48 /-- `fam a`: the element `a` is one of the sets of the family. -/ 49 | fam : setSystemRel 1 50 /-- `mem a b`: the ground element `a` belongs to the set `b`. -/ 51 | mem : setSystemRel 2 52 /-- `marked a`: the element `a` belongs to the marked set. -/ 53 | marked : setSystemRel 1 54 deriving DecidableEq 55 56 /-- The relational language of set systems: a bipartite incidence structure 57 between ground elements and sets of a family, together with a marked subset of 58 the universe whose cardinality serves as threshold. -/ 59 def setSystem : FirstOrder.Language := 60 ⟨fun _ => Empty, setSystemRel⟩ 61 62 instance instIsRelationalSetSystem : FirstOrder.Language.IsRelational setSystem := fun _ => 63 (inferInstance : IsEmpty Empty) 64 65 /-- `elem a`: the element `a` belongs to the ground set. -/ 66 abbrev ssElem : setSystem.Relations 1 := 67 .elem 68 69 /-- `fam a`: the element `a` is one of the sets of the family. -/ 70 abbrev ssFam : setSystem.Relations 1 := 71 .fam 72 73 /-- `mem a b`: the ground element `a` belongs to the set `b`. -/ 74 abbrev ssMem : setSystem.Relations 2 := 75 .mem 76 77 /-- `marked a`: the element `a` belongs to the marked set. -/ 78 abbrev ssMarked : setSystem.Relations 1 := 79 .marked 80 81 open FirstOrder 82 83 open Language Structure 84 85 section Generic 86 87 variable {A : Type} 88 89 /-- Some subfamily of the `Fp`-sets covers every `Ep`-element and is at most 90 as large as the number encoded by the `Kp`-marked elements: “some cover is at 91 most as large as the marked set”. -/ 92 def CoversOn (Ep Fp : A → Prop) (Mp : A → A → Prop) (Kp : A → Prop) : Prop := 93 ∃ G : A → Prop, (∀ s, G s → Fp s) ∧ (∀ x, Ep x → ∃ s, G s ∧ Mp x s) ∧ 94 {s | G s}.ncard ≤ {x | Kp x}.ncard 95 96 /-- Some set of `Ep`-elements meets every `Fp`-set and is at most as large as 97 the number encoded by the `Kp`-marked elements: “some hitting set is at most 98 as large as the marked set”. This is `DescriptiveComplexity.CoversOn` with the roles 99 of elements and sets exchanged and the incidence relation transposed. -/ 100 def HitsOn (Ep Fp : A → Prop) (Mp : A → A → Prop) (Kp : A → Prop) : Prop := 101 CoversOn Fp Ep (fun s x => Mp x s) Kp 102 103 /-- Some subfamily of the `Fp`-sets is pairwise disjoint – no `Ep`-element 104 belongs to two distinct members – and is at least as large as the number 105 encoded by the `Kp`-marked elements: “some packing is at least as large as the 106 marked set”. -/ 107 def PacksOn (Ep Fp : A → Prop) (Mp : A → A → Prop) (Kp : A → Prop) : Prop := 108 ∃ G : A → Prop, (∀ s, G s → Fp s) ∧ 109 (∀ s s', G s → G s' → s ≠ s' → ∀ x, Ep x → ¬(Mp x s ∧ Mp x s')) ∧ 110 {x | Kp x}.ncard ≤ {s | G s}.ncard 111 112 /-- Some subfamily of the `Fp`-sets covers every `Ep`-element *exactly once*: 113 it covers, and no element belongs to two distinct members. Unlike the three 114 properties above this one carries no threshold – exactness is the whole 115 constraint. -/ 116 def ExactlyCoversOn (Ep Fp : A → Prop) (Mp : A → A → Prop) : Prop := 117 ∃ G : A → Prop, (∀ s, G s → Fp s) ∧ (∀ x, Ep x → ∃ s, G s ∧ Mp x s) ∧ 118 ∀ s s', G s → G s' → s ≠ s' → ∀ x, Ep x → ¬(Mp x s ∧ Mp x s') 119 120 /-- Some two-coloring of the ground elements *splits* every set of the 121 family: no set is monochromatic. Like `DescriptiveComplexity.ExactlyCoversOn` this 122 property carries no threshold. -/ 123 def SplitsOn (Ep Fp : A → Prop) (Mp : A → A → Prop) : Prop := 124 ∃ S : A → Prop, ∀ f, Fp f → 125 (∃ x, Ep x ∧ Mp x f ∧ S x) ∧ ∃ x, Ep x ∧ Mp x f ∧ ¬S x 126 127 end Generic 128 129 section Problems 130 131 section Shorthands 132 133 variable {A : Type} [setSystem.Structure A] 134 135 /-- `elem a`: the element `a` belongs to the ground set. -/ 136 def SSElem {A : Type} [setSystem.Structure A] (a0 : A) : Prop := 137 FirstOrder.Language.Structure.RelMap ssElem ![a0] 138 139 /-- `fam a`: the element `a` is one of the sets of the family. -/ 140 def SSFam {A : Type} [setSystem.Structure A] (a0 : A) : Prop := 141 FirstOrder.Language.Structure.RelMap ssFam ![a0] 142 143 /-- `mem a b`: the ground element `a` belongs to the set `b`. -/ 144 def SSMem {A : Type} [setSystem.Structure A] (a0 : A) (a1 : A) : Prop := 145 FirstOrder.Language.Structure.RelMap ssMem ![a0, a1] 146 147 /-- `marked a`: the element `a` belongs to the marked set. -/ 148 def SSMarked {A : Type} [setSystem.Structure A] (a0 : A) : Prop := 149 FirstOrder.Language.Structure.RelMap ssMarked ![a0] 150 151 end Shorthands 152 153 variable (A : Type) [setSystem.Structure A] 154 155 /-- A set system admits a cover at most as large as its marked set. 156 (Finiteness of the universe is part of the property: cardinality thresholds 157 are only meaningful on finite structures.) -/ 158 def HasSmallSetCover : Prop := 159 Finite A ∧ CoversOn (SSElem (A := A)) SSFam SSMem SSMarked 160 161 /-- A set system admits a hitting set at most as large as its marked set. -/ 162 def HasSmallHittingSet : Prop := 163 Finite A ∧ HitsOn (SSElem (A := A)) SSFam SSMem SSMarked 164 165 /-- A set system admits a packing at least as large as its marked set. -/ 166 def HasLargeSetPacking : Prop := 167 Finite A ∧ PacksOn (SSElem (A := A)) SSFam SSMem SSMarked 168 169 /-- A set system admits an exact cover: a subfamily covering every ground 170 element exactly once. There is no threshold here, so no finiteness 171 assumption either. -/ 172 def HasExactCover : Prop := 173 ExactlyCoversOn (SSElem (A := A)) SSFam SSMem 174 175 /-- A set system admits a splitting two-coloring: no set of the family is 176 monochromatic. -/ 177 def HasSetSplitting : Prop := 178 SplitsOn (SSElem (A := A)) SSFam SSMem 179 180 end Problems 181 182 open Lax904597.Problems Lax904597.Classes Lax799700.Problems 183 184 /-- The property `HasSmallSetCover` is isomorphism-invariant. -/ 185 axiom hasSmallSetCover_iso : ∀ {A B : Type} [Lax799700.SetFamily.setSystem.Structure A] [Lax799700.SetFamily.setSystem.Structure B], 186 (A ≃[Lax799700.SetFamily.setSystem] B) → (HasSmallSetCover A ↔ HasSmallSetCover B) 187 188 /-- The problem SetCover: does the structure satisfy `HasSmallSetCover`? -/ 189 def SetCover : DecisionProblem Lax799700.SetFamily.setSystem := 190 DecisionProblem.ofPred HasSmallSetCover 191 192 /-- The yes-instances of SetCover are exactly the structures satisfying 193 `HasSmallSetCover`. -/ 194 axiom setCover_iff : ∀ (A : Type) [Lax799700.SetFamily.setSystem.Structure A], SetCover A ↔ HasSmallSetCover A 195 196 /-- SetCover is NP-complete. -/ 197 axiom setCover_NP_complete : NP.Complete SetCover 198 199 /-- The property `HasExactCover` is isomorphism-invariant. -/ 200 axiom hasExactCover_iso : ∀ {A B : Type} [Lax799700.SetFamily.setSystem.Structure A] [Lax799700.SetFamily.setSystem.Structure B], 201 (A ≃[Lax799700.SetFamily.setSystem] B) → (HasExactCover A ↔ HasExactCover B) 202 203 /-- The problem ExactCover: does the structure satisfy `HasExactCover`? -/ 204 def ExactCover : DecisionProblem Lax799700.SetFamily.setSystem := 205 DecisionProblem.ofPred HasExactCover 206 207 /-- The yes-instances of ExactCover are exactly the structures satisfying 208 `HasExactCover`. -/ 209 axiom exactCover_iff : ∀ (A : Type) [Lax799700.SetFamily.setSystem.Structure A], ExactCover A ↔ HasExactCover A 210 211 /-- ExactCover is NP-complete. -/ 212 axiom exactCover_NP_complete : NP.Complete ExactCover 213 214 /-- The property `HasSmallHittingSet` is isomorphism-invariant. -/ 215 axiom hasSmallHittingSet_iso : ∀ {A B : Type} [Lax799700.SetFamily.setSystem.Structure A] [Lax799700.SetFamily.setSystem.Structure B], 216 (A ≃[Lax799700.SetFamily.setSystem] B) → (HasSmallHittingSet A ↔ HasSmallHittingSet B) 217 218 /-- The problem HittingSet: does the structure satisfy `HasSmallHittingSet`? -/ 219 def HittingSet : DecisionProblem Lax799700.SetFamily.setSystem := 220 DecisionProblem.ofPred HasSmallHittingSet 221 222 /-- The yes-instances of HittingSet are exactly the structures satisfying 223 `HasSmallHittingSet`. -/ 224 axiom hittingSet_iff : ∀ (A : Type) [Lax799700.SetFamily.setSystem.Structure A], HittingSet A ↔ HasSmallHittingSet A 225 226 /-- HittingSet is NP-complete. -/ 227 axiom hittingSet_NP_complete : NP.Complete HittingSet 228 229 /-- The property `HasLargeSetPacking` is isomorphism-invariant. -/ 230 axiom hasLargeSetPacking_iso : ∀ {A B : Type} [Lax799700.SetFamily.setSystem.Structure A] [Lax799700.SetFamily.setSystem.Structure B], 231 (A ≃[Lax799700.SetFamily.setSystem] B) → (HasLargeSetPacking A ↔ HasLargeSetPacking B) 232 233 /-- The problem SetPacking: does the structure satisfy `HasLargeSetPacking`? -/ 234 def SetPacking : DecisionProblem Lax799700.SetFamily.setSystem := 235 DecisionProblem.ofPred HasLargeSetPacking 236 237 /-- The yes-instances of SetPacking are exactly the structures satisfying 238 `HasLargeSetPacking`. -/ 239 axiom setPacking_iff : ∀ (A : Type) [Lax799700.SetFamily.setSystem.Structure A], SetPacking A ↔ HasLargeSetPacking A 240 241 /-- SetPacking is NP-complete. -/ 242 axiom setPacking_NP_complete : NP.Complete SetPacking 243 244 /-- The property `HasSetSplitting` is isomorphism-invariant. -/ 245 axiom hasSetSplitting_iso : ∀ {A B : Type} [Lax799700.SetFamily.setSystem.Structure A] [Lax799700.SetFamily.setSystem.Structure B], 246 (A ≃[Lax799700.SetFamily.setSystem] B) → (HasSetSplitting A ↔ HasSetSplitting B) 247 248 /-- The problem SetSplitting: does the structure satisfy `HasSetSplitting`? -/ 249 def SetSplitting : DecisionProblem Lax799700.SetFamily.setSystem := 250 DecisionProblem.ofPred HasSetSplitting 251 252 /-- The yes-instances of SetSplitting are exactly the structures satisfying 253 `HasSetSplitting`. -/ 254 axiom setSplitting_iff : ∀ (A : Type) [Lax799700.SetFamily.setSystem.Structure A], SetSplitting A ↔ HasSetSplitting A 255 256 /-- SetSplitting is NP-complete. -/ 257 axiom setSplitting_NP_complete : NP.Complete SetSplitting 258 259 end Lax799700.SetFamily 260 - thm✓
Loading the paper…