Lax Lean Archive

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

The Complexity of Fair Repetitive Interval Scheduling in the Fairness Parameter

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

proven

Loading review…

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 1. The problem 1∣rep∣min⁡j∑iZi,j1 \mid \mathrm{rep} \mid \min_j \sum_i Z_{i,j} is solvable in polynomial time when k∈{0, m−1, m}k \in \{0,\, m-1,\, m\}. For every fixed pair (m,k)(m,k) with 0<k<m−10<k<m-1, the problem is NP-hard.

    The three tractable values are settled separately: k=0k = 0 and k=mk = m by inspection of the instance, and k=m−1k = m-1 by a reduction to 2-satisfiability. Hardness holds already for every fixed pair (m,k)(m, k) with m≥3m \ge 3 and 0<k<m−10 < k < m-1; it is obtained for (3,1)(3,1) from a satisfiability problem of bounded occurrence and lifted to all other pairs by two constructions adding one day at a time.

    Concept map
    7 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 uniform_extremes_mem_P proven

    2 uniform_npHard proven

    In the paper

    • page 1 of this submission's paper

    Lean source view on GitHub

    1import Lax117284.Problems
    2
    3/-!
    4---
    5title: The Complexity of Fair Repetitive Interval Scheduling in the Fairness Parameter
    6type: theorem
    7---
    8**Theorem 1.** The problem 1∣rep∣min⁡j∑iZi,j1 \mid \mathrm{rep} \mid \min_j \sum_i Z_{i,j} is solvable in
    9polynomial time when k∈{0, m−1, m}k \in \{0,\, m-1,\, m\}. For every fixed pair (m,k)(m,k)
    10with 0<k<m−10<k<m-1, the problem is NP-hard.
    11
    12The three tractable values are settled separately: k=0k = 0 and k=mk = m by inspection of the
    13instance, and k=m−1k = m-1 by a reduction to 2-satisfiability. Hardness holds already for
    14every fixed pair (m,k)(m, k) with m≥3m \ge 3 and 0<k<m−10 < k < m-1; it is obtained for (3,1)(3,1) from
    15a satisfiability problem of bounded occurrence and lifted to all other pairs by two
    16constructions adding one day at a time.
    17
    18# Formalization Notes
    19
    20The tractable half is one claim about the language of all three cases at once. A word
    21belongs to that language only if its parameter is one of the three values, so an algorithm
    22deciding it must first read the parameter and compare it with the number of days; nothing is
    23gained by splitting the claim.
    24
    25The hard half is stated for each fixed pair (m,k)(m, k) separately, which is the stronger
    26reading: the number of days is a constant of the slice rather than part of the input, so
    27hardness is not an artifact of letting mm grow with the instance.
    28-/
    29
    30namespace Lax117284.Theorem1
    31
    32open Lax117284.Scheduling Lax117284.Problems Lax434930.PolynomialTime
    33
    34/-- **The tractable values of the fairness parameter.** The problem restricted to
    35instances whose fairness parameter is `0`, `m - 1` or `m` is solvable in polynomial
    36time. -/
    37axiom uniform_extremes_mem_P :
    38 Uniform (fun I k => k = 0 ∨ k + 1 = I.days ∨ k = I.days) ∈ P
    39
    40/-- **Theorem 1.** For every fixed number `m ≥ 3` of days and every fairness parameter `k`
    41with `0 < k < m - 1`, the problem restricted to that pair is NP-hard. -/
    42axiom uniform_npHard (m k : ℕ) (hm : 3 ≤ m) (hk : 0 < k) (hk' : k + 1 < m) :
    43 NPHard (Uniform fun I k' => I.days = m ∧ k' = k)
    44
    45end Lax117284.Theorem1
    46
    Show ProofShow Proof
    Formalization Notes

    The tractable half is one claim about the language of all three cases at once. A word belongs to that language only if its parameter is one of the three values, so an algorithm deciding it must first read the parameter and compare it with the number of days; nothing is gained by splitting the claim.

    The hard half is stated for each fixed pair (m,k)(m, k) separately, which is the stronger reading: the number of days is a constant of the slice rather than part of the input, so hardness is not an artifact of letting mm grow with the instance.

    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…