Lax Lean Archive

Just-in-Time Scheduling in Two-Stage Flexible Flow Shops

lax-496464·formalized by Yuval Itzhaki @yuvalyitz · Claude·registered·created ·GitHub @605f30b·Lean v4.33.0 epoch · mathlib db584cd6d46c

Loading review…

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

    This submission formalizes just-in-time scheduling in two-stage flexible flow shops, following Heeger, Hermelin, Itzhaki, Schieber and Shabtay.

    Flow-Shop Scheduling. In FF(1,m)∣∣∑jwjZjFF(1,m) \mid\mid \sum_j w_j Z_j, each job is preprocessed on a single machine and then processed on one of mm identical machines. The objective is to maximize the weight of jobs that finish exactly at their due dates. The formalization proves the feasibility characterization, dynamic programs with running times O(Wnm)O(W n^m), O(W2ωn)O(W 2^\omega n) and O(Wmqmax⁡n)O(W m^{q_{\max}} n), an O(nlog⁡n)O(n\log n) greedy algorithm for equal preprocessing times and unit weights, a totally unimodular integer program for proper instances with equal preprocessing times, and approximation schemes for bounded mm, ω\omega or qmax⁡q_{\max}. Here WW is the total job weight, ω\omega is the maximum overlap of second-stage intervals, and qmax⁡q_{\max} is the largest second-stage processing time. The formalized reduction from Hitting Set preserves the solution-size parameter as the number of machines and produces instances with unit weights. Strong NP-hardness and W[2]-hardness follow from the corresponding hardness of Hitting Set and the bounds established for the reduction.

    The W-Hierarchy. For completeness, the submission includes a supporting development of the W-hierarchy following Flum and Grohe (2006). This material goes beyond the scope of the scheduling project. The scheduling theorem for parameterized hardness states the existence of an FPT-reduction from Hitting Set; its interpretation as W[2]-hardness uses the W[2]-hardness of Hitting Set.

    Machine Model and Hypotheses. Algorithms and reductions are implemented on the archive's word RAM through its verified IMP+ compiler. Scheduling running-time statements assume positive processing times and sufficient word size for the input and intermediate values. FPT bounds use the bit size of the input and a computable parameter-dependent factor. The scheduling reduction uses hitting sets of size at least two and k(n−1)+2k(n-1)+2 segments; its input encoding bounds the universe size by the length of the input word. The concept pages state the precise hypotheses and explain the other differences from the printed scheduling paper. Hitting Set's NP-hardness is proved using the archive's Cook–Levin theorem, and the consecutive-ones theorem used for total unimodularity is also proved.

    The annotated manuscript presents the flow-shop results. The W-hierarchy results are documented in the archive's concept pages and Lean modules.

    View annotated paper

    9 pages · 68 marked passages

    Concepts

    Concept map
    95 concepts
    100%
    Compressed sparse row encoding of a graphA graph with a parameter appendedConjunctive 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 an InstanceThe Two Conditions on a Feasible SetConsecutive Ones Implies TotalUnimodularityThe Construction of Section 8Corollary 1Corollary 2Corollary 3Corollary 4The Dynamic Program of Section 3, and ItsTableEarliest-Start-Time Order, and DistinctEndpointsA Set of Jobs Is Feasible Exactly When ItSatisfies Both ConditionsJust-in-Time Scheduling in a Two-StageFlexible Flow ShopRounding the Weights, and What anApproximation Scheme DeliversThe Greedy of Section 6.1, and ItsDomination OrderHitting SetThe Reduction from Satisfiability to HittingSetHitting Set Is NP-HardThe Integer Program of Section 6.2Lemma 1Lemma 2Lemma 3Lemma 4Lemma 5NP-Hardness, and Strong NP-Hardness, of aScheduling ProblemEvery Instance May Be Assumed to HaveDistinct EndpointsObservation 1Parameterized Problems andFPT-Reductions on a Word RAMThe Just-in-Time Flow Shop as a Problemon WordsThe Due-Date Profile of Section 5, andRecursion (5)Uniform Preprocessing Times, and ProperInstancesThe Endpoint Sweep of Section 4, and ItsTableTheorem 1Theorem 2Theorem 3Theorem 4Theorem 5W[2]-HardnessFixed-Parameter Time on the Word RAMFPT-Reductions, FPT, Hardness andCompletenessThe Calculus of FPT-ReductionsFixed-Parameter Computations ComposePolynomial-Time and Strict Reductions AreFPT-ReductionsComputable BoundsFinite Relational StructuresFirst-Order Formulas and the Classes Σ_tand Π_tModel Checking and Weighted FaginDefinabilityThe W-Hierarchy and the A-HierarchyBasic Facts About the HierarchiesClique, Independent Set and Dominating SetHitting SetWeighted Satisfiability of CNF FormulasClique Is in W[1]Clique Is in A[1]Model Checking for Σ₁ Reduces to PositiveΣ₁Positive Σ₁ Model Checking Reduces toBinary RelationsΣ₁ Model Checking over Binary RelationsReduces to CliqueClique Is A[1]-CompleteWeighted Definability of a Π₁ SentenceReduces to Weighted d-CNF SatisfiabilityWeighted d-CNF Satisfiability Is in A[1]W[1] = A[1]Clique Is W[1]-CompleteIndependent Set Is W[1]-CompleteMulticoloured Clique Is W[1]-CompleteHitting Set Is in W[2]Hitting Set Is W[2]-CompleteDominating Set Is W[2]-CompleteIndependent Set on Adjacency MatricesThe Multicoloured Graph of an IndependentSet InstanceNP-Hardness of a Problem on Words ofNumbersIndependent Set Reduces to MulticolouredCliqueMulticoloured Clique Is NP-HardWord Encoding of an InstanceBinary encoding of finite wordsPolynomial-time computation by a wordRAMPolynomial-time computation by a TuringmachineBinary encoding of graph decision instancesGraph decision problems and NP-hardnessExcluded induced grid minorsIndependent Set without a 5×5 induced gridminorInduced minorsMaximum cutsThe word RAMComputing a function within a time boundMulticoloured CliqueParameterized Problems andFPT-Reductions on a Word RAMPolynomial-Time Many-One Reductions onthe Word RAM
    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-496464,
  author = {Yuval Itzhaki and Claude},
  title = {Just-in-Time Scheduling in Two-Stage Flexible Flow Shops},
  year = {2026},
  howpublished = {Lax Archive, lax-496464},
  url = {https://laxarchive.org/lax-496464/},
}

    References

    1. Klaus Heeger, Danny Hermelin, Yuval Itzhaki, Baruch Schieber and Dvir Shabtay. Just-in-Time Scheduling in Two-Stage Flexible Flow Shops. European Journal of Operational Research 333:652–664, 2026. doi:10.1016/j.ejor.2026.02.017
    2. Richard M. Karp. Reducibility among Combinatorial Problems. In Complexity of Computer Computations 85–103, 1972. doi:10.1007/978-1-4684-2001-2_9
    3. Michael R. Garey and David S. Johnson. Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman, 1979.
    4. Rodney G. Downey and Michael R. Fellows. Parameterized Complexity. Springer, 1999.
    5. Delbert R. Fulkerson and Oliver A. Gross. Incidence Matrices and Interval Graphs. Pacific Journal of Mathematics 15(3):835–855, 1965.
    6. Alan J. Hoffman and Joseph B. Kruskal. Integral Boundary Points of Convex Polyhedra. In Linear Inequalities and Related Systems 223–246, 1956.
    7. Martin C. Carlisle and Errol L. Lloyd. On the kk-Coloring of Intervals. Discrete Applied Mathematics 59(3):225–235, 1995.
    8. Jörg Flum and Martin Grohe. Parameterized Complexity Theory. Springer, 2006. doi:10.1007/3-540-29953-X
    9. Marek Cygan, Fedor V. Fomin, Łukasz Kowalik, Daniel Lokshtanov, Dániel Marx, Marcin Pilipczuk, Michał Pilipczuk and Saket Saurabh. Parameterized Algorithms. Springer, 2015. doi:10.1007/978-3-319-21275-3
    10. 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. doi:10.1016/j.tcs.2008.09.065

    Discussion

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

    Loading discussion…