Three Days and the Fairness Parameter One
Lax117284.Theorem7 · concepts/Lax117284/Theorem7.lean · lax-117284
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Theorem 7. The problem is NP-hard for and .
Let be a [2,3]-bounded 3-SAT formula with variables, clauses of two literals and clauses of three literals. Build an instance with three days and the clients: three dummies; two clients per variable ; and one client per occurrence of a literal in a clause. Every processing time is , so two jobs of a day conflict exactly when their due dates differ by at most one, and the whole construction is a matter of placing due dates on a line, three times.
On the first day the due dates are for the three dummies, for both clients of variable , for both clients of the -th clause of two literals, and for all three clients of the -th clause of three literals. Clients sharing a due date conflict and nothing else does, so the first day admits one client out of each group: one dummy, one of — this is the truth assignment — and one client of every clause. On the second day the dummies, the variable clients and the clients of the clauses of two literals all have the due date , so they are pairwise conflicting, while the clients of the -th clause of three literals sit alone at ; since a dummy runs on every day, the second day is a dead end for everything but one client of each clause of three literals. On the third day sits at and at , while an occurrence of the literal sits at or and an occurrence of at or , according to which of its at most two occurrences it is. So on the third day a client of an occurrence conflicts with exactly the variable client that falsifies its literal, and with nothing else.
The three dummies conflict with each other on all three days, so a -fair schedule runs exactly one of them on each day. This is what forces the selection on the first day and makes the second day a dead end, and a client of an occurrence can then be served only on the third day — which is possible exactly when the assignment selected on the first day makes its literal true.
Concept map
Evidence
In the paper
- page 2 of this submission's paper
Lean source view on GitHub
| 1 | import Lax117284.BoundedSat |
| 2 | import Lax117284.Problems |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Three Days and the Fairness Parameter One |
| 7 | type: theorem |
| 8 | --- |
| 9 | **Theorem 7.** The problem |
| 10 | is NP-hard for and |
| 11 | . |
| 12 | |
| 13 | Let be a [2,3]-bounded 3-SAT formula with variables, clauses of two |
| 14 | literals and clauses of three literals. Build an instance with three days and the |
| 15 | clients: three *dummies*; two clients per variable ; and one client per |
| 16 | occurrence of a literal in a clause. Every processing time is , so two jobs of a day |
| 17 | conflict exactly when their due dates differ by at most one, and the whole construction is a |
| 18 | matter of placing due dates on a line, three times. |
| 19 | |
| 20 | On the first day the due dates are for the three dummies, for both clients of |
| 21 | variable , for both clients of the -th clause of two literals, and |
| 22 | for all three clients of the -th clause of three literals. Clients |
| 23 | sharing a due date conflict and nothing else does, so the first day admits one client out of |
| 24 | each group: one dummy, one of — this is the truth assignment — and one |
| 25 | client of every clause. On the second day the dummies, the variable clients and the clients |
| 26 | of the clauses of two literals all have the due date , so they are pairwise conflicting, |
| 27 | while the clients of the -th clause of three literals sit alone at ; since a dummy |
| 28 | runs on every day, the second day is a dead end for everything but one client of each clause |
| 29 | of three literals. On the third day sits at and at , while |
| 30 | an occurrence of the literal sits at or and an occurrence of |
| 31 | at or , according to which of its at most two occurrences it is. So on the |
| 32 | third day a client of an occurrence conflicts with exactly the variable client that |
| 33 | *falsifies* its literal, and with nothing else. |
| 34 | |
| 35 | The three dummies conflict with each other on all three days, so a -fair schedule runs |
| 36 | exactly one of them on each day. This is what forces the selection on the first day and |
| 37 | makes the second day a dead end, and a client of an occurrence can then be served only on |
| 38 | the third day — which is possible exactly when the assignment selected on the first day |
| 39 | makes its literal true. |
| 40 | |
| 41 | # Formalization Notes |
| 42 | |
| 43 | Clients are numbered: the dummies ; then the pair of variable ; |
| 44 | then one client per occurrence slot, those of the clauses of two literals first. Which of |
| 45 | the at most two occurrences of a literal a slot is, which the third day's layout needs, is |
| 46 | computed from the formula as the number of earlier slots carrying the same literal; it is |
| 47 | the occurrence bound that makes this or . |
| 48 | |
| 49 | The due dates are the source's with every index shifted, since the source numbers variables |
| 50 | and clauses from and these are numbered from . |
| 51 | |
| 52 | All processing times are equal, so the instance lies in the class of instances with |
| 53 | day-independent processing times, which is the restriction Theorem 2 concerns. |
| 54 | -/ |
| 55 | |
| 56 | namespace Lax117284.Theorem7 |
| 57 | |
| 58 | open Lax117284.Scheduling Lax117284.Problems Lax434930.PolynomialTime |
| 59 | open Lax429075.Reductions |
| 60 | |
| 61 | /-- The number of clients of the construction: three dummies, two per variable, and one per |
| 62 | occurrence slot. -/ |
| 63 | def clients (φ : BoundedSat.Formula) : ℕ := 3 + 2 * φ.vars + BoundedSat.slots φ |
| 64 | |
| 65 | /-- The due date of client `c` on day `i` of the construction. -/ |
| 66 | def due (φ : BoundedSat.Formula) (i c : ℕ) : ℕ := |
| 67 | if c < 3 then 2 |
| 68 | else if c < 3 + 2 * φ.vars then |
| 69 | let v := (c - 3) / 2 |
| 70 | if i = 0 then 2 * v + 5 |
| 71 | else if i = 1 then 2 |
| 72 | else if (c - 3) % 2 = 0 then 10 * v + 6 else 10 * v + 11 |
| 73 | else |
| 74 | let o := c - 3 - 2 * φ.vars |
| 75 | let l := BoundedSat.litOfSlot φ o |
| 76 | if i = 2 then |
| 77 | (if l.2 then 10 * l.1 + 5 + 2 * BoundedSat.slotRank φ o |
| 78 | else 10 * l.1 + 10 + 2 * BoundedSat.slotRank φ o) |
| 79 | else if o < 2 * φ.twoClauses then |
| 80 | (if i = 0 then 2 * φ.vars + 2 * (o / 2) + 7 else 2) |
| 81 | else |
| 82 | (if i = 0 then |
| 83 | 2 * φ.vars + 2 * φ.twoClauses + 2 * ((o - 2 * φ.twoClauses) / 3) + 9 |
| 84 | else 3 * ((o - 2 * φ.twoClauses) / 3) + 6) |
| 85 | |
| 86 | theorem two_le_due (φ : BoundedSat.Formula) (i c : ℕ) : 2 ≤ due φ i c := by |
| 87 | unfold due |
| 88 | simp only [] |
| 89 | split_ifs <;> omega |
| 90 | |
| 91 | /-- **The instance of Theorem 7**: three days, all processing times `2`, and the fairness |
| 92 | parameter `1`. -/ |
| 93 | def inst (φ : BoundedSat.Formula) : Instance where |
| 94 | clients := clients φ |
| 95 | days := 3 |
| 96 | p _ _ := 2 |
| 97 | d i c := due φ i c |
| 98 | p_pos _ _ := by omega |
| 99 | p_le_d i c := two_le_due φ i c |
| 100 | |
| 101 | /-- **The constructed instance has three days.** -/ |
| 102 | axiom inst_days (φ : BoundedSat.Formula) : (inst φ).days = 3 |
| 103 | |
| 104 | /-- **All processing times of the constructed instance are equal**, so in particular they |
| 105 | are day-independent. -/ |
| 106 | axiom inst_p_eq (φ : BoundedSat.Formula) (i i' : Fin (inst φ).days) |
| 107 | (j j' : Fin (inst φ).clients) : (inst φ).p i j = (inst φ).p i' j' |
| 108 | |
| 109 | /-- **The construction is correct**: the formula is satisfiable exactly when the instance |
| 110 | admits a schedule serving every client on at least one of the three days. -/ |
| 111 | axiom correct (φ : BoundedSat.Formula) : |
| 112 | φ.Satisfiable ↔ (inst φ).HasKFairSchedule 1 |
| 113 | |
| 114 | open Classical in |
| 115 | /-- **The reduction**, as a map on words: a word encoding a formula with no more variables |
| 116 | than positions is sent to the encoding of the constructed instance with the fairness |
| 117 | parameter `1`, and every other word to the rejected word. -/ |
| 118 | noncomputable def reduce (w : Word) : Word := |
| 119 | if h : ∃ φ : BoundedSat.Formula, |
| 120 | BoundedSat.encodeFormula φ = w ∧ φ.vars ≤ BoundedSat.slots φ then |
| 121 | encodeUniform (inst h.choose) 1 |
| 122 | else rejected |
| 123 | |
| 124 | /-- **The reduction is correct.** -/ |
| 125 | axiom reduce_correct (w : Word) : |
| 126 | w ∈ BoundedSat.BoundedSat ↔ |
| 127 | reduce w ∈ Uniform fun I k => I.days = 3 ∧ k = 1 ∧ I.DayIndepP |
| 128 | |
| 129 | /-- **The reduction runs in polynomial time.** -/ |
| 130 | axiom reduce_polyTime : Nonempty (Turing.TM2ComputableInPolyTime id id reduce) |
| 131 | |
| 132 | /-- **Theorem 7.** The problem with three days, the fairness parameter `1` and |
| 133 | day-independent processing times is NP-hard. -/ |
| 134 | axiom uniform_three_one_npHard : |
| 135 | NPHard (Uniform fun I k => I.days = 3 ∧ k = 1 ∧ I.DayIndepP) |
| 136 | |
| 137 | end Lax117284.Theorem7 |
| 138 |
Formalization Notes
Clients are numbered: the dummies ; then the pair of variable ; then one client per occurrence slot, those of the clauses of two literals first. Which of the at most two occurrences of a literal a slot is, which the third day's layout needs, is computed from the formula as the number of earlier slots carrying the same literal; it is the occurrence bound that makes this or .
The due dates are the source's with every index shifted, since the source numbers variables and clauses from and these are numbered from .
All processing times are equal, so the instance lies in the class of instances with day-independent processing times, which is the restriction Theorem 2 concerns.
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments