The dynamic program for interval scheduling, and its state space

Lax470956.DynamicProgram · concepts/Lax470956/DynamicProgram.lean · lax-470956

proven

Loading review…

Natural Language Statement

Definition

The algorithm behind the third theorem. It sweeps the time axis, carrying at each instant a state — which job, if any, occupies each machine — and the best total weight of the jobs started so far that is consistent with that state. A state at time $t+1$ may follow a state at time $t$ when every job still running continues on its own machine and every job appearing at $t+1$ that had already started was already there.

Writing $\mathrm{opt}_t(s)$ for the best weight of jobs started by time $t$ over the feasible schedules whose occupancy at $t$ is exactly $s$ , the recursion is

\mathrm{dp}_{t+1}(s') = \max_{s \to s'} \mathrm{dp}_t(s) + \mathrm{fresh}_{t+1}(s'),

with $\mathrm{dp}_0(s)$ the weight of the jobs $s$ starts. At the horizon every machine is idle and the value is the optimum of the instance.

The number of states at any instant is at most $(a_t+1)^m$ , where $a_t$ is the number of jobs alive then: a state chooses, for each of the $m$ machines, one job alive at $t$ or nothing. This is where fixed-parameter tractability comes from — the table is indexed by the parameter, not by the instance — and it is why the preprocessing step, which bounds $a_t$ by a function of $m$ and $p_{\max}$ alone, completes the argument.

Concept map

2 concepts; 1 descendant hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

This concept declares 3 statements. Each proof establishes one of them relative to its assumptions.

Lean source view on GitHub

1	import Lax470956.Scheduling
2	import Mathlib.Algebra.Order.Monoid.WithTop
3
4	/-!
5	---
6	title: The dynamic program for interval scheduling, and its state space
7	type: definition
8	---
9	The algorithm behind the third theorem. It sweeps the time axis, carrying at each
10	instant a state — which job, if any, occupies each machine — and the best total weight
11	of the jobs started so far that is consistent with that state. A state at time $t+1$ may
12	follow a state at time $t$ when every job still running continues on its own machine and
13	every job appearing at $t+1$ that had already started was already there.
14
15	Writing $\mathrm{opt}_t(s)$ for the best weight of jobs started by time $t$ over the
16	feasible schedules whose occupancy at $t$ is exactly $s$ , the recursion is
17	$\mathrm{dp}_{t+1}(s') = \max_{s \to s'} \mathrm{dp}_t(s) + \mathrm{fresh}_{t+1}(s'),$
18	with $\mathrm{dp}_0(s)$ the weight of the jobs $s$ starts. At the horizon every machine
19	is idle and the value is the optimum of the instance.
20
21	The number of states at any instant is at most $(a_t+1)^m$ , where $a_t$ is the number of
22	jobs alive then: a state chooses, for each of the $m$ machines, one job alive at $t$ or
23	nothing. This is where fixed-parameter tractability comes from — the table is indexed by
24	the parameter, not by the instance — and it is why the preprocessing step, which bounds
25	$a_t$ by a function of $m$ and $p_{\max}$ alone, completes the argument.
26
27	# Formalization notes
28
29	A state is a total function from machines to `Option` jobs, so a machine is idle exactly
30	when it is mapped to `none`. Defining it as a partial injection would be closer to the
31	intent and further from what a table is indexed by; the injectivity that an occupancy
32	has is a clause of `ValidState` instead.
33
34	The value of the table is `WithBot ℕ` rather than `ℕ`, with `⊥` for a state no feasible
35	schedule realizes. The distinction is needed: a state of weight zero and a state that
36	cannot occur are different, and a maximum over an empty set of schedules has to be
37	smaller than every real value rather than equal to zero.
38
39	`dp` is a recursion on the time index and is computable, while `optAt` quantifies over
40	schedules and is not. They are separate definitions so that their agreement is a theorem.
41	That theorem is the paper's Lemma 6, and it justifies running the recursion in place of the
42	specification.
43
44	The state-space bound is stated as a cardinality of a `Finset` of states rather than as
45	an asymptotic count. It is an exact inequality, as a running-time argument needs.
46	-/
47
48	namespace Lax470956.DynamicProgram
49
50	open Lax470956.Scheduling Lax470956.Scheduling.Instance
51
52	variable (I : Instance)
53
54	/-- A snapshot of the machines at one instant: which job, if any, occupies each. -/
55	abbrev State : Type := Fin I.machines → Option (Fin I.jobs)
56
57	variable {I}
58
59	/-- Job `j` is running at time `t`, that is `t ∈ [d j - p j, d j)`. -/
60	def Active (t : ℕ) (j : Fin I.jobs) : Prop := I.start j ≤ t ∧ t < I.d j
61
62	instance (t : ℕ) (j : Fin I.jobs) : Decidable (Active t j) :=
63	inferInstanceAs (Decidable (_ ∧ _))
64
65	instance (j j' : Fin I.jobs) : Decidable (I.Overlap j j') :=
66	inferInstanceAs (Decidable (_ ∧ _))
67
68	instance (σ : I.Schedule) : Decidable (Feasible σ) :=
69	inferInstanceAs (Decidable (_ ∧ _))
70
71	variable (I)
72
73	/-- The value of an optimal schedule. -/
74	def optimum : ℕ := (Finset.univ.filter fun σ : I.Schedule => Feasible σ).sup weight
75
76	/-- The time horizon: every job has finished by then. -/
77	def horizon : ℕ := Finset.univ.sup I.d
78
79	/-- The total weight of the scheduled jobs that have started by time `t`. -/
80	def weightStarted (σ : I.Schedule) (t : ℕ) : ℕ :=
81	∑ j, if σ j ≠ none ∧ I.start j ≤ t then I.w j else 0
82
83	/-- The total weight of the jobs a state shows as beginning at time `t`. -/
84	def freshWeight (t : ℕ) (s : State I) : ℕ :=
85	∑ j, if (∃ i, s i = some j) ∧ I.start j = t then I.w j else 0
86
87	/-- A state that could be the machine occupancy at time `t`: every occupant is eligible
88	and active, and no job occupies two machines. -/
89	def ValidState (t : ℕ) (s : State I) : Prop :=
90	(∀ i j, s i = some j → i ∈ I.eligible j ∧ Active t j) ∧
91	(∀ i i' j, s i = some j → s i' = some j → i = i')
92
93	instance (t : ℕ) (s : State I) : Decidable (ValidState I t s) :=
94	inferInstanceAs (Decidable (_ ∧ _))
95
96	/-- The transition relation: state `s` at time `t` may be followed by state `s'` at time
97	`t + 1`. A job still running continues on its machine, and a job appearing at `t + 1`
98	that had already started must have been there at `t`. -/
99	def Step (t : ℕ) (s s' : State I) : Prop :=
100	ValidState I (t + 1) s' ∧
101	(∀ i j, s i = some j → t + 1 < I.d j → s' i = some j) ∧
102	(∀ i j, s' i = some j → I.start j ≤ t → s i = some j)
103
104	instance (t : ℕ) (s s' : State I) : Decidable (Step I t s s') :=
105	inferInstanceAs (Decidable (_ ∧ _))
106
107	variable {I}
108
109	/-- The machine occupancy at time `t` of the schedule `σ`. -/
110	noncomputable def runOf (σ : I.Schedule) (t : ℕ) : State I := fun i =>
111	if h : ∃ j, σ j = some i ∧ Active t j then some h.choose else none
112
113	variable (I)
114
115	/-- The best total weight of jobs started by time `t`, over the feasible schedules whose
116	machine occupancy at time `t` is exactly `s`. `⊥` when there is no such schedule. -/
117	noncomputable def optAt (t : ℕ) (s : State I) : WithBot ℕ :=
118	open Classical in
119	(Finset.univ.filter fun σ : I.Schedule => Feasible σ ∧ runOf σ t = s).sup
120	fun σ => (weightStarted I σ t : WithBot ℕ)
121
122	/-- The dynamic program. A recursion on the time index: the value of a state at
123	`t + 1` is the best value of a predecessor, plus the weight of the jobs beginning then. -/
124	def dp : ℕ → State I → WithBot ℕ
125	\| 0, s => if ValidState I 0 s then (freshWeight I 0 s : WithBot ℕ) else ⊥
126	\| t + 1, s' =>
127	((Finset.univ.filter fun s => Step I t s s').sup fun s => dp t s)
128	+ (freshWeight I (t + 1) s' : WithBot ℕ)
129
130	/-- The value the algorithm returns: the table at the horizon, with every machine idle. -/
131	def solve : WithBot ℕ := dp I (horizon I) fun _ => none
132
133	/-- The number of jobs alive at time `t`. -/
134	def aliveCount (t : ℕ) : ℕ := (Finset.univ.filter fun j => Active (I := I) t j).card
135
136	/-- Lemma 6. The recursion computes the specification: at every instant and every
137	state, the dynamic program's value is the best weight of jobs started by then over the
138	feasible schedules with that occupancy. -/
139	axiom dp_eq_optAt (I : Instance) (t : ℕ) (s : State I) : dp I t s = optAt I t s
140
141	/-- Theorem 3, algorithmic half. The dynamic program returns the optimum of the
142	instance. -/
143	axiom solve_eq_optimum (I : Instance) : solve I = (optimum I : WithBot ℕ)
144
145	/-- The state-space bound. At any instant there are at most `(a_t + 1) ^ m` valid
146	states, where `a_t` is the number of jobs alive then. -/
147	axiom card_validState_le (I : Instance) (t : ℕ) :
148	(Finset.univ.filter fun s : State I => ValidState I t s).card
149	≤ (aliveCount I t + 1) ^ I.machines
150
151	end Lax470956.DynamicProgram
152

Show ProofShow ProofShow Proof

Formalization notes

A state is a total function from machines to $Option$ jobs, so a machine is idle exactly when it is mapped to $none$ . Defining it as a partial injection would be closer to the intent and further from what a table is indexed by; the injectivity that an occupancy has is a clause of $ValidState$ instead.

The value of the table is $WithBot ℕ$ rather than $ℕ$ , with $⊥$ for a state no feasible schedule realizes. The distinction is needed: a state of weight zero and a state that cannot occur are different, and a maximum over an empty set of schedules has to be smaller than every real value rather than equal to zero.

$dp$ is a recursion on the time index and is computable, while $optAt$ quantifies over schedules and is not. They are separate definitions so that their agreement is a theorem. That theorem is the paper's Lemma 6, and it justifies running the recursion in place of the specification.

The state-space bound is stated as a cardinality of a $Finset$ of states rather than as an asymptotic count. It is an exact inequality, as a running-time argument needs.

Builds on

Lax470956.Scheduling

Used by

Lax470956.Preprocessing

From Mathlib

Mathlib.Algebra.Order.Monoid.WithTop

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 for interval scheduling, and its state space

Flags

Flag this concept

Natural Language Statement

Definition

1 `card_validState_le` proven

2 `dp_eq_optAt` proven

3 `solve_eq_optimum` proven

Lean source view on GitHub

Discussion

Settings

Your comments

The dynamic program for interval scheduling, and its state space

Natural Language Statement

Definition

1 card_validState_le proven

2 dp_eq_optAt proven

3 solve_eq_optimum proven

Lean source view on GitHub

Discussion

1 `card_validState_le` proven

2 `dp_eq_optAt` proven

3 `solve_eq_optimum` proven