While this submission is a draft, it cannot be used by other submissions.

Three Days and the Fairness Parameter One

Lax117284.Theorem7 · concepts/Lax117284/Theorem7.lean · lax-117284

proven

Loading review…

Sign in with ORCID

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    Theorem 7. The problem 1∣rep, pi,j=p∣min⁡j∑iZi,j1 \mid \mathrm{rep},\, p_{i,j} = p \mid \min_j \sum_i Z_{i,j} is NP-hard for k=1k = 1 and m=3m = 3.

    Let φ\varphi be a [2,3]-bounded 3-SAT formula with nn variables, ℓ\ell clauses of two literals and qq clauses of three literals. Build an instance with three days and the clients: three dummies; two clients xv1,xv0x_v^1, x_v^0 per variable vv; and one client per occurrence of a literal in a clause. Every processing time is 22, 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 22 for the three dummies, 2v+52v+5 for both clients of variable vv, 2n+2j+72n+2j+7 for both clients of the jj-th clause of two literals, and 2n+2ℓ+2j+92n+2\ell+2j+9 for all three clients of the jj-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 xv1/xv0x_v^1 / x_v^0 — 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 22, so they are pairwise conflicting, while the clients of the jj-th clause of three literals sit alone at 3j+63j+6; 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 xv1x_v^1 sits at 10v+610v+6 and xv0x_v^0 at 10v+1110v+11, while an occurrence of the literal vv sits at 10v+510v+5 or 10v+710v+7 and an occurrence of ¬v\lnot v at 10v+1010v+10 or 10v+1210v+12, 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 11-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
    8 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 correct proven

    2 inst_days proven

    3 inst_p_eq proven

    In the paper

    • page 2 of this submission's paper

    Lean source view on GitHub

    1import Lax117284.BoundedSat
    2import Lax117284.Problems
    3
    4/-!
    5---
    6title: Three Days and the Fairness Parameter One
    7type: theorem
    8---
    9**Theorem 7.** The problem
    101∣rep, pi,j=p∣min⁡j∑iZi,j1 \mid \mathrm{rep},\, p_{i,j} = p \mid \min_j \sum_i Z_{i,j} is NP-hard for k=1k = 1 and
    11m=3m = 3.
    12
    13Let φ\varphi be a [2,3]-bounded 3-SAT formula with nn variables, ℓ\ell clauses of two
    14literals and qq clauses of three literals. Build an instance with three days and the
    15clients: three *dummies*; two clients xv1,xv0x_v^1, x_v^0 per variable vv; and one client per
    16occurrence of a literal in a clause. Every processing time is 22, so two jobs of a day
    17conflict exactly when their due dates differ by at most one, and the whole construction is a
    18matter of placing due dates on a line, three times.
    19
    20On the first day the due dates are 22 for the three dummies, 2v+52v+5 for both clients of
    21variable vv, 2n+2j+72n+2j+7 for both clients of the jj-th clause of two literals, and
    222n+2ℓ+2j+92n+2\ell+2j+9 for all three clients of the jj-th clause of three literals. Clients
    23sharing a due date conflict and nothing else does, so the first day admits one client out of
    24each group: one dummy, one of xv1/xv0x_v^1 / x_v^0 — this is the truth assignment — and one
    25client of every clause. On the second day the dummies, the variable clients and the clients
    26of the clauses of two literals all have the due date 22, so they are pairwise conflicting,
    27while the clients of the jj-th clause of three literals sit alone at 3j+63j+6; since a dummy
    28runs on every day, the second day is a dead end for everything but one client of each clause
    29of three literals. On the third day xv1x_v^1 sits at 10v+610v+6 and xv0x_v^0 at 10v+1110v+11, while
    30an occurrence of the literal vv sits at 10v+510v+5 or 10v+710v+7 and an occurrence of ¬v\lnot v
    31at 10v+1010v+10 or 10v+1210v+12, according to which of its at most two occurrences it is. So on the
    32third day a client of an occurrence conflicts with exactly the variable client that
    33*falsifies* its literal, and with nothing else.
    34
    35The three dummies conflict with each other on all three days, so a 11-fair schedule runs
    36exactly one of them on each day. This is what forces the selection on the first day and
    37makes the second day a dead end, and a client of an occurrence can then be served only on
    38the third day — which is possible exactly when the assignment selected on the first day
    39makes its literal true.
    40
    41# Formalization Notes
    42
    43Clients are numbered: the dummies 0,1,20, 1, 2; then the pair xv1,xv0x_v^1, x_v^0 of variable vv;
    44then one client per occurrence slot, those of the clauses of two literals first. Which of
    45the at most two occurrences of a literal a slot is, which the third day's layout needs, is
    46computed from the formula as the number of earlier slots carrying the same literal; it is
    47the occurrence bound that makes this 00 or 11.
    48
    49The due dates are the source's with every index shifted, since the source numbers variables
    50and clauses from 11 and these are numbered from 00.
    51
    52All processing times are equal, so the instance lies in the class of instances with
    53day-independent processing times, which is the restriction Theorem 2 concerns.
    54-/
    55
    56namespace Lax117284.Theorem7
    57
    58open Lax117284.Scheduling Lax117284.Problems Lax434930.PolynomialTime
    59open Lax429075.Reductions
    60
    61/-- The number of clients of the construction: three dummies, two per variable, and one per
    62occurrence slot. -/
    63def clients (φ : BoundedSat.Formula) : ℕ := 3 + 2 * φ.vars + BoundedSat.slots φ
    64
    65/-- The due date of client `c` on day `i` of the construction. -/
    66def 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
    86theorem 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
    92parameter `1`. -/
    93def 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.** -/
    102axiom inst_days (φ : BoundedSat.Formula) : (inst φ).days = 3
    103
    104/-- **All processing times of the constructed instance are equal**, so in particular they
    105are day-independent. -/
    106axiom 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
    110admits a schedule serving every client on at least one of the three days. -/
    111axiom correct (φ : BoundedSat.Formula) :
    112 φ.Satisfiable ↔ (inst φ).HasKFairSchedule 1
    113
    114open Classical in
    115/-- **The reduction**, as a map on words: a word encoding a formula with no more variables
    116than positions is sent to the encoding of the constructed instance with the fairness
    117parameter `1`, and every other word to the rejected word. -/
    118noncomputable 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.** -/
    125axiom 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.** -/
    130axiom reduce_polyTime : Nonempty (Turing.TM2ComputableInPolyTime id id reduce)
    131
    132/-- **Theorem 7.** The problem with three days, the fairness parameter `1` and
    133day-independent processing times is NP-hard. -/
    134axiom uniform_three_one_npHard :
    135 NPHard (Uniform fun I k => I.days = 3 ∧ k = 1 ∧ I.DayIndepP)
    136
    137end Lax117284.Theorem7
    138
    Show ProofShow ProofShow ProofShow ProofShow ProofShow Proof
    Formalization Notes

    Clients are numbered: the dummies 0,1,20, 1, 2; then the pair xv1,xv0x_v^1, x_v^0 of variable vv; 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 00 or 11.

    The due dates are the source's with every index shifted, since the source numbers variables and clauses from 11 and these are numbered from 00.

    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.

    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

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

    Loading discussion…