Documentation

DescriptiveComplexity.Problems.JobSequencing.Defs

Job sequencing: definition #

SEQUENCING (Karp 1972): given jobs with execution times, deadlines and penalties, and a bound, is there a one-processor schedule whose jobs missing their deadline carry a total penalty at most the bound? Like Knapsack it is written in binary (DescriptiveComplexity.Numbers.BinRel) – times, deadlines, penalties and the bound – since under the unary encoding the problem is solvable in polynomial time by dynamic programming and is therefore not NP-hard at all.

The vocabulary #

FirstOrder.Language.jobSeq carries

job j and posn p, the jobs and the bit positions;
time j p, dline j p and pen j p, the bits of the execution time, of the deadline and of the penalty of j;
bnd p, the bits of the penalty bound;
le, a linear order fixing the place values, folded into the yes-instances (DescriptiveComplexity.IsLinOrd) as everywhere in the binary encoding.

The schedule #

A schedule is a linear order on the universe rather than a permutation of an initial segment: on a finite universe the two are the same thing, and a relation is what a Σ₁ certificate can guess and what a first-order kernel can constrain. A job's completion time is then the total execution time of the jobs at or before it (DescriptiveComplexity.JSCompletion), it is late when that exceeds its deadline, and the schedule is good when the late jobs' penalties sum to at most the bound. Only jobs are summed over, so the elements of the universe that are bit positions ride along in the order harmlessly.

@[reducible, inline]

abbrev FirstOrder.Language.jsDline :

Language.jobSeq.Relations 2

dline j p: the deadline of j has bit 1 at position p.

Equations

FirstOrder.Language.jsDline = FirstOrder.Language.jobSeqRel.dline

Instances For

Dependency graph

instance FirstOrder.Language.instIsRelationalJobSeq :

Language.jobSeq.IsRelational

Dependency graph

@[instance_reducible]

instance FirstOrder.Language.instDecidableEqJobSeqRel {a✝ : ℕ} :

DecidableEq (jobSeqRel a✝)

Equations

FirstOrder.Language.instDecidableEqJobSeqRel = FirstOrder.Language.instDecidableEqJobSeqRel.decEq

Dependency graph

inductive FirstOrder.Language.jobSeqRel :

The relation symbols of the language.

job : jobSeqRel 1
job j: j is a job.
posn : jobSeqRel 1
posn p: p is a bit position.
time : jobSeqRel 2
time j p: the execution time of j has bit 1 at position p.
dline : jobSeqRel 2
dline j p: the deadline of j has bit 1 at position p.
pen : jobSeqRel 2
pen j p: the penalty of j has bit 1 at position p.
bnd : jobSeqRel 1
bnd p: the penalty bound has bit 1 at position p.
le : jobSeqRel 2
le a b: the linear order carrying the place values.

Instances For

Dependency graph

def FirstOrder.Language.instDecidableEqJobSeqRel.decEq {a✝ : ℕ} (x✝ x✝¹ : jobSeqRel a✝) :

Decidable (x✝ = x✝¹)

Equations

Instances For

Dependency graph

@[reducible, inline]

abbrev FirstOrder.Language.jsTime :

Language.jobSeq.Relations 2

time j p: the execution time of j has bit 1 at position p.

Equations

FirstOrder.Language.jsTime = FirstOrder.Language.jobSeqRel.time

Instances For

Dependency graph

@[reducible, inline]

abbrev FirstOrder.Language.jsPen :

Language.jobSeq.Relations 2

pen j p: the penalty of j has bit 1 at position p.

Equations

FirstOrder.Language.jsPen = FirstOrder.Language.jobSeqRel.pen

Instances For

Dependency graph

@[reducible, inline]

abbrev FirstOrder.Language.jsJob :

Language.jobSeq.Relations 1

job j: j is a job.

Equations

FirstOrder.Language.jsJob = FirstOrder.Language.jobSeqRel.job

Instances For

Dependency graph

@[reducible, inline]

abbrev FirstOrder.Language.jsLe :

Language.jobSeq.Relations 2

le a b: the linear order carrying the place values.

Equations

FirstOrder.Language.jsLe = FirstOrder.Language.jobSeqRel.le

Instances For

Dependency graph

def FirstOrder.Language.jobSeq :

The relational language of job-sequencing instances: jobs and bit positions, the bits of each job's execution time, deadline and penalty, the bits of the penalty bound, and a linear order.

Equations

FirstOrder.Language.jobSeq = { Functions := fun (x : ℕ) => Empty, Relations := FirstOrder.Language.jobSeqRel }

Instances For

Dependency graph

@[reducible, inline]

abbrev FirstOrder.Language.jsBnd :

Language.jobSeq.Relations 1

bnd p: the penalty bound has bit 1 at position p.

Equations

FirstOrder.Language.jsBnd = FirstOrder.Language.jobSeqRel.bnd

Instances For

Dependency graph

@[reducible, inline]

abbrev FirstOrder.Language.jsPosn :

Language.jobSeq.Relations 1

posn p: p is a bit position.

Equations

FirstOrder.Language.jsPosn = FirstOrder.Language.jobSeqRel.posn

Instances For

Dependency graph

The shorthands of the vocabulary #

def DescriptiveComplexity.JSJob {A : Type} [FirstOrder.Language.jobSeq.Structure A] (a0 : A) :

job j: j is a job.

Equations

DescriptiveComplexity.JSJob a0 = FirstOrder.Language.Structure.RelMap FirstOrder.Language.jsJob ![a0]

Instances For

Dependency graph

def DescriptiveComplexity.JSBnd {A : Type} [FirstOrder.Language.jobSeq.Structure A] (a0 : A) :

bnd p: the penalty bound has bit 1 at position p.

Equations

DescriptiveComplexity.JSBnd a0 = FirstOrder.Language.Structure.RelMap FirstOrder.Language.jsBnd ![a0]

Instances For

Dependency graph

def DescriptiveComplexity.JSTime {A : Type} [FirstOrder.Language.jobSeq.Structure A] (a0 a1 : A) :

time j p: the execution time of j has bit 1 at position p.

Equations

DescriptiveComplexity.JSTime a0 a1 = FirstOrder.Language.Structure.RelMap FirstOrder.Language.jsTime ![a0, a1]

Instances For

Dependency graph

def DescriptiveComplexity.JSPosn {A : Type} [FirstOrder.Language.jobSeq.Structure A] (a0 : A) :

posn p: p is a bit position.

Equations

DescriptiveComplexity.JSPosn a0 = FirstOrder.Language.Structure.RelMap FirstOrder.Language.jsPosn ![a0]

Instances For

Dependency graph

def DescriptiveComplexity.JSLe {A : Type} [FirstOrder.Language.jobSeq.Structure A] (a0 a1 : A) :

le a b: the linear order carrying the place values.

Equations

DescriptiveComplexity.JSLe a0 a1 = FirstOrder.Language.Structure.RelMap FirstOrder.Language.jsLe ![a0, a1]

Instances For

Dependency graph

def DescriptiveComplexity.JSDline {A : Type} [FirstOrder.Language.jobSeq.Structure A] (a0 a1 : A) :

dline j p: the deadline of j has bit 1 at position p.

Equations

DescriptiveComplexity.JSDline a0 a1 = FirstOrder.Language.Structure.RelMap FirstOrder.Language.jsDline ![a0, a1]

Instances For

Dependency graph

def DescriptiveComplexity.JSPen {A : Type} [FirstOrder.Language.jobSeq.Structure A] (a0 a1 : A) :

pen j p: the penalty of j has bit 1 at position p.

Equations

DescriptiveComplexity.JSPen a0 a1 = FirstOrder.Language.Structure.RelMap FirstOrder.Language.jsPen ![a0, a1]

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.JSTimeVal {A : Type} [FirstOrder.Language.jobSeq.Structure A] (j : A) :

The execution time of a job, decoded.

Equations

DescriptiveComplexity.JSTimeVal j = DescriptiveComplexity.binNum DescriptiveComplexity.JSLe DescriptiveComplexity.JSPosn (DescriptiveComplexity.JSTime j)

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.JSDlineVal {A : Type} [FirstOrder.Language.jobSeq.Structure A] (j : A) :

The deadline of a job, decoded.

Equations

DescriptiveComplexity.JSDlineVal j = DescriptiveComplexity.binNum DescriptiveComplexity.JSLe DescriptiveComplexity.JSPosn (DescriptiveComplexity.JSDline j)

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.JSPenVal {A : Type} [FirstOrder.Language.jobSeq.Structure A] (j : A) :

The penalty of a job, decoded.

Equations

DescriptiveComplexity.JSPenVal j = DescriptiveComplexity.binNum DescriptiveComplexity.JSLe DescriptiveComplexity.JSPosn (DescriptiveComplexity.JSPen j)

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.JSBound (A : Type) [FirstOrder.Language.jobSeq.Structure A] :

The penalty bound of an instance, decoded.

Equations

DescriptiveComplexity.JSBound A = DescriptiveComplexity.binNum DescriptiveComplexity.JSLe DescriptiveComplexity.JSPosn DescriptiveComplexity.JSBnd

Instances For

Dependency graph

Schedules #

noncomputable def DescriptiveComplexity.JSCompletion {A : Type} [FirstOrder.Language.jobSeq.Structure A] (sched : A → A → Prop) (j : A) :

The completion time of a job under a schedule: the total execution time of the jobs scheduled at or before it.

Equations

DescriptiveComplexity.JSCompletion sched j = ∑ᶠ (i : A) (_ : i ∈ {i : A | DescriptiveComplexity.JSJob i ∧ sched i j}), DescriptiveComplexity.JSTimeVal i

Instances For

Dependency graph

def DescriptiveComplexity.JSLate {A : Type} [FirstOrder.Language.jobSeq.Structure A] (sched : A → A → Prop) (j : A) :

A job is late under a schedule when it completes after its deadline.

Equations

DescriptiveComplexity.JSLate sched j = (DescriptiveComplexity.JSDlineVal j < DescriptiveComplexity.JSCompletion sched j)

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.JSPenalty {A : Type} [FirstOrder.Language.jobSeq.Structure A] (sched : A → A → Prop) :

The total penalty of the jobs a schedule leaves late.

Equations

DescriptiveComplexity.JSPenalty sched = ∑ᶠ (j : A) (_ : j ∈ {j : A | DescriptiveComplexity.JSJob j ∧ DescriptiveComplexity.JSLate sched j}), DescriptiveComplexity.JSPenVal j

Instances For

Dependency graph

The problem #

def DescriptiveComplexity.HasGoodSchedule (A : Type) [FirstOrder.Language.jobSeq.Structure A] :

A job-sequencing instance is a yes-instance when its order is a linear order and some schedule – some linear order on the universe – leaves late only jobs whose penalties sum to at most the bound.

Equations

One or more equations did not get rendered due to their size.

Instances For

Dependency graph

theorem DescriptiveComplexity.hasGoodSchedule_iso {A B : Type} [FirstOrder.Language.jobSeq.Structure A] [FirstOrder.Language.jobSeq.Structure B] (e : FirstOrder.Language.jobSeq.Equiv A B) :

HasGoodSchedule A ↔ HasGoodSchedule B

Being a yes-instance of job sequencing is isomorphism-invariant.

Dependency graph

def DescriptiveComplexity.JobSequencing :

DecisionProblem FirstOrder.Language.jobSeq

SEQUENCING, as a problem on job-sequencing instances: is there a schedule whose late jobs carry a total penalty at most the bound? The times, deadlines, penalties and bound are written in binary, which is what makes the problem NP-hard rather than polynomial-time.

Equations

DescriptiveComplexity.JobSequencing = { Holds := fun (A : Type) (inst : FirstOrder.Language.jobSeq.Structure A) => DescriptiveComplexity.HasGoodSchedule A, iso_invariant := ⋯ }

Instances For

Dependency graph