FPT-Reductions, FPT, Hardness and Completeness

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

definition

Loading review…

Natural Language Statement

Definition

A parameterized problem consists of a set of instances, the yes-instances among them, and a parameter $\kappa$ assigning a number to each instance; $\kappa$ is required to be computable in polynomial time [FG06, Definition 1.1]. The problem is fixed-parameter tractable if it is decided in time $f(\kappa(x))\cdot|x|^{O(1)}$ for a computable $f$ [FG06, Definition 1.4].

An fpt-reduction from $(P, \kappa)$ to $(Q, \kappa')$ is a map $R$ such that [FG06, Definition 2.1]

$x$ is a yes-instance of $P$ if and only if $R(x)$ is a yes-instance of $Q$ ;
$\kappa'(R(x)) \le g(\kappa(x))$ for a computable function $g$ ;
$R$ is computable in time $f(\kappa(x))\cdot|x|^{O(1)}$ for a computable $f$ .

For a class $C$ of parameterized problems, $[C]^{\mathrm{fpt}}$ is the class of parameterized problems that fpt-reduce to a member of $C$ . A problem is $C$ -hard if every member of $C$ fpt-reduces to it, and $C$ -complete if it is moreover a member of $C$ [FG06, Chapter 2].

Concept map

7 concepts; 21 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

1	import Lax496464.WH_A1_FptTime
2	import Lax888481.ParameterizedComplexity
3
4	/-!
5	---
6	title: FPT-Reductions, FPT, Hardness and Completeness
7	type: definition
8	---
9	A parameterized problem consists of a set of instances, the yes-instances among them, and a
10	parameter $\kappa$ assigning a number to each instance; $\kappa$ is required to be computable in
11	polynomial time [FG06, Definition 1.1]. The problem is fixed-parameter tractable if it is
12	decided in time $f(\kappa(x))\cdot\|x\|^{O(1)}$ for a computable $f$ [FG06, Definition 1.4].
13
14	An fpt-reduction from $(P, \kappa)$ to $(Q, \kappa')$ is a map $R$ such that
15	[FG06, Definition 2.1]
16
17	1. $x$ is a yes-instance of $P$ if and only if $R(x)$ is a yes-instance of $Q$ ;
18	2. $\kappa'(R(x)) \le g(\kappa(x))$ for a computable function $g$ ;
19	3. $R$ is computable in time $f(\kappa(x))\cdot\|x\|^{O(1)}$ for a computable $f$ .
20
21	For a class $C$ of parameterized problems, $[C]^{\mathrm{fpt}}$ is the class of parameterized
22	problems that fpt-reduce to a member of $C$ . A problem is $C$ -hard if every member of $C$
23	fpt-reduces to it, and $C$ -complete if it is moreover a member of $C$ [FG06, Chapter 2].
24
25	# Formalization Notes
26
27	Problems are the archive's `Lax888481.ParameterizedComplexity.Problem`: a set `Domain` of words
28	encoding instances, a predicate `Yes`, and the parameter `param`. Reductions and algorithms are
29	constrained on the domain only.
30
31	The three conditions of an fpt-reduction are separate definitions — `IsReduction`,
32	`ParamBounded` and `FptTimeOn` — so that a hardness proof establishes the construction and its
33	correctness, the parameter bound, and the running time one at a time. `IsFptReduction` bundles
34	them, and `P ≤ᶠᵖᵗ Q` (`FptReduces`, scoped notation: `open Lax496464.WH_A2_FptReductions`) states
35	that one exists. Polynomial-time reductions and the archive's strict fpt-reductions are
36	fpt-reductions by `WH_A5_Bridges`.
37
38	Classes. `Closure C` contains only parameterized problems (`IsParameterized`); `Hard` places no
39	such condition on the hard problem. An algorithm witnessing `FPT` writes `[1]` on yes-instances
40	and `[0]` on no-instances.
41	-/
42
43	namespace Lax496464.WH_A2_FptReductions
44
45	open Lax888481.ParameterizedComplexity (Problem)
46	open Lax496464.WH_A1_FptTime
47
48	/-- Step 1 of a reduction: construction and correctness. `R` maps instances of `P` to
49	instances of `Q`, yes-instances to yes-instances and no-instances to no-instances. -/
50	structure IsReduction (P Q : Problem) (R : List ℕ → List ℕ) : Prop where
51	/-- Instances go to instances. -/
52	maps_domain : ∀ x ∈ P.Domain, R x ∈ Q.Domain
53	/-- Yes-instances go to yes-instances, and no-instances to no-instances. -/
54	correct : ∀ x ∈ P.Domain, (P.Yes x ↔ Q.Yes (R x))
55
56	/-- Step 2 of a reduction: the parameter bound. The parameter of `R x` is at most a computable
57	function of the parameter of `x`. -/
58	def ParamBounded (P Q : Problem) (R : List ℕ → List ℕ) : Prop :=
59	∃ g : ℕ → ℕ, Computable g ∧ ∀ x ∈ P.Domain, Q.param (R x) ≤ g (P.param x)
60
61	/-- An fpt-reduction [FG06, Definition 2.1]: a reduction with a bounded parameter,
62	computable in fixed-parameter time (step 3) on the instances of `P`. -/
63	structure IsFptReduction (P Q : Problem) (R : List ℕ → List ℕ) : Prop where
64	/-- Construction and correctness. -/
65	reduction : IsReduction P Q R
66	/-- The parameter bound. -/
67	param_bounded : ParamBounded P Q R
68	/-- The running time. -/
69	fpt_time : FptTimeOn P.Domain P.param R
70
71	/-- `P` fpt-reduces to `Q`. -/
72	def FptReduces (P Q : Problem) : Prop := ∃ R, IsFptReduction P Q R
73
74	@[inherit_doc] scoped infix:50 " ≤ᶠᵖᵗ " => FptReduces
75
76	/-- `P` is a parameterized problem: its parameter is computable
77	in polynomial time on its instances [FG06, Definition 1.1]. -/
78	def IsParameterized (P : Problem) : Prop := PolyTimeOn P.Domain fun x => [P.param x]
79
80	open Classical in
81	/-- FPT: the parameterized problems decided in fixed-parameter time, the program writing `[1]`
82	on yes-instances and `[0]` on no-instances [FG06, Definition 1.4]. -/
83	def FPT : Set Problem :=
84	{P \| IsParameterized P ∧ FptTimeOn P.Domain P.param fun x => if P.Yes x then [1] else [0]}
85
86	/-- `[C]^fpt`: the parameterized problems that fpt-reduce to a member of `C`. -/
87	def Closure (C : Set Problem) : Set Problem :=
88	{P \| IsParameterized P ∧ ∃ Q ∈ C, P ≤ᶠᵖᵗ Q}
89
90	/-- `Q` is `C`-hard: every member of `C` fpt-reduces to it. -/
91	def Hard (C : Set Problem) (Q : Problem) : Prop := ∀ P ∈ C, P ≤ᶠᵖᵗ Q
92
93	/-- `Q` is `C`-complete: it belongs to `C` and is `C`-hard. -/
94	def Complete (C : Set Problem) (Q : Problem) : Prop := Q ∈ C ∧ Hard C Q
95
96	end Lax496464.WH_A2_FptReductions
97

Formalization Notes

Problems are the archive's $Lax888481.ParameterizedComplexity.Problem$ : a set $Domain$ of words encoding instances, a predicate $Yes$ , and the parameter $param$ . Reductions and algorithms are constrained on the domain only.

The three conditions of an fpt-reduction are separate definitions — $IsReduction$ , $ParamBounded$ and $FptTimeOn$ — so that a hardness proof establishes the construction and its correctness, the parameter bound, and the running time one at a time. $IsFptReduction$ bundles them, and $P ≤ᶠᵖᵗ Q$ ( $FptReduces$ , scoped notation: $open Lax496464.WH_A2_FptReductions$ ) states that one exists. Polynomial-time reductions and the archive's strict fpt-reductions are fpt-reductions by $WH_A5_Bridges$ .

Classes. $Closure C$ contains only parameterized problems ( $IsParameterized$ ); $Hard$ places no such condition on the hard problem. An algorithm witnessing $FPT$ writes $[1]$ on yes-instances and $[0]$ on no-instances.

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

FPT-Reductions, FPT, Hardness and Completeness

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments