The auxiliary problem AUX(p, q)

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

definition

Loading review…

Natural Language Statement

Definition

The intermediate problem through which the hardness proof passes. Fix two job lengths $p > q$ . An instance consists of a set $J$ of ordinary jobs, each long (of length $p$ ) or short (of length $q$ ), with non-negative release times and deadlines, together with two sequences $J_p$ and $J_q$ of $N$ pending jobs each. The pending jobs of $J_p$ are long and those of $J_q$ are short. Every pending job is released at time $0$ and carries two deadlines: an early deadline $d'$ and a late deadline $d$ . The deadlines satisfy

d'_{p,1} \le d_{p,1} \le d'_{p,2} \le d_{p,2} \le \dots \le d'_{p,N} \le d_{p,N},

d'_{q,1} \le d_{q,1} \le d'_{q,2} \le d_{q,2} \le \dots \le d'_{q,N} \le d_{q,N},

d_{p,i} \le d'_{q,i} \quad\text{for all } i = 1, \dots, N.

The pending jobs $J_{p,i}$ and $J_{q,i}$ are connected. The question is whether $J \cup J_p \cup J_q$ has a feasible schedule, every job meeting its late deadline, in which for every $i$ at least one of $J_{p,i}$ and $J_{q,i}$ completes by its early deadline.

A connected pair is a disjunction between two jobs that may sit anywhere on the time line, which is what lets the problem express the clauses of a formula.

Concept map

2 concepts; 6 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

1	import Lax391470.Scheduling
2
3	/-!
4	---
5	title: The auxiliary problem AUX(p, q)
6	type: definition
7	---
8	The intermediate problem through which the hardness proof passes. Fix two job lengths
9	$p > q$ . An instance consists of a set $J$ of ordinary jobs, each long (of length $p$ )
10	or short (of length $q$ ), with non-negative release times and deadlines, together with
11	two sequences $J_p$ and $J_q$ of $N$ pending jobs each. The pending jobs of $J_p$ are
12	long and those of $J_q$ are short. Every pending job is released at time $0$ and carries
13	two deadlines: an early deadline $d'$ and a late deadline $d$ . The deadlines satisfy
14	$d'_{p,1} \le d_{p,1} \le d'_{p,2} \le d_{p,2} \le \dots \le d'_{p,N} \le d_{p,N},$
15	$d'_{q,1} \le d_{q,1} \le d'_{q,2} \le d_{q,2} \le \dots \le d'_{q,N} \le d_{q,N},$
16	$d_{p,i} \le d'_{q,i} \quad\text{for all } i = 1, \dots, N.$
17	The pending jobs $J_{p,i}$ and $J_{q,i}$ are connected. The question is whether
18	$J \cup J_p \cup J_q$ has a feasible schedule, every job meeting its late deadline, in
19	which for every $i$ at least one of $J_{p,i}$ and $J_{q,i}$ completes by its early
20	deadline.
21
22	A connected pair is a disjunction between two jobs that may sit anywhere on the time
23	line, which is what lets the problem express the clauses of a formula.
24
25	# Formalization notes
26
27	An instance is data only; the three chains of inequalities are the separate predicate
28	`Ordered`. A construction can then be written down without proof obligations, and that
29	its output is ordered becomes a statement about it.
30
31	The job lengths $p$ and $q$ are not part of an instance. An ordinary job records only
32	whether it is long, and the lengths enter where the instance is read as a scheduling
33	instance. The problem is thereby one family of instances interpreted at each pair of
34	lengths, as the notation $\mathrm{AUX}(p, q)$ suggests.
35
36	All times of an instance are natural numbers: the source requires the ordinary jobs'
37	release times and deadlines to be non-negative, and a pending job, released at $0$ , could
38	not meet a negative deadline.
39
40	Forgetting the early deadlines gives an ordinary scheduling instance, `toInstance`, whose
41	jobs are the ordinary jobs, then the long pending jobs, then the short ones. A solution
42	is a feasible schedule of that instance satisfying the condition on connected pairs.
43	-/
44
45	namespace Lax391470.AuxiliaryProblem
46
47	open Lax391470.Scheduling
48
49	/-- The data of an instance of `AUX(p, q)`: ordinary jobs, each long or short, and
50	`pairs` connected pairs of pending jobs with an early and a late deadline each. -/
51	structure Instance where
52	/-- The number of ordinary jobs. -/
53	ordinary : ℕ
54	/-- The release time of an ordinary job. -/
55	r : Fin ordinary → ℕ
56	/-- The deadline of an ordinary job. -/
57	d : Fin ordinary → ℕ
58	/-- Whether an ordinary job is long (of length `p`) rather than short (of length `q`). -/
59	long : Fin ordinary → Bool
60	/-- The number `N` of connected pairs of pending jobs. -/
61	pairs : ℕ
62	/-- The early deadline `d'_{p,i}` of the `i`-th long pending job. -/
63	longEarly : Fin pairs → ℕ
64	/-- The late deadline `d_{p,i}` of the `i`-th long pending job. -/
65	longDue : Fin pairs → ℕ
66	/-- The early deadline `d'_{q,i}` of the `i`-th short pending job. -/
67	shortEarly : Fin pairs → ℕ
68	/-- The late deadline `d_{q,i}` of the `i`-th short pending job. -/
69	shortDue : Fin pairs → ℕ
70
71	namespace Instance
72
73	variable (A : Instance)
74
75	/-- The conditions on the deadlines of the pending jobs: within each sequence the
76	intervals between early and late deadline are ordered and do not intersect, and in every
77	connected pair the long job is the more urgent. -/
78	structure Ordered : Prop where
79	/-- `d'_{p,i} ≤ d_{p,i}`. -/
80	longEarly_le : ∀ i, A.longEarly i ≤ A.longDue i
81	/-- `d_{p,i} ≤ d'_{p,i+1}`. -/
82	longDue_le : ∀ i j : Fin A.pairs, (i : ℕ) + 1 = j → A.longDue i ≤ A.longEarly j
83	/-- `d'_{q,i} ≤ d_{q,i}`. -/
84	shortEarly_le : ∀ i, A.shortEarly i ≤ A.shortDue i
85	/-- `d_{q,i} ≤ d'_{q,i+1}`. -/
86	shortDue_le : ∀ i j : Fin A.pairs, (i : ℕ) + 1 = j → A.shortDue i ≤ A.shortEarly j
87	/-- `d_{p,i} ≤ d'_{q,i}`. -/
88	longDue_le_shortEarly : ∀ i, A.longDue i ≤ A.shortEarly i
89
90	/-- The scheduling instance underlying `A` at the job lengths `p` and `q`: the ordinary
91	jobs, then the long pending jobs, then the short pending jobs, the pending jobs released
92	at `0` and due at their late deadlines. -/
93	def toInstance (p q : ℕ) : Scheduling.Instance where
94	jobs := A.ordinary + A.pairs + A.pairs
95	r j := if h : (j : ℕ) < A.ordinary then A.r ⟨j, h⟩ else 0
96	d j :=
97	if h : (j : ℕ) < A.ordinary then A.d ⟨j, h⟩
98	else if h' : (j : ℕ) < A.ordinary + A.pairs then
99	A.longDue ⟨j - A.ordinary, by omega⟩
100	else A.shortDue ⟨j - A.ordinary - A.pairs, by have := j.isLt; omega⟩
101	p j :=
102	if h : (j : ℕ) < A.ordinary then (if A.long ⟨j, h⟩ then p else q)
103	else if (j : ℕ) < A.ordinary + A.pairs then p
104	else q
105
106	/-- The `i`-th long pending job, as a job of the underlying instance. -/
107	def longJob (p q : ℕ) (i : Fin A.pairs) : Fin (A.toInstance p q).jobs :=
108	⟨A.ordinary + i, by have := i.isLt; simp only [toInstance]; omega⟩
109
110	/-- The `i`-th short pending job, as a job of the underlying instance. -/
111	def shortJob (p q : ℕ) (i : Fin A.pairs) : Fin (A.toInstance p q).jobs :=
112	⟨A.ordinary + A.pairs + i, by have := i.isLt; simp only [toInstance]; omega⟩
113
114	variable {A}
115
116	/-- A schedule solves `A` at the lengths `p` and `q`: it is feasible, and in every
117	connected pair the long job completes by its early deadline or the short one does. -/
118	def Solves (p q : ℕ) (t : (A.toInstance p q).Schedule) : Prop :=
119	Scheduling.Instance.Feasible t ∧
120	∀ i : Fin A.pairs,
121	t (A.longJob p q i) + p ≤ A.longEarly i ∨ t (A.shortJob p q i) + q ≤ A.shortEarly i
122
123	variable (A)
124
125	/-- `A` has a solution at the lengths `p` and `q`. -/
126	def Solvable (p q : ℕ) : Prop := ∃ t, A.Solves p q t
127
128	end Instance
129
130	end Lax391470.AuxiliaryProblem
131

Formalization notes

An instance is data only; the three chains of inequalities are the separate predicate $Ordered$ . A construction can then be written down without proof obligations, and that its output is ordered becomes a statement about it.

The job lengths $p$ and $q$ are not part of an instance. An ordinary job records only whether it is long, and the lengths enter where the instance is read as a scheduling instance. The problem is thereby one family of instances interpreted at each pair of lengths, as the notation $\mathrm{AUX}(p, q)$ suggests.

All times of an instance are natural numbers: the source requires the ordinary jobs' release times and deadlines to be non-negative, and a pending job, released at $0$ , could not meet a negative deadline.

Forgetting the early deadlines gives an ordinary scheduling instance, $toInstance$ , whose jobs are the ordinary jobs, then the long pending jobs, then the short ones. A solution is a feasible schedule of that instance satisfying the condition on connected pairs.

Builds on

Lax391470.Scheduling

Used by

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

The auxiliary problem AUX(p, q)

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments