Hitting Set

Lax496464.HittingSet · concepts/Lax496464/HittingSet.lean · lax-496464

definition

Loading review…

Natural Language Statement

Definition

An instance consists of a universe $\{1, \dots, n\}$ and a family $F_1, \dots, F_m$ of subsets of it; together with an integer $k$ it asks whether some $H$ with $|H| = k$ meets every set of the family. Hitting Set is the problem the hardness results of this submission reduce from, parameterized by the solution size $k$ .

This is the problem [SP8] of Garey and Johnson. It contains Karp's Node Cover (problem 5 of his list) as the case of sets of size two. Karp's own Hitting Set (problem 15) is a different problem: it asks for a set meeting every member of the family in exactly one element.

The instances considered here are those with $2 \le k \le n$ . The lower bound is what the construction of the reduction needs, and the upper bound is a normalization: a hitting set of size exactly $k$ cannot exist once $k$ exceeds the universe. Neither restriction costs anything — see the statement of the problem's hardness.

Concept map

5 concepts; 10 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

In the paper

page 7 of this submission's paper

Lean source view on GitHub

1	import Lax496464.ParameterizedComplexity
2	import Lax434930.PolynomialTime
3	import Mathlib.Data.List.FinRange
4	import Mathlib.Data.Nat.Bits
5
6	/-!
7	---
8	title: Hitting Set
9	type: definition
10	---
11	An instance consists of a universe $\{1, \dots, n\}$ and a family $F_1, \dots, F_m$ of
12	subsets of it; together with an integer $k$ it asks whether some $H$ with $\|H\| = k$ meets
13	every set of the family. Hitting Set is the problem the hardness results of this
14	submission reduce from, parameterized by the solution size $k$ .
15
16	This is the problem [SP8] of Garey and Johnson. It contains Karp's Node Cover (problem 5
17	of his list) as the case of sets of size two. Karp's own Hitting Set (problem 15) is a
18	different problem: it asks for a set meeting every member of the family in exactly one
19	element.
20
21	The instances considered here are those with $2 \le k \le n$ . The lower bound is what the
22	construction of the reduction needs, and the upper bound is a normalization: a hitting
23	set of size exactly $k$ cannot exist once $k$ exceeds the universe. Neither restriction
24	costs anything — see the statement of the problem's hardness.
25
26	# Formalization Notes
27
28	The family is presented to a machine in the compressed sparse row form that presents a
29	graph to a machine elsewhere in the archive: an array of $m+1$ offsets cutting a member
30	array into one block per set. The blocks are not required to be sorted and repetitions
31	are not forbidden; leaving those conditions out admits more words and therefore
32	strengthens every claim about programs reading the format. The solution size is the final
33	entry, so that the family occupies the same offsets whether or not it is followed by one.
34
35	The universe is `Fin n`, counted from zero where the paper counts from one. The
36	construction of the reduction uses an element as an additive offset inside a due date and
37	needs it to be at least one, so it adds one; that is a detail of the construction and not
38	of the problem.
39
40	The required size is exact, $\|H\| = k$ , as the paper writes it. For a nonempty universe
41	the exact and the "at most" versions are interchangeable, and the exact one is what the
42	construction's target is calibrated against.
43
44	The universe is required to be no larger than the word: $n \le \|x\|$ . Every reduction of this
45	submission writes an instance of size at least $n^2$ , and a word states $n$ as a single
46	entry, so without the bound a word of five entries could name a universe of a billion
47	elements and no reduction could write its image in time bounded by the length of the word.
48	The bound costs nothing — an element occurring in no set can be deleted and the others
49	renumbered, and the reduction from satisfiability of `HittingSetFromSat` already emits
50	instances with $n + m$ polynomial in the size of its input — and it agrees with the
51	convention that every element of the universe occurs.
52
53	The binary encoding exists beside the word encoding for the same reason as elsewhere: a
54	claim quantifying over NP is a claim about a Turing machine and hence about bits. It
55	writes the two counts and the solution size, and then each set as its size followed by its
56	members in increasing order. A number is written as its binary digits, least significant
57	first, preceded by their number in unary; that code is prefix-free, so the encoding is
58	injective. The language of Hitting Set is the set of binary words of the instances, with a
59	solution size, that have a hitting set of that size.
60	-/
61
62	namespace Lax496464.HittingSet
63
64	open Lax496464.ParameterizedComplexity Lax434930.PolynomialTime
65
66	/-- An instance of Hitting Set: a universe `Fin n` and a family of `m` subsets of it. The
67	solution size is carried separately, as the parameter. -/
68	structure Instance where
69	/-- The size `n` of the universe. -/
70	n : ℕ
71	/-- The number `m` of sets in the family. -/
72	m : ℕ
73	/-- The family `F₁, …, F_m`. -/
74	F : Fin m → Finset (Fin n)
75
76	/-- `P` has a hitting set of size exactly `k`. -/
77	def Instance.HasHittingSet (P : Instance) (k : ℕ) : Prop :=
78	∃ H : Finset (Fin P.n), H.card = k ∧ ∀ j : Fin P.m, ∃ i ∈ H, i ∈ P.F j
79
80	/-- The size of the universe declared by a word: its first entry. -/
81	def universeSize (x : List ℕ) : ℕ := x.getD 0 0
82
83	/-- The number of sets declared by a word: its second entry. -/
84	def setCount (x : List ℕ) : ℕ := x.getD 1 0
85
86	/-- The `i`-th offset: the `m+1` offsets follow the two header entries. -/
87	def offset (x : List ℕ) (i : ℕ) : ℕ := x.getD (2 + i) 0
88
89	/-- The `t`-th entry of the member array, which follows the offsets. -/
90	def member (x : List ℕ) (t : ℕ) : ℕ := x.getD (3 + setCount x + t) 0
91
92	/-- The solution size `k`: the entry following the member array. -/
93	def solutionSize (x : List ℕ) : ℕ :=
94	x.getD (3 + setCount x + offset x (setCount x)) 0
95
96	/-- The word `x` encodes the instance `P` with solution size `k`. -/
97	structure Encodes (x : List ℕ) (P : Instance) (k : ℕ) : Prop where
98	/-- The word declares `P`'s universe. -/
99	universeSize_eq : universeSize x = P.n
100	/-- The word declares `P`'s family. -/
101	setCount_eq : setCount x = P.m
102	/-- The word is the two header entries, the `m+1` offsets, a member array as long as
103	the last offset says, and the solution size. -/
104	length_eq : x.length = 4 + P.m + offset x P.m
105	/-- The block of the first set begins at the start of the member array. -/
106	offset_zero : offset x 0 = 0
107	/-- The offsets are nondecreasing, so they cut the member array into one block per
108	set. -/
109	offset_mono : ∀ j < P.m, offset x j ≤ offset x (j + 1)
110	/-- Every entry of the member array is an element of the universe. -/
111	member_lt : ∀ t < offset x P.m, member x t < P.n
112	/-- The block of a set lists exactly its elements. -/
113	mem_iff : ∀ (j : Fin P.m) (i : Fin P.n),
114	i ∈ P.F j ↔ ∃ t, offset x j ≤ t ∧ t < offset x (j + 1) ∧ member x t = i
115	/-- The word declares the solution size. -/
116	solutionSize_eq : solutionSize x = k
117	/-- The solution size is at least two and at most the size of the universe. -/
118	size_bounds : 2 ≤ k ∧ k ≤ P.n
119	/-- The universe is no larger than the word that presents it. -/
120	universeSize_le : P.n ≤ x.length
121
122	/-- The words that encode an instance with its solution size. -/
123	def Instances : Set (List ℕ) := {x \| ∃ P k, Encodes x P k}
124
125	/-- Hitting Set, parameterized by the solution size. -/
126	def byK : Problem where
127	Domain := Instances
128	Yes x := ∃ P k, Encodes x P k ∧ Instance.HasHittingSet P k
129	param x := solutionSize x
130
131	/-- The elements of the `j`-th set, in the order of the universe. -/
132	def Instance.members (P : Instance) (j : Fin P.m) : List (Fin P.n) :=
133	(List.finRange P.n).filter fun i => decide (i ∈ P.F j)
134
135	/-- A natural number as a binary word: its digits, least significant first, preceded by
136	their number in unary. -/
137	def encodeNat (n : ℕ) : Word :=
138	List.replicate n.bits.length true ++ [false] ++ n.bits
139
140	/-- An instance with its solution size as a binary word: the two counts, the solution
141	size, and then each set as its size followed by its members. -/
142	def encodeInstance (P : Instance) (k : ℕ) : Word :=
143	encodeNat P.n ++ encodeNat P.m ++ encodeNat k ++
144	(List.finRange P.m).flatMap fun j =>
145	encodeNat (P.F j).card ++ (P.members j).flatMap fun i => encodeNat i
146
147	/-- Hitting Set as a language: the binary words of the instances, with a solution size,
148	that have a hitting set of that size. -/
149	def HittingSetLanguage : Language :=
150	{w \| ∃ (P : Instance) (k : ℕ), encodeInstance P k = w ∧ P.HasHittingSet k}
151
152	end Lax496464.HittingSet
153

Formalization Notes

The family is presented to a machine in the compressed sparse row form that presents a graph to a machine elsewhere in the archive: an array of $m+1$ offsets cutting a member array into one block per set. The blocks are not required to be sorted and repetitions are not forbidden; leaving those conditions out admits more words and therefore strengthens every claim about programs reading the format. The solution size is the final entry, so that the family occupies the same offsets whether or not it is followed by one.

The universe is $Fin n$ , counted from zero where the paper counts from one. The construction of the reduction uses an element as an additive offset inside a due date and needs it to be at least one, so it adds one; that is a detail of the construction and not of the problem.

The required size is exact, $|H| = k$ , as the paper writes it. For a nonempty universe the exact and the "at most" versions are interchangeable, and the exact one is what the construction's target is calibrated against.

The universe is required to be no larger than the word: $n \le |x|$ . Every reduction of this submission writes an instance of size at least $n^2$ , and a word states $n$ as a single entry, so without the bound a word of five entries could name a universe of a billion elements and no reduction could write its image in time bounded by the length of the word. The bound costs nothing — an element occurring in no set can be deleted and the others renumbered, and the reduction from satisfiability of $HittingSetFromSat$ already emits instances with $n + m$ polynomial in the size of its input — and it agrees with the convention that every element of the universe occurs.

The binary encoding exists beside the word encoding for the same reason as elsewhere: a claim quantifying over NP is a claim about a Turing machine and hence about bits. It writes the two counts and the solution size, and then each set as its size followed by its members in increasing order. A number is written as its binary digits, least significant first, preceded by their number in unary; that code is prefix-free, so the encoding is injective. The language of Hitting Set is the set of binary words of the instances, with a solution size, that have a hitting set of that size.

Builds on

Used by

From Mathlib

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

Hitting Set

Flags

Flag this concept

Natural Language Statement

Definition

In the paper

Lean source view on GitHub

Discussion

Settings

Your comments