Hitting Set

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

definition

Loading review…

Natural Language Statement

Definition

$p$ -Hitting-Set. Instance: a hypergraph — a universe and a family of subsets of it — and $k \in \mathbb N$ . Parameter: $k$ . Question: is there a set of $k$ elements of the universe that meets every set of the family? [FG06, Example 4.42]

Concept map

7 concepts; 3 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

1	import Lax888481.ParameterizedComplexity
2	import Lax496464.HittingSet
3
4	/-!
5	---
6	title: Hitting Set
7	type: definition
8	---
9	$p$ -Hitting-Set. Instance: a hypergraph — a universe and a family of subsets of it — and
10	$k \in \mathbb N$ . Parameter: $k$ . Question: is there a set of $k$ elements of the universe that
11	meets every set of the family? [FG06, Example 4.42]
12
13	# Formalization Notes
14
15	The instances and the question are those of the Hitting Set of the just-in-time flow shop part of
16	this submission (`Lax496464.HittingSet`): a universe $\{0,\dots,n-1\}$ , sets
17	$F_0,\dots,F_{m-1}$ and an exact size $k$ . The word is its binary encoding of the instance with $k$ ,
18	each bit written as the number $0$ or $1$ . Hardness results for this problem are therefore results
19	about the problem the flow shop reductions start from.
20
21	The binary code is prefix-free, so a word encodes at most one instance and one $k$ ; the parameter
22	of a word is the $k$ it encodes. Since $n$ and $k$ are written in binary, a reduction from this
23	problem that ranges over the universe first restricts it to the elements occurring in the sets.
24	-/
25
26	namespace Lax496464.WH_C2_HittingSet
27
28	open Lax496464.HittingSet
29	open Lax888481.ParameterizedComplexity (Problem)
30
31	/-- The word of an instance with solution size `k`: its binary word, one number `0` or `1` per
32	bit. -/
33	def word (P : Instance) (k : ℕ) : List ℕ := (encodeInstance P k).map fun b => if b then 1 else 0
34
35	open Classical in
36	/-- The solution size a word encodes (`0` on other words). -/
37	noncomputable def sizeParam (x : List ℕ) : ℕ :=
38	if h : ∃ p : Instance × ℕ, x = word p.1 p.2 then (Classical.choose h).2 else 0
39
40	/-- `p-Hitting-Set`. -/
41	noncomputable def HittingSet : Problem where
42	Domain := {x \| ∃ P k, x = word P k}
43	Yes x := ∃ P k, x = word P k ∧ P.HasHittingSet k
44	param := sizeParam
45
46	end Lax496464.WH_C2_HittingSet
47

Formalization Notes

The instances and the question are those of the Hitting Set of the just-in-time flow shop part of this submission ( $Lax496464.HittingSet$ ): a universe $\{0,\dots,n-1\}$ , sets $F_0,\dots,F_{m-1}$ and an exact size $k$ . The word is its binary encoding of the instance with $k$ , each bit written as the number $0$ or $1$ . Hardness results for this problem are therefore results about the problem the flow shop reductions start from.

The binary code is prefix-free, so a word encodes at most one instance and one $k$ ; the parameter of a word is the $k$ it encodes. Since $n$ and $k$ are written in binary, a reduction from this problem that ranges over the universe first restricts it to the elements occurring in the sets.

Builds on

Used by

From Mathlib

none

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

Lean source view on GitHub

Discussion

Settings

Your comments