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

Fair Repetitive Interval Scheduling

lax-117284·formalized by Yuval Itzhaki @yuvalyitz · Claude·created ·GitHub @6e9d9e2·Lean v4.33.0 epoch · mathlib db584cd6d46c

Loading review…

Sign in with ORCID

Community review

Flags

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

No flags have been submitted.

    Community review

    Flag this submission

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

    Abstract

    Each of nn clients submits one job on every one of mm days. A job has a processing time and a due date, and — the schedule being just-in-time — occupies exactly the interval between them, so that on any single day the jobs a machine can accept are the ones whose intervals are pairwise disjoint. The objective is fairness rather than throughput: every client must be served on at least kk of the mm days. This submission formalizes the theorems of Heeger, Hermelin, Itzhaki, Molter and Shabtay on this problem, 1∣rep∣min⁡j∑iZi,j1 \mid \mathrm{rep} \mid \min_j \sum_i Z_{i,j}.

    For 0≤k≤m0 \le k \le m, the problem is solvable in polynomial time when k∈{0,m−1,m}k \in \{0,m-1,m\} and NP-hard for every fixed pair (m,k)(m,k) with 0<k<m−10<k<m-1. Hardness already holds for m=3m=3 and k=1k=1, with identical processing times. Under day-independent processing times it remains NP-hard and becomes a bipartite matching problem when the processing times are one. Under day-independent due dates it remains NP-hard, and becomes tractable either for a constant number of days, by a dynamic program over the clients in due-date order, or for day-independent processing times, where a kk-fair schedule exists exactly when kk times the chromatic number of the one conflict graph is at most mm. Measured against the treewidth τ\tau of the overall conflict graph, the problem is NP-hard for constant τ\tau, fixed-parameter tractable for m+τm + \tau, and fixed-parameter tractable for nn.

    Every gadget construction is given explicitly, with numbered clients and days, and each statement about it is separate: that the construction is correct, that the instance it produces has the structure claimed of it, and that it is computed within the stated resources. The two objectives — the uniform one and the per-client generalization 1∣kj,rep∣min⁡j∑iZi,j1 \mid k_j, \mathrm{rep} \mid \min_j \sum_i Z_{i,j}, through which the treewidth reduction passes — are one definition, the uniform case being the constant one. Hardness is stated against the class NP of the archive; treewidth is the archive's, and the tree decompositions the dynamic program of the treewidth algorithm runs on are nice ones in the sense of Kloks.

    The formalization adjusts the placement of inactive jobs to preserve the conflict graph required by the treewidth argument. On each gadget day, the dummy client's interval covers a region containing a separate, disjoint slot for every inactive client. This preserves the blocking argument without introducing conflicts between inactive clients. The concept pages specify the construction and its tree decomposition.

    View annotated paper

    6 pages · 24 marked passages

    Concepts

    Concept map
    54 concepts
    100%
    Saturating and Perfect Matchings, Decidedin the Same TimeBipartite Graphs with a Fixed Bipartition,and Their EncodingKuhn's AlgorithmKuhn's Algorithm Computes a MaximumMatchingThe Matching Number of a Bipartite Graphin Time O(n · |x|)Matchings, the Matching Number, andSaturationNice Tree Decompositions of Small WidthAre Found in Fixed-Parameter TimeNice tree decompositions of small width arefound in fixed-parameter timeOptimal tree decompositions from a givenoneSatisfiability of Bounded OccurrenceThe Conflict Graphs of an InstanceRaising the Number of Days and theFairness ParameterThe Extreme Values of the FairnessParameterGraphs and nice tree decompositions aswordsThe Integer Programs of the Clients'Reduction Are Fixed-Parameter TractableWord Encoding of an InstanceJust-in-Time Scheduling on UnrelatedParallel MachinesPer-Client Fairness Parameters at TreewidthFourPer-Client Fairness Parameters Reduce to aUniform OneMulticoloured Independent SetParameterized Problems on a Word RAMThe Decision Problems as LanguagesFair Repetitive Interval SchedulingThe Complexity of Fair Repetitive IntervalScheduling in the Fairness ParameterUnit Processing Times as a BipartiteMatching ProblemJust-in-Time Scheduling on UnrelatedMachines as Day-Independent Due DatesThe Dynamic Program for Day-IndependentDue DatesDay-Independent Due Dates and ProcessingTimesDay-Independent Processing TimesDay-Independent Due DatesStructural Parameters of the Conflict GraphThree Days and the Fairness Parameter OneThe Fairness Parameter One Below theNumber of DaysThe Algorithm: Reachability in theImplication Graph, One Variable at a Time2-CNF Formulas and the Language 2-SATCorrectness of the AlgorithmThe Satisfiability Criterion for 2-CNFFormulasThe Implication Graph of a 2-CNF Formula2-SAT Is in P2-SAT Is Decided in Time Linear in theWord Times the Number of VariablesTwo-SatisfiabilityTreewidthCompressed sparse row encoding of a graphConjunctive normal formBinary encoding of CNF formulasPolynomial many-one reductions andNP-completenessThe satisfiability language and verifierBinary encoding of an input and a certificateThe complexity class NPThe complexity class PBinary encoding of finite wordsPolynomial-time computation by a wordRAMThe word RAMComputing a function within a time bound
    Proven claimDefinitionThis submissionOther submissionA → B: B builds on A

    Proofs

    Proof networkview on GitHub

    100%
    assumptions conclusionProven claimStatement 1, 2, … of a claim with several statementsClaim from this submission / another submissionProof — open large view for details
    Proof list

    Lean sources for these proofs: proofs/ on GitHub

    Proof code is not displayed; the archive records each proof's checked relationship between claims.

    Related submissions

    Submission map

    100%
    This submissionOther submissionA → B: B's concepts build on AA → B: only B's proofs build on A

    Cite this

    This is only the formalizers. The authors of the formalized results may be different (see References).

    @misc{lax-117284,
      author = {Yuval Itzhaki and Claude},
      title = {Fair Repetitive Interval Scheduling},
      year = {2026},
      howpublished = {Lax Archive, lax-117284},
      url = {https://laxarchive.org/lax-117284/},
      note = {draft},
    }

    References

    1. Klaus Heeger, Danny Hermelin, Yuval Itzhaki, Hendrik Molter and Dvir Shabtay. Fair Repetitive Interval Scheduling. Algorithmica, 2025. doi:10.1007/s00453-025-01322-y
    2. Craig A. Tovey. A Simplified NP-Complete Satisfiability Problem. Discrete Applied Mathematics 8(1):85–89, 1984.
    3. Shao Chin Sung and Milan Vlach. Maximizing Weighted Number of Just-in-Time Jobs on Unrelated Parallel Machines. Journal of Scheduling 8(5):453–460, 2005.
    4. Krzysztof Pietrzak. On the Parameterized Complexity of the Fixed Alphabet Shortest Common Supersequence and Longest Common Subsequence Problems. Journal of Computer and System Sciences 67(4):757–771, 2003.
    5. Michael R. Fellows, Danny Hermelin, Frances Rosamond and Stéphane Vialette. On the Parameterized Complexity of Multiple-Interval Graph Problems. Theoretical Computer Science 410(1):53–61, 2009.
    6. Bengt Aspvall, Michael F. Plass and Robert E. Tarjan. A Linear-Time Algorithm for Testing the Truth of Certain Quantified Boolean Formulas. Information Processing Letters 8(3):121–123, 1979.
    7. John E. Hopcroft and Richard M. Karp. An n5/2n^{5/2} Algorithm for Maximum Matchings in Bipartite Graphs. SIAM Journal on Computing 2(4):225–231, 1973.
    8. Hans L. Bodlaender. A Linear-Time Algorithm for Finding Tree-Decompositions of Small Treewidth. SIAM Journal on Computing 25(6):1305–1317, 1996.
    9. Ton Kloks. Treewidth: Computations and Approximations. Springer 842, 1994.
    10. Hans L. Bodlaender and Ton Kloks. Efficient and Constructive Algorithms for the Pathwidth and Treewidth of Graphs. Journal of Algorithms 21(2):358–402, 1996.
    11. Ernst Althaus and Sarah Ziegler. Optimal Tree Decompositions Revisited: A Simpler Linear-Time FPT Algorithm. arXiv:1912.09144, 2020.
    12. Martin Charles Golumbic. Algorithmic Graph Theory and Perfect Graphs. Academic Press, 1980.
    13. Harold W. Kuhn. The Hungarian Method for the Assignment Problem. Naval Research Logistics Quarterly 2(1–2):83–97, 1955.

    Discussion

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

    Loading discussion…