Lax Lean Archive

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

Maximizing the minimum machine load

Lax434175.MachineCovering · concepts/Lax434175/MachineCovering.lean · lax-434175

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

    The problem P∣∣Cmin⁡P \mid\mid C_{\min}. An instance has nn jobs with processing times pjp_j and mm identical machines. A solution assigns every job to a machine. The load of a machine is the sum of the processing times of its jobs, and the goal is to maximize the smallest load.

    As a minimization problem, the cost of an assignment is the negative of the smallest load; without machines it is 00.

    Concept map
    2 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

    Lean source view on GitHub

    1import Mathlib.Algebra.BigOperators.Group.Finset.Basic
    2import Mathlib.Data.Finset.Lattice.Fold
    3import Mathlib.Data.Fintype.BigOperators
    4import Lax434175.Problems
    5
    6/-!
    7---
    8title: Maximizing the minimum machine load
    9type: definition
    10---
    11The problem P∣∣Cmin⁡P \mid\mid C_{\min}. An instance has nn jobs with processing
    12times pjp_j and mm identical machines. A solution assigns every job to a
    13machine. The load of a machine is the sum of the processing times of its
    14jobs, and the goal is to maximize the smallest load.
    15
    16As a minimization problem, the cost of an assignment is the negative of the
    17smallest load; without machines it is 00.
    18-/
    19
    20namespace Lax434175.MachineCovering
    21open Lax434175.Problems
    22
    23structure Inst where
    24 jobs : ℕ
    25 machines : ℕ
    26 p : Fin jobs → ℕ
    27
    28/-- The load of a machine. -/
    29def load (x : Inst) (σ : Fin x.jobs → Fin x.machines) (i : Fin x.machines) : ℕ :=
    30 ∑ j ∈ Finset.univ.filter (fun j => σ j = i), x.p j
    31
    32/-- The smallest load of a machine; `0` without machines. -/
    33def minLoad (x : Inst) (σ : Fin x.jobs → Fin x.machines) : ℕ :=
    34 if h : 0 < x.machines then Finset.univ.inf' ⟨⟨0, h⟩, Finset.mem_univ _⟩ (load x σ) else 0
    35
    36/-- `P || C_min` -/
    37def problem : Problem where
    38 Inst := Inst
    39 Sched x := Fin x.jobs → Fin x.machines
    40 feasible _ _ := True
    41 cost x σ := -(minLoad x σ : ℚ)
    42
    43end Lax434175.MachineCovering
    44
    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…