The Dynamic Program of Section 3, and Its Table

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

definition

Loading review…

Natural Language Statement

Definition

The algorithm behind the second theorem. The jobs are in earliest-start-time order and are considered one at a time, from the last to the first. The state carried is a set $X$ of at most $m$ thresholds, one per second-stage machine: the smallest index a job on that machine may have. The table entry

T[X, W']

is the earliest instant at which the first-stage machine may begin, if a set of jobs of total weight $W'$ compatible with $X$ is still to be preprocessed in time. It is $-\infty$ when no such set exists, and $+\infty$ when the empty set will do.

A set $Z$ is compatible with $X$ when each of its jobs can be assigned a threshold in $X$ not exceeding it, with no two conflicting jobs sharing a threshold. Taking $X$ to be the first $m$ indices asks for nothing beyond schedulability on $m$ machines, which is how the table is read off at the end.

The recursion removes the smallest threshold $j$ of $X$ and decides whether job $j$ is selected. If it is not, $j$ is replaced by the smallest index above it that is not already a threshold — the paper's $j_1$ — and the table is consulted at the resulting $X_1$ . If it is, the weight drops by $w_j$ and the budget by $p_j$ , and $j$ is replaced by the smallest index not already a threshold whose second operation starts at or after $d_j$ — the paper's $j_2$ — giving $X_2$ .

Concept map

3 concepts; 2 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

In the paper

page 3 of this submission's paper

Lean source view on GitHub

1	import Lax496464.EstOrder
2	import Mathlib.Data.Finset.Max
3
4	/-!
5	---
6	title: The Dynamic Program of Section 3, and Its Table
7	type: definition
8	---
9	The algorithm behind the second theorem. The jobs are in earliest-start-time order and
10	are considered one at a time, from the last to the first. The state carried is a set $X$
11	of at most $m$ thresholds, one per second-stage machine: the smallest index a job on
12	that machine may have. The table entry
13	$T[X, W']$
14	is the earliest instant at which the first-stage machine may begin, if a set of jobs of
15	total weight $W'$ compatible with $X$ is still to be preprocessed in time. It is $-\infty$
16	when no such set exists, and $+\infty$ when the empty set will do.
17
18	A set $Z$ is compatible with $X$ when each of its jobs can be assigned a threshold in
19	$X$ not exceeding it, with no two conflicting jobs sharing a threshold. Taking $X$ to be
20	the first $m$ indices asks for nothing beyond schedulability on $m$ machines, which is
21	how the table is read off at the end.
22
23	The recursion removes the smallest threshold $j$ of $X$ and decides whether job $j$ is
24	selected. If it is not, $j$ is replaced by the smallest index above it that is not
25	already a threshold — the paper's $j_1$ — and the table is consulted at the resulting
26	$X_1$ . If it is, the weight drops by $w_j$ and the budget by $p_j$ , and $j$ is replaced by
27	the smallest index not already a threshold whose second operation starts at or after
28	$d_j$ — the paper's $j_2$ — giving $X_2$ .
29
30	# Formalization Notes
31
32	The table is recorded as the predicate "a set of weight $W'$ compatible with $X$ can be
33	preprocessed starting from $P'$ " rather than as a value in $\mathbb{Z}$ extended by two
34	infinities. The predicate is downward closed in $P'$ , so it determines the value, and it
35	keeps the two infinities out of the statements: $-\infty$ is the predicate holding for no
36	$P'$ and $+\infty$ its holding for all of them, neither of which needs a name.
37
38	Compatibility is the paper's condition with the enumeration of machines removed. The
39	paper writes $X$ as a list $x_1 < \dots < x_m$ and assigns job $j$ to a machine index;
40	here a machine is its own threshold, so an assignment is a function into $X$ . The two
41	carry the same information, and the second needs no bookkeeping to keep the list sorted.
42
43	$j_1$ and $j_2$ are `Option`-valued, since the paper's definitions do not always produce
44	an index, and $X_1$ and $X_2$ drop the threshold without replacement when they do not.
45	The paper does not treat these cases; they are exactly the cases in which no machine is
46	left waiting for a job above the one just decided, and dropping the threshold is what
47	that means.
48
49	The budget $P'$ is an integer, as start times are, and the preprocessing condition is
50	stated from an arbitrary starting instant rather than from zero, which is what makes it
51	the quantity a backwards recursion carries.
52	-/
53
54	namespace Lax496464.DynamicProgram
55
56	open Lax496464.FlowShop Lax496464.FlowShop.Instance
57
58	variable (I : Instance)
59
60	/-- `Z` is compatible with `X`: every job of `Z` can be given a threshold in `X` not
61	exceeding it, no two conflicting jobs sharing a threshold. -/
62	def CompatibleWith (X Z : Finset I.Job) : Prop :=
63	∃ mach : I.Job → I.Job,
64	(∀ j ∈ Z, mach j ∈ X) ∧ (∀ j ∈ Z, mach j ≤ j) ∧
65	∀ i ∈ Z, ∀ j ∈ Z, i ≠ j → mach i = mach j → ¬ Conflict i j
66
67	/-- `Z` can be preprocessed from `P`: starting at the instant `P`, the first-stage
68	machine finishes each job of `Z` by the time its second operation must start. -/
69	def PreprocessableFrom (Z : Finset I.Job) (P : ℤ) : Prop :=
70	∀ j ∈ Z, P + ∑ i ∈ Z.filter (fun i => i ≤ j), (I.p i : ℤ) ≤ s j
71
72	/-- The table: a set of weight `W'` compatible with `X` can be preprocessed from `P'`.
73	The paper's `T[X, W']` is the largest `P'` for which this holds. -/
74	def Achievable (X : Finset I.Job) (W' : ℕ) (P' : ℤ) : Prop :=
75	∃ Z : Finset I.Job, weight I Z = W' ∧ CompatibleWith I X Z ∧ PreprocessableFrom I Z P'
76
77	/-- The paper's `j₁`: the smallest index above `j` that is not already a threshold. -/
78	noncomputable def j1 (X : Finset I.Job) (j : I.Job) : Option I.Job :=
79	letI := Classical.decPred fun x : I.Job => x ∉ X ∧ j < x
80	if h : (Finset.univ.filter fun x : I.Job => x ∉ X ∧ j < x).Nonempty then
81	some ((Finset.univ.filter fun x : I.Job => x ∉ X ∧ j < x).min' h) else none
82
83	/-- The paper's `j₂`: the smallest index that is not already a threshold and whose second
84	operation starts at or after `d j`. -/
85	noncomputable def j2 (X : Finset I.Job) (j : I.Job) : Option I.Job :=
86	letI := Classical.decPred fun x : I.Job => x ∉ X ∧ (I.d j : ℤ) ≤ s x
87	if h : (Finset.univ.filter fun x : I.Job => x ∉ X ∧ (I.d j : ℤ) ≤ s x).Nonempty then
88	some ((Finset.univ.filter fun x : I.Job => x ∉ X ∧ (I.d j : ℤ) ≤ s x).min' h) else none
89
90	/-- The paper's `X₁`: the thresholds after `j` is passed over. -/
91	noncomputable def X1 (X : Finset I.Job) (j : I.Job) : Finset I.Job :=
92	match j1 I X j with
93	\| some y => insert y (X.erase j)
94	\| none => X.erase j
95
96	/-- The paper's `X₂`: the thresholds after `j` is selected. -/
97	noncomputable def X2 (X : Finset I.Job) (j : I.Job) : Finset I.Job :=
98	match j2 I X j with
99	\| some y => insert y (X.erase j)
100	\| none => X.erase j
101
102	/-- The `m` smallest indices, the thresholds the table is read off at: a set compatible
103	with them is one that fits on `m` machines and nothing more. -/
104	def firstM : Finset I.Job := Finset.univ.filter fun i : I.Job => (i : ℕ) < I.machines
105
106	end Lax496464.DynamicProgram
107

Formalization Notes

The table is recorded as the predicate "a set of weight $W'$ compatible with $X$ can be preprocessed starting from $P'$ " rather than as a value in $\mathbb{Z}$ extended by two infinities. The predicate is downward closed in $P'$ , so it determines the value, and it keeps the two infinities out of the statements: $-\infty$ is the predicate holding for no $P'$ and $+\infty$ its holding for all of them, neither of which needs a name.

Compatibility is the paper's condition with the enumeration of machines removed. The paper writes $X$ as a list $x_1 < \dots < x_m$ and assigns job $j$ to a machine index; here a machine is its own threshold, so an assignment is a function into $X$ . The two carry the same information, and the second needs no bookkeeping to keep the list sorted.

$j_1$ and $j_2$ are $Option$ -valued, since the paper's definitions do not always produce an index, and $X_1$ and $X_2$ drop the threshold without replacement when they do not. The paper does not treat these cases; they are exactly the cases in which no machine is left waiting for a job above the one just decided, and dropping the threshold is what that means.

The budget $P'$ is an integer, as start times are, and the preprocessing condition is stated from an arbitrary starting instant rather than from zero, which is what makes it the quantity a backwards recursion carries.

Builds on

Lax496464.EstOrder

Used by

From Mathlib

Mathlib.Data.Finset.Max

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

The Dynamic Program of Section 3, and Its Table

Flags

Flag this concept

Natural Language Statement

Definition

In the paper

Lean source view on GitHub

Discussion

Settings

Your comments