Rounding the Weights, and What an Approximation Scheme Delivers

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

definition

Loading review…

Natural Language Statement

Definition

The rounding behind the fifth theorem, and the shape of the guarantee it gives.

Rounding every weight up to a multiple of $k$ and dividing by $k$ leaves an instance with the same jobs whose weights are smaller by a factor of about $k$ . A set that is optimal for the rounded weights loses, against the true optimum, at most $k$ per job selected, hence at most $kn$ in total; and since the optimum is at least the largest single weight, choosing $k$ so that $kn$ is a small fraction of the largest weight makes the loss a small fraction of the optimum. That is the chain of inequalities (8), and what it delivers is stated with the theorem that uses it.

An approximation scheme is a program that is handed an instance together with a positive integer $e$ and returns a number $W$ that a feasible set reaches, and that is within a factor $1 - 1/e$ of the optimum.

Concept map

7 concepts; 1 descendant 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.Problems
2
3	/-!
4	---
5	title: Rounding the Weights, and What an Approximation Scheme Delivers
6	type: definition
7	---
8	The rounding behind the fifth theorem, and the shape of the guarantee it gives.
9
10	Rounding every weight up to a multiple of $k$ and dividing by $k$ leaves an instance with
11	the same jobs whose weights are smaller by a factor of about $k$ . A set that is optimal
12	for the rounded weights loses, against the true optimum, at most $k$ per job selected,
13	hence at most $kn$ in total; and since the optimum is at least the largest single weight,
14	choosing $k$ so that $kn$ is a small fraction of the largest weight makes the loss a small
15	fraction of the optimum. That is the chain of inequalities (8), and what it delivers is
16	stated with the theorem that uses it.
17
18	An approximation scheme is a program that is handed an instance together with a
19	positive integer $e$ and returns a number $W$ that a feasible set reaches, and that is within
20	a factor $1 - 1/e$ of the optimum.
21
22	# Formalization Notes
23
24	The accuracy is a positive integer $e$ rather than a rational $\varepsilon$ , and the
25	guarantee is written as $(e-1)\,\mathrm{opt} \le e\,W$ . This is the same statement as
26	$(1-\varepsilon)\,\mathrm{opt} \le W$ with $\varepsilon = 1/e$ , in whole numbers, which
27	is what the input of a machine and the arithmetic of the bound both want. A scheme for
28	every $1/e$ is a scheme for every $\varepsilon$ , since every positive rational exceeds
29	some $1/e$ .
30
31	The program returns a number rather than the set: a value $W$ such that some feasible set
32	has weight at least $W$ , and such that $(e-1)\,\mathrm{opt} \le e\,W$ . Since $W$ never exceeds
33	the optimum either, this is the usual value form of an approximation guarantee, and there is
34	a feasible set whose weight is at least $W \ge (1-1/e)\,\mathrm{opt}$ . The output is a single
35	number, as the decision programs' is. The program is not asked to name that set, nor to
36	return its exact weight: which is not something the exact algorithms it is built from
37	retain, and which the paper's guarantee does not constrain.
38
39	What a scheme delivers is not a function of its input — many sets meet the guarantee — so
40	it cannot be stated through the notion of computing a function within a time bound. It is
41	stated directly: on every admissible input the machine halts within the bound, having
42	written some output that meets the guarantee.
43
44	The instance is presented without a threshold, with the accuracy in the position the
45	threshold would occupy. An approximation instance is therefore a decision instance read
46	differently, which costs nothing and keeps one format.
47	-/
48
49	namespace Lax496464.Fptas
50
51	open Lax496464.FlowShop Lax496464.FlowShop.Instance
52	open Lax496464.WordEncoding Lax496464.Problems
53	open Lax808846.Ram
54
55	variable (I : Instance)
56
57	/-- The largest weight of a single job. -/
58	def wmax : ℕ := ((List.finRange I.jobs).map I.w).foldr max 0
59
60	/-- The instance with every weight rounded up to a multiple of `k` and divided by it. -/
61	def rescale (k : ℕ) : Instance where
62	jobs := I.jobs
63	machines := I.machines
64	p := I.p
65	q := I.q
66	d := I.d
67	w j := (I.w j + (k - 1)) / k
68
69	variable {I}
70
71	variable (I)
72
73	/-- The word `x` presents the instance `I` together with the accuracy `e`. -/
74	def EncodesApprox (x : List ℕ) (e : ℕ) : Prop :=
75	∃ y, x = y ++ [e] ∧ 1 ≤ e ∧ EncodesInstance y I
76
77	variable {I}
78
79	/-- The words that present an instance together with an accuracy. -/
80	def ApproxInstances : Set (List ℕ) := {x \| ∃ I e, EncodesApprox I x e}
81
82	/-- The output `y` is an acceptable answer on the input `x`: a number that some feasible set
83	reaches, within a factor `1 − 1/e` of the optimum. -/
84	def Delivers (x y : List ℕ) : Prop :=
85	∃ (I : Instance) (e W : ℕ), EncodesApprox I x e ∧ y = [W] ∧
86	HasWeight I W ∧ (e - 1) * optimum I ≤ e * W
87
88	/-- At word length `w`, on every admissible input, the program halts within `T x`
89	instructions having written an acceptable answer. -/
90	def ApproximatesInTime (w : ℕ) (prog : Program) (D : Set (List ℕ))
91	(T : List ℕ → ℕ) : Prop :=
92	∀ x ∈ D, ∃ (y : List ℕ) (t : ℕ), t ≤ T x ∧ RunsTo w prog x y t ∧ Delivers x y
93
94	end Lax496464.Fptas
95

Formalization Notes

The accuracy is a positive integer $e$ rather than a rational $\varepsilon$ , and the guarantee is written as $(e-1)\,\mathrm{opt} \le e\,W$ . This is the same statement as $(1-\varepsilon)\,\mathrm{opt} \le W$ with $\varepsilon = 1/e$ , in whole numbers, which is what the input of a machine and the arithmetic of the bound both want. A scheme for every $1/e$ is a scheme for every $\varepsilon$ , since every positive rational exceeds some $1/e$ .

The program returns a number rather than the set: a value $W$ such that some feasible set has weight at least $W$ , and such that $(e-1)\,\mathrm{opt} \le e\,W$ . Since $W$ never exceeds the optimum either, this is the usual value form of an approximation guarantee, and there is a feasible set whose weight is at least $W \ge (1-1/e)\,\mathrm{opt}$ . The output is a single number, as the decision programs' is. The program is not asked to name that set, nor to return its exact weight: which is not something the exact algorithms it is built from retain, and which the paper's guarantee does not constrain.

What a scheme delivers is not a function of its input — many sets meet the guarantee — so it cannot be stated through the notion of computing a function within a time bound. It is stated directly: on every admissible input the machine halts within the bound, having written some output that meets the guarantee.

The instance is presented without a threshold, with the accuracy in the position the threshold would occupy. An approximation instance is therefore a decision instance read differently, which costs nothing and keeps one format.

Builds on

Lax496464.Problems

Used by

Lax496464.Theorem5

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

Rounding the Weights, and What an Approximation Scheme Delivers

Flags

Flag this concept

Natural Language Statement

Definition

In the paper

Lean source view on GitHub

Discussion

Settings

Your comments