The Reduction from Satisfiability to Hitting Set

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

definition

Loading review…

Natural Language Statement

Definition

A CNF formula $F$ on the variables $x_0, \dots, x_{V-1}$ becomes an instance of Hitting Set on the universe $\{0, \dots, 2V - 1\}$ , in which $2i$ stands for the literal $x_i$ and $2i + 1$ for $\bar x_i$ . The family has one set $\{2i, 2i+1\}$ for each variable and one set for each clause, holding the elements of its literals; the required size is $V$ .

A hitting set of size $V$ meets each of the $V$ disjoint pairs in exactly one element, so it is a truth assignment, and it meets the set of a clause exactly when the assignment satisfies the clause. This is the composition of Karp's reductions from satisfiability to Clique and from Clique to Node Cover, read on the literals rather than on the occurrences.

The reduction on words decodes a formula, builds the instance and encodes it; a word that encodes no formula is treated as the formula with one empty clause, whose instance has no hitting set.

Concept map

10 concepts; 1 descendant hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

In the paper

page 8 of this submission's paper

Lean source view on GitHub

1	import Lax496464.HittingSet
2	import Lax429075.Satisfiability
3
4	/-!
5	---
6	title: The Reduction from Satisfiability to Hitting Set
7	type: definition
8	---
9	A CNF formula $F$ on the variables $x_0, \dots, x_{V-1}$ becomes an instance of Hitting Set
10	on the universe $\{0, \dots, 2V - 1\}$ , in which $2i$ stands for the literal $x_i$ and
11	$2i + 1$ for $\bar x_i$ . The family has one set $\{2i, 2i+1\}$ for each variable and one set
12	for each clause, holding the elements of its literals; the required size is $V$ .
13
14	A hitting set of size $V$ meets each of the $V$ disjoint pairs in exactly one element, so
15	it is a truth assignment, and it meets the set of a clause exactly when the assignment
16	satisfies the clause. This is the composition of Karp's reductions from satisfiability to
17	Clique and from Clique to Node Cover, read on the literals rather than on the occurrences.
18
19	The reduction on words decodes a formula, builds the instance and encodes it; a word that
20	encodes no formula is treated as the formula with one empty clause, whose instance has no
21	hitting set.
22
23	# Formalization Notes
24
25	Formulas, their binary encoding and satisfiability are those of the archive's Cook–Levin
26	theorem (`lax-429075`).
27
28	The number of variables is one more than the largest index occurring, and at least two: the
29	hardness statements ask for a solution size of at least two, and a fresh pair costs nothing.
30	An empty clause gives an empty set, which no hitting set meets, as it should.
31
32	The sets are written as lists of elements, and the family is the membership predicate of
33	those lists on `Fin (2V)`; an element of a clause lies below $2V$ by the choice of $V$ .
34	-/
35
36	namespace Lax496464.HittingSetFromSat
37
38	open Lax429075.CNF Lax429075.Encoding Lax434930.PolynomialTime Lax496464.HittingSet
39
40	/-- One more than the largest variable index of the formula, and `1` for no literal. -/
41	def bound (F : Formula) : ℕ := (F.flatMap id).foldr (fun l n => max (l.index + 1) n) 1
42
43	/-- The number of variables of the construction: the formula's, but at least two. -/
44	def vars (F : Formula) : ℕ := max (bound F) 2
45
46	/-- The element standing for a literal: `2i` for `x_i`, `2i + 1` for `¬x_i`. -/
47	def elem (l : Literal) : ℕ := 2 * l.index + if l.positive then 0 else 1
48
49	/-- The sets, as lists of elements: the pair of each variable, then the elements of each
50	clause. -/
51	def sets (F : Formula) : List (List ℕ) :=
52	(List.range (vars F)).map (fun i => [2 * i, 2 * i + 1]) ++ F.map fun C => C.map elem
53
54	/-- The instance of a formula: the universe `2·vars F`, one set per variable and one per
55	clause. -/
56	def inst (F : Formula) : Instance where
57	n := 2 * vars F
58	m := vars F + F.length
59	F := fun j => Finset.univ.filter fun i : Fin (2 * vars F) => (i : ℕ) ∈ (sets F).getD j []
60
61	/-- The instance with its solution size. -/
62	def transform (F : Formula) : Instance × ℕ := (inst F, vars F)
63
64	/-- The formula a word encodes, and the formula with one empty clause if it encodes none. -/
65	def parseF (w : Word) : Formula := (decodeCNF w).getD [[]]
66
67	/-- The reduction on words, to an instance with its solution size. -/
68	def reduce (w : Word) : Instance × ℕ := transform (parseF w)
69
70	/-- The reduction on words, to the binary word of the instance. -/
71	def reduceWord (w : Word) : Word := encodeInstance (reduce w).1 (reduce w).2
72
73	end Lax496464.HittingSetFromSat
74

Formalization Notes

Formulas, their binary encoding and satisfiability are those of the archive's Cook–Levin theorem ( $lax-429075$ ).

The number of variables is one more than the largest index occurring, and at least two: the hardness statements ask for a solution size of at least two, and a fresh pair costs nothing. An empty clause gives an empty set, which no hitting set meets, as it should.

The sets are written as lists of elements, and the family is the membership predicate of those lists on $Fin (2V)$ ; an element of a clause lies below $2V$ by the choice of $V$ .

Builds on

Used by

Lax496464.HittingSetHardness

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

The Reduction from Satisfiability to Hitting Set

Flags

Flag this concept

Natural Language Statement

Definition

In the paper

Lean source view on GitHub

Discussion

Settings

Your comments