The steps between objectives on words

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

proven

Loading review…

Natural Language Statement

Theorem

The zoo relates objectives by reductions of decision versions that change the objective data and the threshold: the makespan and the maximum lateness reduce to the number of late jobs and to the total tardiness, flow time to tardiness with due dates at the release dates, and completion time to flow time with the threshold lowered by the release dates ( $Thresholds$ ). On standard words such a step rewrites only the final block of release dates, weights and due dates and the threshold.

There are five modes. With the threshold $D$ , the release date $r_j$ , the weight $w_j$ and the due date $d_j$ of job $j$ :

Mode	Steps	New due date	New threshold
late, constant	$C_{\max} \to \sum U_j, \sum T_j$	$\max(D, 0)$	$-1$ if $D < 0$ , else $0$
late, shifted	$L_{\max} \to \sum U_j, \sum T_j$	$\max(d_j + D, 0)$	$-1$ if $n = 0$ and $D < 0$ or some $d_j + D < 0$ , else $0$
release	$\sum F_j \to \sum T_j$ , $\sum w_jF_j \to \sum w_jT_j$ , $F_{\max} \to L_{\max}$	$r_j$	$D$
shift	$\sum C_j \to \sum F_j$	$d_j$	$D - \sum_j r_j$
weighted shift	$\sum w_jC_j \to \sum w_jF_j$	$d_j$	$D - \sum_j w_j r_j$

The word map reads the number $n$ of jobs from the second number of the word and the threshold from its last two numbers, and rewrites the $3n$ numbers before the threshold; a word too short for this is left unchanged.

Theorem. The word map of every mode is computable in polynomial time on the word RAM. On the standard word of an instance $x$ of a specification of the operations family with the standard encoding and the source objective, with threshold $D$ , it writes the standard word of the stepped instance with the new threshold, which has the same answer.

Theorem. Consequently NP-hardness and strong NP-hardness go from the source objective to the target objective.

Concept map

60 concepts; 1 descendant hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

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

Lean source view on GitHub

Show types on hover

1	import Lax434175.StandardReading
2
3	/-!
4	---
5	title: The steps between objectives on words
6	type: theorem
7	---
8	The zoo relates objectives by reductions of decision versions that change the
9	objective data and the threshold: the makespan and the maximum lateness reduce to
10	the number of late jobs and to the total tardiness, flow time to tardiness with
11	due dates at the release dates, and completion time to flow time with the
12	threshold lowered by the release dates (`Thresholds`). On standard words such a
13	step rewrites only the final block of release dates, weights and due dates and
14	the threshold.
15
16	There are five modes. With the threshold $D$ , the release date $r_j$ , the weight
17	$w_j$ and the due date $d_j$ of job $j$ :
18
19	\| Mode \| Steps \| New due date \| New threshold \|
20	\|---\|---\|---\|---\|
21	\| late, constant \| $C_{\max} \to \sum U_j, \sum T_j$ \| $\max(D, 0)$ \| $-1$ if $D < 0$ , else $0$ \|
22	\| late, shifted \| $L_{\max} \to \sum U_j, \sum T_j$ \| $\max(d_j + D, 0)$ \| $-1$ if $n = 0$ and $D < 0$ or some $d_j + D < 0$ , else $0$ \|
23	\| release \| $\sum F_j \to \sum T_j$ , $\sum w_jF_j \to \sum w_jT_j$ , $F_{\max} \to L_{\max}$ \| $r_j$ \| $D$ \|
24	\| shift \| $\sum C_j \to \sum F_j$ \| $d_j$ \| $D - \sum_j r_j$ \|
25	\| weighted shift \| $\sum w_jC_j \to \sum w_jF_j$ \| $d_j$ \| $D - \sum_j w_j r_j$ \|
26
27	The word map reads the number $n$ of jobs from the second number of the word and
28	the threshold from its last two numbers, and rewrites the $3n$ numbers before the
29	threshold; a word too short for this is left unchanged.
30
31	Theorem. The word map of every mode is computable in polynomial time on the
32	word RAM. On the standard word of an instance $x$ of a specification of the
33	operations family with the standard encoding and the source objective, with
34	threshold $D$ , it writes the standard word of the stepped instance with the new
35	threshold, which has the same answer.
36
37	Theorem. Consequently NP-hardness and strong NP-hardness go from the source
38	objective to the target objective.
39	-/
40
41	namespace Lax434175.ThresholdWords
42	open Lax434175 Lax434175.Problems Lax434175.Assembly Lax434175.Results
43
44	/-- The modes of the steps. -/
45	inductive StepMode
46	\| lateConst
47	\| lateShift
48	\| toRelease
49	\| shift
50	\| weightedShift
51	deriving DecidableEq
52
53	/-- The step from one objective to another, if there is one. -/
54	def stepOf : Objectives.Value → Objectives.Value → Option StepMode
55	\| .makespan, .sumU \| .makespan, .sumT => some .lateConst
56	\| .lmax, .sumU \| .lmax, .sumT => some .lateShift
57	\| .sumF, .sumT \| .sumWF, .sumWT \| .fmax, .lmax => some .toRelease
58	\| .sumC, .sumF => some .shift
59	\| .sumWC, .sumWF => some .weightedShift
60	\| _, _ => none
61
62	/-- The threshold of the sign and the absolute value. -/
63	def readThr (neg a : ℕ) : ℤ := if neg = 0 then (a : ℤ) else -(a : ℤ)
64
65	/-- The threshold as sign and absolute value. -/
66	def thrWord (D : ℤ) : List ℕ := [if D < 0 then 1 else 0, D.natAbs]
67
68	/-- The new due date. -/
69	def newDue : StepMode → ℤ → ℕ → ℕ → ℕ
70	\| .lateConst, D, _, _ => D.toNat
71	\| .lateShift, D, _, d => ((d : ℤ) + D).toNat
72	\| .toRelease, _, r, _ => r
73	\| .shift, _, _, d => d
74	\| .weightedShift, _, _, d => d
75
76	open Classical in
77	/-- The new threshold. -/
78	noncomputable def newThr : StepMode → ℕ → ℤ → (ℕ → ℕ) → (ℕ → ℕ) → (ℕ → ℕ) → ℤ
79	\| .lateConst, _, D, _, _, _ => if D < 0 then -1 else 0
80	\| .lateShift, n, D, _, _, d =>
81	if (n = 0 ∧ D < 0) ∨ ∃ j < n, (d j : ℤ) + D < 0 then -1 else 0
82	\| .toRelease, _, D, _, _, _ => D
83	\| .shift, n, D, r, _, _ => D - ∑ j ∈ Finset.range n, (r j : ℤ)
84	\| .weightedShift, n, D, r, w, _ => D - ∑ j ∈ Finset.range n, (w j : ℤ) * (r j : ℤ)
85
86	open Classical in
87	/-- The word map of a mode. -/
88	noncomputable def stepWord (mode : StepMode) (u : List ℕ) : List ℕ :=
89	if u.length < 3 * u.getD 1 0 + 2 then u else
90	let n := u.getD 1 0
91	let base := u.length - 2 - 3 * n
92	let D := readThr (u.getD (u.length - 2) 0) (u.getD (u.length - 1) 0)
93	let r := fun j => u.getD (base + 3 * j) 0
94	let w := fun j => u.getD (base + 3 * j + 1) 0
95	let d := fun j => u.getD (base + 3 * j + 2) 0
96	u.take base ++ (List.ofFn fun j : Fin n => [r j, w j, newDue mode D (r j) (d j)]).flatten ++
97	thrWord (newThr mode n D r w d)
98
99	axiom stepWord_polytime (mode : StepMode) : Lax759944.RamPolytime.RamPolytime (stepWord mode)
100
101	variable {values : (i : OperationsFamily.FieldName) → (OperationsFamily.family.module i).Value}
102
103	axiom stepWord_correct (hs : values .encoding = .standard) {o o' : Objectives.Value}
104	{mode : StepMode} (hm : stepOf o o' = some mode) {u : List ℕ}
105	{x : Inst OperationsFamily.family (Thresholds.withObjective values o)} {D : ℤ}
106	(hx : EncodesDecision (StandardReading.ops.at (Thresholds.withObjective values o)) u x D) :
107	∃ y D', EncodesDecision (StandardReading.ops.at (Thresholds.withObjective values o'))
108	(stepWord mode u) y D' ∧
109	((problem _ (Thresholds.withObjective values o)).Decides x D ↔
110	(problem _ (Thresholds.withObjective values o')).Decides y D')
111
112	axiom npHard_step (hs : values .encoding = .standard) {o o' : Objectives.Value} {mode : StepMode}
113	(hm : stepOf o o' = some mode) :
114	NPHard (StandardReading.ops.at (Thresholds.withObjective values o)) →
115	NPHard (StandardReading.ops.at (Thresholds.withObjective values o'))
116
117	axiom stronglyNPHard_step (hs : values .encoding = .standard) {o o' : Objectives.Value}
118	{mode : StepMode} (hm : stepOf o o' = some mode) :
119	StronglyNPHard (StandardReading.ops.at (Thresholds.withObjective values o)) →
120	StronglyNPHard (StandardReading.ops.at (Thresholds.withObjective values o'))
121
122	end Lax434175.ThresholdWords
123

Show ProofShow ProofShow ProofShow Proof

Builds on

Lax434175.StandardReading

Used by

Lax434175.ThresholdParams

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 steps between objectives on words

Flags

Flag this concept

Natural Language Statement

Theorem

1 `npHard_step` proven

2 `stepWord_correct` proven

3 `stepWord_polytime` proven

4 `stronglyNPHard_step` proven

Lean source view on GitHub

Discussion

Settings

Your comments

The steps between objectives on words

Natural Language Statement

Theorem

1 npHard_step proven

2 stepWord_correct proven

3 stepWord_polytime proven

4 stronglyNPHard_step proven

Lean source view on GitHub

Discussion

1 `npHard_step` proven

2 `stepWord_correct` proven

3 `stepWord_polytime` proven

4 `stronglyNPHard_step` proven