Batch scheduling on a single machine

Lax434175.Batching · concepts/Lax434175/Batching.lean · lax-434175

proven

Loading review…

Natural Language Statement

Theorem

An instance has $n$ jobs with processing times $p_j$ and a setup time $s$ . A schedule partitions the jobs into batches, numbered in the order in which they are processed, and assigns a start time to every batch. All jobs of a batch start when the batch starts and complete when the batch completes.

There are two modes. In serial batching the processing time of a batch is the sum of the processing times of its jobs; in parallel batching it is their maximum.

A schedule is feasible for the kernel if a setup precedes every batch: a batch starts no earlier than time $s$ , and no earlier than $s$ time units after the completion of every batch with a smaller number.

The capacity field has the values

unbounded: a batch may contain any number of jobs;
bounded: a number $b$ is given, and a batch contains at most $b$ jobs;
sizes: a number $b$ and a size for every job are given, and the sizes of the jobs of a batch sum to at most $b$ .

Unbounded is the special case $b = n$ of bounded, and bounded the special case of sizes in which every job has size $1$ .

The processing-time field restricts the instances to unit or to equal processing times.

Theorem. In both modes the capacity field and the processing-time field are sound.

Concept map

3 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

Evidence

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

1 `capacity_sound` proven

no assumptions

thm✓Lax434175.Batching (1st statement)

⊢Lax434175Proofs.Batching.capacity_sound

2 `processingTimes_sound` proven

no assumptions

thm✓Lax434175.Batching (2nd statement)

⊢Lax434175Proofs.Batching.processingTimes_sound

Lean source view on GitHub

Show types on hover

1	import Mathlib.Algebra.BigOperators.Group.Finset.Basic
2	import Mathlib.Data.Finset.Lattice.Fold
3	import Mathlib.Data.Fintype.BigOperators
4	import Mathlib.Data.NNRat.Defs
5	import Lax434175.Modules
6
7	/-!
8	---
9	title: Batch scheduling on a single machine
10	type: theorem
11	---
12	An instance has $n$ jobs with processing times $p_j$ and a setup time $s$ . A
13	schedule partitions the jobs into batches, numbered in the order in which
14	they are processed, and assigns a start time to every batch. All jobs of a
15	batch start when the batch starts and complete when the batch completes.
16
17	There are two modes. In serial batching the processing time of a batch is
18	the sum of the processing times of its jobs; in parallel batching it is
19	their maximum.
20
21	A schedule is feasible for the kernel if a setup precedes every batch: a
22	batch starts no earlier than time $s$ , and no earlier than $s$ time units
23	after the completion of every batch with a smaller number.
24
25	The capacity field has the values
26
27	- unbounded: a batch may contain any number of jobs;
28	- bounded: a number $b$ is given, and a batch contains at most $b$ jobs;
29	- sizes: a number $b$ and a size for every job are given, and the sizes of
30	the jobs of a batch sum to at most $b$ .
31
32	Unbounded is the special case $b = n$ of bounded, and bounded the special
33	case of sizes in which every job has size $1$ .
34
35	The processing-time field restricts the instances to unit or to equal
36	processing times.
37
38	Theorem. In both modes the capacity field and the processing-time field
39	are sound.
40	-/
41
42	namespace Lax434175.Batching
43	open Lax434175.Kernels Lax434175.Modules
44
45	structure Inst where
46	jobs : ℕ
47	p : Fin jobs → ℕ
48	/-- The release date of a job. -/
49	r : Fin jobs → ℕ
50	/-- The setup time before every batch. -/
51	setup : ℕ
52
53	inductive Mode
54	\| serial
55	\| parallel
56
57	structure Sched (x : Inst) where
58	/-- The number of the batch of a job. -/
59	batch : Fin x.jobs → ℕ
60	/-- The start time of a batch. -/
61	start : ℕ → ℕ
62
63	/-- The jobs of a batch. -/
64	def members {x : Inst} (σ : Sched x) (k : ℕ) : Finset (Fin x.jobs) :=
65	Finset.univ.filter (fun j => σ.batch j = k)
66
67	/-- The processing time of a batch. -/
68	def length (mode : Mode) (x : Inst) (σ : Sched x) (k : ℕ) : ℕ :=
69	match mode with
70	\| .serial => ∑ j ∈ members σ k, x.p j
71	\| .parallel => (members σ k).sup x.p
72
73	/-- The completion time of a batch. -/
74	def finish (mode : Mode) (x : Inst) (σ : Sched x) (k : ℕ) : ℕ :=
75	σ.start k + length mode x σ k
76
77	/-- A setup precedes every batch. -/
78	def feasible (mode : Mode) (x : Inst) (σ : Sched x) : Prop :=
79	(∀ j, x.setup ≤ σ.start (σ.batch j)) ∧
80	∀ i j, σ.batch i < σ.batch j →
81	finish mode x σ (σ.batch i) + x.setup ≤ σ.start (σ.batch j)
82
83	/-- The kernel of batch scheduling in a mode. -/
84	def kernel (mode : Mode) : Kernel where
85	Inst := Inst
86	jobs := Inst.jobs
87	release := Inst.r
88	Sched := Sched
89	feasible := feasible mode
90	start _ σ j := (σ.start (σ.batch j) : NNRat)
91	completion x σ j := (finish mode x σ (σ.batch j) : NNRat)
92
93	inductive Capacity
94	\| unbounded
95	\| bounded
96	\| sizes
97
98	/-- The data of a capacity value. -/
99	def Capacity.Data : Capacity → Inst → Type
100	\| .unbounded, _ => Unit
101	\| .bounded, _ => ℕ
102	\| .sizes, x => ℕ × (Fin x.jobs → ℕ)
103
104	/-- The capacity of a batch; the number of jobs when unbounded. -/
105	def Capacity.bound {x : Inst} : (v : Capacity) → v.Data x → ℕ
106	\| .unbounded, _ => x.jobs
107	\| .bounded, b => b
108	\| .sizes, d => d.1
109
110	/-- The size of a job; `1` without sizes. -/
111	def Capacity.size {x : Inst} : (v : Capacity) → v.Data x → Fin x.jobs → ℕ
112	\| .unbounded, _ => fun _ => 1
113	\| .bounded, _ => fun _ => 1
114	\| .sizes, d => d.2
115
116	def Capacity.le : Capacity → Capacity → Bool
117	\| .unbounded, _ => true
118	\| .bounded, .unbounded => false
119	\| .bounded, _ => true
120	\| .sizes, .sizes => true
121	\| .sizes, _ => false
122
123	def Capacity.embed : {v w : Capacity} → Capacity.le v w = true → (x : Inst) →
124	v.Data x → w.Data x
125	\| _, .unbounded, _, _, _ => ()
126	\| v, .bounded, _, _, d => v.bound d
127	\| v, .sizes, _, _, d => (v.bound d, v.size d)
128
129	/-- The capacity field. -/
130	def capacity (mode : Mode) : Module (kernel mode) where
131	Value := Capacity
132	Data := Capacity.Data
133	admits _ _ _ := True
134	constraint v _ d σ := ∀ k, ∑ j ∈ members σ k, v.size d j ≤ v.bound d
135	le := Capacity.le
136	embed := Capacity.embed
137
138	inductive ProcessingTimes
139	\| unit
140	\| equal
141	\| arbitrary
142
143	/-- The instances of a processing-time restriction. -/
144	def ProcessingTimes.holds : ProcessingTimes → Inst → Prop
145	\| .unit, x => ∀ j, x.p j = 1
146	\| .equal, x => ∃ p, ∀ j, x.p j = p
147	\| .arbitrary, _ => True
148
149	/-- The position of a value in the chain unit, equal, arbitrary. -/
150	def ProcessingTimes.rank : ProcessingTimes → ℕ
151	\| .unit => 0
152	\| .equal => 1
153	\| .arbitrary => 2
154
155	/-- The processing-time field. -/
156	def processingTimes (mode : Mode) : Module (kernel mode) :=
157	Module.ofRestriction ProcessingTimes ProcessingTimes.holds
158	(fun v w => decide (v.rank ≤ w.rank))
159
160	axiom capacity_sound (mode : Mode) : (capacity mode).Sound
161
162	axiom processingTimes_sound (mode : Mode) : (processingTimes mode).Sound
163
164	end Lax434175.Batching
165

Show ProofShow Proof

Builds on

Lax434175.Modules

Used by

Lax434175.BatchProblems

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

Batch scheduling on a single machine

Flags

Flag this concept

Natural Language Statement

Theorem

1 `capacity_sound` proven

2 `processingTimes_sound` proven

Lean source view on GitHub

Discussion

Settings

Your comments

Batch scheduling on a single machine

Natural Language Statement

Theorem

1 capacity_sound proven

2 processingTimes_sound proven

Lean source view on GitHub

Discussion

1 `capacity_sound` proven

2 `processingTimes_sound` proven