Single machine scheduling with release times and deadlines

Lax391470.Scheduling · concepts/Lax391470/Scheduling.lean · lax-391470

definition

Loading review…

Natural Language Statement

Definition

An instance consists of $n$ jobs to be run on a single machine. Job $i$ has a release time $r_i \in \mathbb{Z}$ , a deadline $d_i \in \mathbb{Z}$ and a processing time $p_i \in \mathbb{N}$ ; the interval $[r_i, d_i]$ is its availability interval. A schedule assigns a start time $t(i)$ to every job. It is feasible if $r_i \le t(i) \le d_i - p_i$ for every job and the execution intervals $[t(i),\, t(i) + p_i)$ are pairwise disjoint: no job starts before its release time, no job completes after its deadline, no job is interrupted, and no two jobs run at the same time. The decision problem, written $1 \mid r_j \mid L_{\max}$ in the three-field notation, asks whether a feasible schedule exists — equivalently, whether the maximum lateness can be made non-positive.

The problem is parameterized by the set of processing times its jobs may have. An instance is on the lengths $\{p, q\}$ if every processing time is $p$ or $q$ .

Concept map

1 concept; 8 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

1	import Mathlib.Data.Real.Basic
2
3	/-!
4	---
5	title: Single machine scheduling with release times and deadlines
6	type: definition
7	---
8	An instance consists of $n$ jobs to be run on a single machine. Job $i$ has a release
9	time $r_i \in \mathbb{Z}$ , a deadline $d_i \in \mathbb{Z}$ and a processing time
10	$p_i \in \mathbb{N}$ ; the interval $[r_i, d_i]$ is its availability interval. A
11	schedule assigns a start time $t(i)$ to every job. It is feasible if
12	$r_i \le t(i) \le d_i - p_i$ for every job and the execution intervals
13	$[t(i),\, t(i) + p_i)$ are pairwise disjoint: no job starts before its release time, no
14	job completes after its deadline, no job is interrupted, and no two jobs run at the same
15	time. The decision problem, written $1 \mid r_j \mid L_{\max}$ in the three-field
16	notation, asks whether a feasible schedule exists — equivalently, whether the maximum
17	lateness can be made non-positive.
18
19	The problem is parameterized by the set of processing times its jobs may have. An
20	instance is on the lengths $\{p, q\}$ if every processing time is $p$ or $q$ .
21
22	# Formalization notes
23
24	Jobs are `Fin n` rather than an abstract finite type: an instance is something a machine
25	is handed as a word, and a word presents its jobs in an order.
26
27	Start times are integers. The source allows real start times; since all data are
28	integral this changes nothing, and that it changes nothing is a statement of this
29	submission rather than a convention of this file. Both readings are therefore defined
30	here, the real one only so that their equivalence can be stated.
31
32	Disjointness of two execution intervals is written as the arithmetic condition that one
33	job completes before the other starts. For jobs of positive processing time the two
34	formulations agree, and every statement of this submission concerns lengths
35	$p > q \ge 1$ . A job of processing time zero is not excluded by the structure, because
36	excluding it would put a proof obligation into every construction; it plays no role.
37	-/
38
39	namespace Lax391470.Scheduling
40
41	/-- An instance of single machine scheduling with release times and deadlines: `jobs`
42	jobs, each with a release time, a deadline and a processing time. -/
43	structure Instance where
44	/-- The number `n` of jobs. -/
45	jobs : ℕ
46	/-- The release time `r i` of job `i`. -/
47	r : Fin jobs → ℤ
48	/-- The deadline `d i` of job `i`. -/
49	d : Fin jobs → ℤ
50	/-- The processing time `p i` of job `i`. -/
51	p : Fin jobs → ℕ
52
53	namespace Instance
54
55	variable (I : Instance)
56
57	/-- A schedule assigns a start time to every job. -/
58	abbrev Schedule := Fin I.jobs → ℤ
59
60	variable {I}
61
62	/-- A schedule is feasible if every job runs inside its availability interval and no two
63	jobs run at the same time. -/
64	def Feasible (t : I.Schedule) : Prop :=
65	(∀ i, I.r i ≤ t i ∧ t i + I.p i ≤ I.d i) ∧
66	(∀ i j, i ≠ j → t i + I.p i ≤ t j ∨ t j + I.p j ≤ t i)
67
68	/-- The same condition for a schedule with real start times. -/
69	def RealFeasible (t : Fin I.jobs → ℝ) : Prop :=
70	(∀ i, (I.r i : ℝ) ≤ t i ∧ t i + I.p i ≤ I.d i) ∧
71	(∀ i j, i ≠ j → t i + I.p i ≤ t j ∨ t j + I.p j ≤ t i)
72
73	variable (I)
74
75	/-- `I` admits a feasible schedule. -/
76	def Schedulable : Prop := ∃ t : I.Schedule, Feasible t
77
78	/-- `I` admits a feasible schedule with real start times. -/
79	def RealSchedulable : Prop := ∃ t : Fin I.jobs → ℝ, RealFeasible t
80
81	/-- Every processing time of `I` is `p` or `q`. -/
82	def LengthsIn (p q : ℕ) : Prop := ∀ i, I.p i = p ∨ I.p i = q
83
84	end Instance
85
86	end Lax391470.Scheduling
87

Formalization notes

Jobs are $Fin n$ rather than an abstract finite type: an instance is something a machine is handed as a word, and a word presents its jobs in an order.

Start times are integers. The source allows real start times; since all data are integral this changes nothing, and that it changes nothing is a statement of this submission rather than a convention of this file. Both readings are therefore defined here, the real one only so that their equivalence can be stated.

Disjointness of two execution intervals is written as the arithmetic condition that one job completes before the other starts. For jobs of positive processing time the two formulations agree, and every statement of this submission concerns lengths $p > q \ge 1$ . A job of processing time zero is not excluded by the structure, because excluding it would put a proof obligation into every construction; it plays no role.

Builds on

none

Used by

From Mathlib

Mathlib.Data.Real.Basic

Discussion

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

Loading discussion…

Lax Lean Archive

Single machine scheduling with release times and deadlines

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments