Lax Lean Archive

The Integer Program of Section 6.2

Lax496464.IntegerProgram · concepts/Lax496464/IntegerProgram.lean · lax-496464

definition

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

    Definition

    When all preprocessing times are equal to pp, a set of jobs is feasible exactly when it satisfies two families of linear inequalities in its own indicator vector x∈{0,1}n\mathbf{x} \in \{0,1\}^n:

    ∑i≤jxi≤⌊sj/p⌋(6),∑i alive at sjxi≤m(7),\sum_{i \le j} x_i \le \lfloor s_j / p \rfloor \quad (6), \qquad \sum_{i \text{ alive at } s_j} x_i \le m \quad (7),

    one of each per job jj. The first is Condition 1 — with equal preprocessing times, the time the first stage has spent is the number of jobs it has run — and the second is Condition 2 in its depth form, tested at the start times, where the number of jobs alive can only increase.

    Maximizing ∑jwjxj\sum_j w_j x_j subject to these is therefore the problem itself, written as an integer program with 2n2n constraints and nn variables.

    Concept map
    5 concepts; 1 descendant hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    In the paper

    • page 6 of this submission's paper

    Lean source view on GitHub

    1import Lax496464.Conditions
    2import Lax496464.EstOrder
    3import Lax496464.ProperInstances
    4import Mathlib.Data.Matrix.Mul
    5
    6/-!
    7---
    8title: The Integer Program of Section 6.2
    9type: definition
    10---
    11When all preprocessing times are equal to pp, a set of jobs is feasible exactly when it
    12satisfies two families of linear inequalities in its own indicator vector
    13x∈{0,1}n\mathbf{x} \in \{0,1\}^n:
    14∑i≤jxi≤⌊sj/p⌋(6),∑i alive at sjxi≤m(7),\sum_{i \le j} x_i \le \lfloor s_j / p \rfloor \quad (6), \qquad \sum_{i \text{ alive at } s_j} x_i \le m \quad (7),
    15
    16one of each per job jj. The first is Condition 1 — with equal preprocessing times, the
    17time the first stage has spent is the number of jobs it has run — and the second is
    18Condition 2 in its depth form, tested at the start times, where the number of jobs alive
    19can only increase.
    20
    21Maximizing ∑jwjxj\sum_j w_j x_j subject to these is therefore the problem itself, written as
    22an integer program with 2n2n constraints and nn variables.
    23
    24# Formalization Notes
    25
    26The constraint matrix is indexed by a sum type, one copy of the jobs for each family, so
    27that the two families can be told apart without an arithmetic encoding of the row index.
    28Its entries are integers rather than naturals, because the inequalities are, and because
    29total unimodularity is a statement about an integer matrix.
    30
    31Constraint (6) is imposed for *every* job, selected or not. That is what the program
    32says, and it makes the correspondence to feasible sets fail on an instance with a
    33negative start time: the row of such a job is unsatisfiable even at x=0\mathbf{x} = \mathbf{0}
    34, while the empty set is feasible. Such a job can never be completed just in
    35time and would be deleted in advance, which is presumably what the paper intends; since
    36the model here admits negative start times, the correspondence carries the hypothesis
    37that they are nonnegative.
    38
    39Properness is *not* needed for the correspondence. It is needed only for the consecutive
    40ones property of the second family, which is what the fifth lemma is about.
    41-/
    42
    43namespace Lax496464.IntegerProgram
    44
    45open Lax496464.FlowShop Lax496464.FlowShop.Instance
    46
    47variable (I : Instance)
    48
    49/-- The constraint matrix: the rows `inl j` are the prefix sums of constraint (6), the
    50rows `inr j` the jobs alive at `s j` of constraint (7). -/
    51def matrix : Matrix (I.Job ⊕ I.Job) I.Job ℤ
    52 | Sum.inl j, i => if i ≤ j then 1 else 0
    53 | Sum.inr j, i => if s i ≤ s j ∧ s j < (I.d i : ℤ) then 1 else 0
    54
    55/-- The right-hand sides: `⌊s j / p⌋` for (6) and `m` for (7). -/
    56def rhs (p : ℕ) : I.Job ⊕ I.Job → ℤ
    57 | Sum.inl j => s j / p
    58 | Sum.inr _ => I.machines
    59
    60/-- The `0/1` vector of a set of jobs. -/
    61def indicator (Z : Finset I.Job) : I.Job → ℤ := fun i => if i ∈ Z then 1 else 0
    62
    63end Lax496464.IntegerProgram
    64
    Formalization Notes

    The constraint matrix is indexed by a sum type, one copy of the jobs for each family, so that the two families can be told apart without an arithmetic encoding of the row index. Its entries are integers rather than naturals, because the inequalities are, and because total unimodularity is a statement about an integer matrix.

    Constraint (6) is imposed for every job, selected or not. That is what the program says, and it makes the correspondence to feasible sets fail on an instance with a negative start time: the row of such a job is unsatisfiable even at x=0\mathbf{x} = \mathbf{0}, while the empty set is feasible. Such a job can never be completed just in time and would be deleted in advance, which is presumably what the paper intends; since the model here admits negative start times, the correspondence carries the hypothesis that they are nonnegative.

    Properness is not needed for the correspondence. It is needed only for the consecutive ones property of the second family, which is what the fifth lemma is about.

    Builds on
    Used by
    From Mathlib

    Discussion

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

    Loading discussion…