The Integer Programs of the Clients' Reduction Are Fixed-Parameter Tractable

Lax117284.IlpClients · concepts/Lax117284/IlpClients.lean · lax-117284

proven

Loading review…

Natural Language Statement

Definition

An integer program here is a system of $M$ linear equality constraints over $N$ non-negative integer variables, with non-negative integer coefficients and right-hand sides: find $x : Fin N → ℕ$ with $∑ᵢ a j i * x i = b j$ for every constraint $j$ . It is feasible if such an $x$ exists.

The integer programs that the paper solves with Lenstra's algorithm (Heeger–Hermelin–Itzhaki–Molter–Shabtay, proof of Theorem 4's third bullet, via the integer program of $Theorem4ILP.lean$ 's $HasILPSolution$ ) form one explicit family, one constraint matrix $A_n$ for each number $n$ of clients: $2 ^ (n * n)$ types of day (a type is a conflict relation on the clients), $2 ^ n$ subsets of clients, one variable for every pair of a type and a subset and one slack variable for every client, and one constraint for each type and one for each client. This module states, for exactly this family, that feasibility is fixed-parameter tractable in the number of variables: $ilpClients_fpt$ . The matrix is fixed by $n$ ; only the right-hand side (the number $cnt t$ of days of each type $t$ and the number $B$ of days a client may go unserved) is free. The reduction of the problem of the clients to this problem is $Theorem4.byClients_fptReduces_ilp$ , and $ilpClients_fpt$ is proved in the proofs package, by a guess-and-verify algorithm specific to these matrices, not cited.

Concept map

4 concepts; 1 descendant hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

Each proof establishes this claim relative to its assumptions.

no assumptions

def✓Lax117284.IlpClients

⊢Lax117284Proofs.Machine.Ilp.ilpClients_fpt_proved

In the paper

page 6 of this submission's paper

Lean source view on GitHub

Show types on hover

1	import Mathlib.Algebra.BigOperators.Group.Finset.Basic
2	import Mathlib.Data.Fintype.Fin
3	import Mathlib.Data.Nat.Bitwise
4	import Lax117284.ParameterizedComplexity
5
6	/-!
7	---
8	title: The Integer Programs of the Clients' Reduction Are Fixed-Parameter Tractable
9	type: definition
10	---
11	An integer program here is a system of `M` linear equality constraints over `N`
12	non-negative integer variables, with non-negative integer coefficients and right-hand
13	sides: find `x : Fin N → ℕ` with `∑ᵢ a j i * x i = b j` for every constraint `j`. It is
14	feasible if such an `x` exists.
15
16	The integer programs that the paper solves with Lenstra's algorithm (Heeger–Hermelin–Itzhaki–Molter–Shabtay,
17	proof of Theorem 4's third bullet, via the integer program of `Theorem4ILP.lean`'s `HasILPSolution`) form
18	one explicit family, one constraint matrix `A_n` for each number `n` of clients: `2 ^ (n * n)` types of day
19	(a type is a conflict relation on the clients), `2 ^ n` subsets of clients, one variable for every
20	pair of a type and a subset and one slack variable for every client, and one constraint for each
21	type and one for each client. This module states, for exactly this family, that feasibility is
22	fixed-parameter tractable in the number of variables: `ilpClients_fpt`. The matrix is fixed by `n`;
23	only the right-hand side (the number `cnt t` of days of each type `t` and the number `B` of days a
24	client may go unserved) is free. The reduction of the problem of the clients to this problem is
25	`Theorem4.byClients_fptReduces_ilp`, and `ilpClients_fpt` is proved in the proofs package, by a
26	guess-and-verify algorithm specific to these matrices, not cited.
27
28	# Formalization Notes
29
30	The family is written out here, the coefficient formula included, because this module cannot import the
31	proofs; the proofs identify it, definition by definition, with the construction of the reduction. Column
32	`t * 2^n + s` (`t` a type, `s` a subset of clients, both as numbers) has the coefficient `1` in the row of type
33	`t` and in the row of client `j` for every client `j` not in `s`, when `s` contains no two clients that `t` makes
34	conflict (`indepB`), and is the zero column otherwise; the column `2 ^ (n * n) * 2 ^ n + j` is the slack of client `j` and
35	has a single `1`, in the row of client `j`. The right-hand side is `cnt t` in the row of type `t` and `B` in
36	every client row.
37
38	The domain is the words of this family, which are the words of the integer programs that the reduction
39	outputs, and, in addition, the fixed word `[1, 1, 0, 1]` of the infeasible program `0 · x = 1`. It is
40	needed: for `n ≤ 1` every member of the family is feasible, whatever the right-hand side, so for a fairness
41	parameter above the number of days the reduction has no infeasible word of the family to output. The
42	word of an integer program is its two counts, then the `M * N` coefficients of the constraint matrix row
43	by row, then the `M` right-hand sides (the layout convention of `InstSem.lean`'s `instToks`); reading it back
44	is total, missing entries being read as `0`.
45
46	The bound of `FPT` is, as everywhere in this development, `c * g k * (\|x\| + 1) ^ c` with `g` an arbitrary
47	function of the parameter. The `g` of the proof is astronomically large (of the order of
48	`(n^n)^(2^(n²))` in the number `n` of clients, more than the paper's algorithm needs); it is a
49	function of the parameter alone, which is all fixed-parameter tractability asks. Unlike a general
50	integer-programming algorithm this one needs no factor polynomial in the word length: all its numbers stay
51	below a fixed power of the length of the word plus its largest entry.
52	-/
53
54	namespace Lax117284.IlpClients
55
56	open Lax117284.ParameterizedComplexity
57
58	/-- An integer program: `M` linear equality constraints over `N` non-negative integer
59	variables, with non-negative integer coefficients `a` and right-hand sides `b`. -/
60	structure ILP where
61	/-- The number of variables. -/
62	N : ℕ
63	/-- The number of constraints. -/
64	M : ℕ
65	/-- The coefficient of variable `i` in constraint `j`. -/
66	a : Fin M → Fin N → ℕ
67	/-- The right-hand side of constraint `j`. -/
68	b : Fin M → ℕ
69
70	/-- `E` is feasible: some assignment of its variables satisfies every constraint. -/
71	def ILP.Feasible (E : ILP) : Prop := ∃ x : Fin E.N → ℕ, ∀ j, ∑ i, E.a j i * x i = E.b j
72
73	/-- The numbers of an integer program: the two counts, then the coefficients row by row,
74	then the right-hand sides. Total and well-defined on every list, reading absent entries as
75	`0`, exactly like `Instance.pAt`/`Instance.dAt`. -/
76	def decodeILP (w : List ℕ) : ILP where
77	N := w.getD 0 0
78	M := w.getD 1 0
79	a := fun j i => w.getD (2 + j.val * w.getD 0 0 + i.val) 0
80	b := fun j => w.getD (2 + w.getD 1 0 * w.getD 0 0 + j.val) 0
81
82	/-- The number of types of day for `n` clients: `2 ^ (n * n)` (bit `a * n + b` of a type says
83	that clients `a` and `b` conflict on the days of that type). -/
84	def nT (n : ℕ) : ℕ := 2 ^ (n * n)
85
86	/-- The number of subsets of the `n` clients, `2 ^ n` (bit `j` of a subset says that client `j` is served). -/
87	def nZ (n : ℕ) : ℕ := 2 ^ n
88
89	/-- The number of pairs of a type and a subset, `2 ^ (n * n) * 2 ^ n`. -/
90	def nV (n : ℕ) : ℕ := nT n * nZ n
91
92	/-- The number of variables, `2 ^ (n * n) * 2 ^ n + n`: one for every pair of a type and a
93	subset, and one slack for every client. -/
94	def nN (n : ℕ) : ℕ := nV n + n
95
96	/-- The number of constraints, `2 ^ (n * n) + n`: one for every type and one for every client. -/
97	def nM (n : ℕ) : ℕ := nT n + n
98
99	/-- The subset `S` (a number) is independent for the type `t` (a number): it contains no two distinct
100	clients `a`, `b` that the type makes conflict (bit `a * n + b` of `t`). -/
101	def indepB (n t S : ℕ) : Bool :=
102	decide (∀ a < n, ∀ b < n, a ≠ b → S.testBit a = true → S.testBit b = true →
103	t.testBit (a * n + b) = false)
104
105	/-- The coefficient of variable `c` in constraint `r`: the variable `c < nV n` is the pair
106	of the type `c / 2 ^ n` and the subset `c % 2 ^ n`, whose column has a `1` in the row of its type and in the row
107	of every client outside the subset, unless the subset is not independent for the type, when the column is
108	zero; the other variables are the slacks, `1` in the row of their client. -/
109	def coef (n r c : ℕ) : ℕ :=
110	if c < nV n then
111	(if indepB n (c / nZ n) (c % nZ n) then
112	(if r < nT n then (if c / nZ n = r then 1 else 0)
113	else (if (c % nZ n).testBit (r - nT n) = false then 1 else 0))
114	else 0)
115	else (if nT n ≤ r ∧ c - nV n = r - nT n then 1 else 0)
116
117	/-- The word of the integer program of `n` clients with `cnt t` days of type `t` and `B` days that a
118	client may go unserved: the two counts, the coefficients row by row, and the right-hand sides, `cnt r` in the row
119	of type `r` and `B` in each client row. -/
120	def ilpWord (n : ℕ) (cnt : ℕ → ℕ) (B : ℕ) : List ℕ :=
121	[nN n, nM n] ++ (List.range (nM n * nN n)).map (fun i => coef n (i / nN n) (i % nN n))
122	++ (List.range (nM n)).map (fun r => if r < nT n then cnt r else B)
123
124	/-- The integer programs of the clients' reduction, as a parameterized problem: the domain is the words
125	`ilpWord n cnt B` of the family and the fixed word `[1, 1, 0, 1]` of the program `0 · x = 1`; a yes-instance
126	is a word whose integer program is feasible; the parameter is the number of variables. -/
127	def ilpClients : Problem where
128	Domain := {z \| (∃ n cnt B, z = ilpWord n cnt B) ∨ z = [1, 1, 0, 1]}
129	Yes z := (decodeILP z).Feasible
130	param z := (decodeILP z).N
131
132	/-- Integer programs of the clients' family are fixed-parameter tractable in the number of variables. -/
133	axiom ilpClients_fpt : FPT ilpClients
134
135	end Lax117284.IlpClients
136

Show Proof

Formalization Notes

The family is written out here, the coefficient formula included, because this module cannot import the proofs; the proofs identify it, definition by definition, with the construction of the reduction. Column $t * 2^n + s$ ( $t$ a type, $s$ a subset of clients, both as numbers) has the coefficient $1$ in the row of type $t$ and in the row of client $j$ for every client $j$ not in $s$ , when $s$ contains no two clients that $t$ makes conflict ( $indepB$ ), and is the zero column otherwise; the column $2 ^ (n * n) * 2 ^ n + j$ is the slack of client $j$ and has a single $1$ , in the row of client $j$ . The right-hand side is $cnt t$ in the row of type $t$ and $B$ in every client row.

The domain is the words of this family, which are the words of the integer programs that the reduction outputs, and, in addition, the fixed word $[1, 1, 0, 1]$ of the infeasible program $0 · x = 1$ . It is needed: for $n ≤ 1$ every member of the family is feasible, whatever the right-hand side, so for a fairness parameter above the number of days the reduction has no infeasible word of the family to output. The word of an integer program is its two counts, then the $M * N$ coefficients of the constraint matrix row by row, then the $M$ right-hand sides (the layout convention of $InstSem.lean$ 's $instToks$ ); reading it back is total, missing entries being read as $0$ .

The bound of $FPT$ is, as everywhere in this development, $c * g k * (|x| + 1) ^ c$ with $g$ an arbitrary function of the parameter. The $g$ of the proof is astronomically large (of the order of $(n^n)^(2^(n²))$ in the number $n$ of clients, more than the paper's algorithm needs); it is a function of the parameter alone, which is all fixed-parameter tractability asks. Unlike a general integer-programming algorithm this one needs no factor polynomial in the word length: all its numbers stay below a fixed power of the length of the word plus its largest entry.

Builds on

Lax117284.ParameterizedComplexity

Used by

Lax117284.Theorem4

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

The Integer Programs of the Clients' Reduction Are Fixed-Parameter Tractable

Flags

Flag this concept

Natural Language Statement

Definition

In the paper

Lean source view on GitHub

Discussion

Settings

Your comments