Job sequencing is NP-hard

Karp derives SEQUENCING from Partition: one job per number, every deadline and the bound both Σ / 2. That reduction does not transfer here, because a first-order interpretation has to write the deadline and the bound in binary, and half of a total is an iterated sum – the same obstruction that ruled out Karp's padding for Partition, one step further along.

The way out is to make the gadget's own total a number it can write. By DescriptiveComplexity.hasGoodSchedule_iff_exists_half, with a common deadline D, penalties equal to execution times, jobs weighing 2 D in total and the bound equal to D, a good schedule is exactly a set of jobs weighing D: Partition's condition. So it is enough to build a balanced-split gadget all of whose digit blocks total an even number, and then to let D be the digit-wise half – which is first-order, one bit per block, while Σ = 2 D holds by DescriptiveComplexity.digitNum_mul_left.

The gadget

One digit block per variable and one per clause, in base 2 ^ (3 |A|), and one job per literal and per slack occurrence (DescriptiveComplexity.SatOcc.Mid), as in the reduction to Partition:

• the block of a variable totals 2, so a balanced split takes exactly one of its two literals: it is an assignment;
• the block of a clause of width w totals w + (w − 2) = 2 (w − 1), so a balanced split takes between 1 and w − 1 true literals: exactly not-all-equal satisfaction.

Every block total is 2 (w − 1), hence D has digit w − 1 there. That is a single bit per block only when w − 1 is a power of two, so – unlike Partition, which never had to write the number to reach – the width has to be bounded: the source is NAE-3SAT, and w − 1 ∈ {1, 2} is the bit at the base of the block, or the one just above it.

Positions are pairs of a block and an index inside it, as in the reduction to Partition, but the key ordering them (DescriptiveComplexity.JSRed.leKF) puts the index last: the positions of a block are then consecutive, so the bit just above a block's base is worth exactly twice it (DescriptiveComplexity.JSRed.bitRank_jPos), which is what lets the deadline carry the digit 2.

The degenerate instances

The width bound of NAE-3SAT is folded into its yes-instances, and a clause of width at most one is not-all-equal unsatisfiable, so both kinds of degeneracy (DescriptiveComplexity.JSRed.Deg: a wide clause, or a short one) mark a no-instance of the source. The gadget gates the deadline and the bound on their absence: a degenerate input is sent to an instance of deadline 0 and bound 0, which no schedule can meet, every literal job having a positive execution time.

The degenerate inputs

Two first-order tests carve out the instances the gadget refuses to encode: a clause with four distinct occurrences – DescriptiveComplexity.Wide, the negation of the width bound of 3SAT – and a clause with at most one, which is not-all-equal unsatisfiable. A clause has two occurrences exactly when one of them is not the first one (DescriptiveComplexity.SatOcc.Chained), which is how the second test avoids counting.

def DescriptiveComplexity.JSRed.Short {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (c : A) : Prop

A short clause: one with at most one occurrence, that is, one none of whose occurrences is preceded by another.

Equations

• DescriptiveComplexity.JSRed.Short c = (DescriptiveComplexity.SatOcc.IsCl c ∧ ∀ (x : A) (s : Bool), ¬DescriptiveComplexity.SatOcc.Chained c x s)

def DescriptiveComplexity.JSRed.Deg (A : Type) [FirstOrder.Language.sat.Structure A] [LinearOrder A] : Prop

A degenerate input: one with a wide clause or a short one. Both mark a no-instance of NAE-3SAT, and the gadget sends them to an instance no schedule can serve.

Equations

• DescriptiveComplexity.JSRed.Deg A = (DescriptiveComplexity.ThreeSatToSat.Wide A ∨ ∃ (c : A), DescriptiveComplexity.JSRed.Short c)

theorem DescriptiveComplexity.JSRed.not_naeProper_of_short {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {c : A} (hc : Short c) (ν : A → Prop) : ¬NAEProper ν

A short clause is not-all-equal unsatisfiable: its true and its false literal would be one and the same occurrence.

theorem DescriptiveComplexity.JSRed.midSet_subsingleton {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] (hwidth : WidthAtMostThree A) {c x y : A} {s t : Bool} (hx : SatOcc.Mid c x s) (hy : SatOcc.Mid c y t) : x = y ∧ s = t

A clause has at most one slack occurrence under the width bound: its first occurrence, its last one and two distinct slack ones would be four.

theorem DescriptiveComplexity.JSRed.exists_chained_of_not_deg {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (hd : ¬Deg A) {c : A} (hc : SatOcc.IsCl c) : ∃ (x : A) (s : Bool), SatOcc.Chained c x s

A clause of a non-degenerate input has an occurrence which is not the first one, hence at least two occurrences.

The tags

inductive DescriptiveComplexity.JSRed.JTag : Type

Tags of the reduction. The jobs are those of the literals and of the slack occurrences; the positions carry a block – a variable block (false) or a clause block (true) – and an index inside it, of which Fin 3 are enough to keep the base above every digit and to leave room for the deadline's bit.

• lit (s : Bool) : JTag

  The job of the literal (x, s); its tuple is (x, ⊥).

• slk (s : Bool) : JTag

  The job of the slack occurrence (x, s) of c; its tuple is (c, x).

• pos (k : Bool) (f : Fin 3) : JTag

  The f-th position of the block (k, e); its tuple is (e, y).

@[instance_reducible]

instance DescriptiveComplexity.JSRed.instDecidableEqJTag : DecidableEq JTag

Equations

• DescriptiveComplexity.JSRed.instDecidableEqJTag = DescriptiveComplexity.JSRed.instDecidableEqJTag.decEq

def DescriptiveComplexity.JSRed.instDecidableEqJTag.decEq (x✝ x✝¹ : JTag) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.JSRed.instDecidableEqJTag.decEq (DescriptiveComplexity.JSRed.JTag.lit a) (DescriptiveComplexity.JSRed.JTag.lit b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• DescriptiveComplexity.JSRed.instDecidableEqJTag.decEq (DescriptiveComplexity.JSRed.JTag.lit s) (DescriptiveComplexity.JSRed.JTag.slk s_1) = isFalse ⋯
• DescriptiveComplexity.JSRed.instDecidableEqJTag.decEq (DescriptiveComplexity.JSRed.JTag.lit s) (DescriptiveComplexity.JSRed.JTag.pos k f) = isFalse ⋯
• DescriptiveComplexity.JSRed.instDecidableEqJTag.decEq (DescriptiveComplexity.JSRed.JTag.slk s) (DescriptiveComplexity.JSRed.JTag.lit s_1) = isFalse ⋯
• DescriptiveComplexity.JSRed.instDecidableEqJTag.decEq (DescriptiveComplexity.JSRed.JTag.slk a) (DescriptiveComplexity.JSRed.JTag.slk b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• DescriptiveComplexity.JSRed.instDecidableEqJTag.decEq (DescriptiveComplexity.JSRed.JTag.slk s) (DescriptiveComplexity.JSRed.JTag.pos k f) = isFalse ⋯
• DescriptiveComplexity.JSRed.instDecidableEqJTag.decEq (DescriptiveComplexity.JSRed.JTag.pos k f) (DescriptiveComplexity.JSRed.JTag.lit s) = isFalse ⋯
• DescriptiveComplexity.JSRed.instDecidableEqJTag.decEq (DescriptiveComplexity.JSRed.JTag.pos k f) (DescriptiveComplexity.JSRed.JTag.slk s) = isFalse ⋯

@[instance_reducible]

instance DescriptiveComplexity.JSRed.instFintypeJTag : Fintype JTag

Equations

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

instance DescriptiveComplexity.JSRed.instNonemptyJTag : Nonempty JTag

def DescriptiveComplexity.JSRed.tagRk : JTag → ℕ

The rank of a tag: the jobs first, then the positions of the variable blocks, then those of the clause blocks. It is the leading component of the key, so it separates jobs from positions and variable blocks from clause blocks.

Equations

• DescriptiveComplexity.JSRed.tagRk (DescriptiveComplexity.JSRed.JTag.lit false) = 0
• DescriptiveComplexity.JSRed.tagRk (DescriptiveComplexity.JSRed.JTag.lit true) = 1
• DescriptiveComplexity.JSRed.tagRk (DescriptiveComplexity.JSRed.JTag.slk false) = 2
• DescriptiveComplexity.JSRed.tagRk (DescriptiveComplexity.JSRed.JTag.slk true) = 3
• DescriptiveComplexity.JSRed.tagRk (DescriptiveComplexity.JSRed.JTag.pos false f) = 4
• DescriptiveComplexity.JSRed.tagRk (DescriptiveComplexity.JSRed.JTag.pos true f) = 5

def DescriptiveComplexity.JSRed.subRk : JTag → ℕ

The rank of a tag inside a block: the index of a position, and 0 for the jobs, which no block holds. Unlike the reduction to Partition, this is the last component of the key, so that consecutive indices are consecutive positions and the deadline can carry the digit 2.

Equations

• DescriptiveComplexity.JSRed.subRk (DescriptiveComplexity.JSRed.JTag.pos k f) = ↑f
• DescriptiveComplexity.JSRed.subRk x✝ = 0

theorem DescriptiveComplexity.JSRed.tag_ext {t t' : JTag} (h₁ : tagRk t = tagRk t') (h₂ : subRk t = subRk t') : t = t'

The two ranks together determine the tag.

The interpretation

noncomputable def DescriptiveComplexity.JSRed.minF {α : Type} (x : α) : SatOcc.satOrd.Formula α

A minimum of the order, as a formula over the ordered expansion of the vocabulary of CNF instances.

Equations

• DescriptiveComplexity.JSRed.minF x = DescriptiveComplexity.botF x

@[simp]

theorem DescriptiveComplexity.JSRed.realize_minF {α A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {v : α → A} {x : α} : (minF x).Realize v ↔ IsBot (v x)

noncomputable def DescriptiveComplexity.JSRed.hasChainedF {α : Type} (c : α) : SatOcc.satOrd.Formula α

c has an occurrence which is not its first one, as a formula.

Equations

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

@[simp]

theorem DescriptiveComplexity.JSRed.realize_hasChainedF {α A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {v : α → A} {c : α} : (hasChainedF c).Realize v ↔ ∃ (x : A) (s : Bool), SatOcc.Chained (v c) x s

noncomputable def DescriptiveComplexity.JSRed.hasMidF {α : Type} (c : α) : SatOcc.satOrd.Formula α

c has a slack occurrence, as a formula: the width-three test, a clause of a non-degenerate input having width two or three.

Equations

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

@[simp]

theorem DescriptiveComplexity.JSRed.realize_hasMidF {α A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {v : α → A} {c : α} : (hasMidF c).Realize v ↔ ∃ (x : A) (s : Bool), SatOcc.Mid (v c) x s

noncomputable def DescriptiveComplexity.JSRed.shortF {α : Type} (c : α) : SatOcc.satOrd.Formula α

c is a short clause, as a formula.

Equations

• DescriptiveComplexity.JSRed.shortF c = DescriptiveComplexity.SatOcc.clF c ⊓ FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.JSRed.hasChainedF c)

@[simp]

theorem DescriptiveComplexity.JSRed.realize_shortF {α A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {v : α → A} {c : α} : (shortF c).Realize v ↔ Short (v c)

noncomputable def DescriptiveComplexity.JSRed.degF {α : Type} : SatOcc.satOrd.Formula α

The input is degenerate, as a (closed) formula.

Equations

• DescriptiveComplexity.JSRed.degF = DescriptiveComplexity.ThreeSatToSat.wideOrdF ⊔ FirstOrder.Language.Formula.iExs Unit (DescriptiveComplexity.JSRed.shortF (Sum.inr ()))

@[simp]

theorem DescriptiveComplexity.JSRed.realize_degF {α A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {v : α → A} : degF.Realize v ↔ Deg A

noncomputable def DescriptiveComplexity.JSRed.jobF : JTag → SatOcc.satOrd.Formula (Fin 1 × Fin 2)

Defining formula for the jobs: one per literal and one per slack occurrence.

Equations

• DescriptiveComplexity.JSRed.jobF (DescriptiveComplexity.JSRed.JTag.lit s) = DescriptiveComplexity.JSRed.minF (0, 1)
• DescriptiveComplexity.JSRed.jobF (DescriptiveComplexity.JSRed.JTag.slk s) = DescriptiveComplexity.SatOcc.midF s (0, 0) (0, 1)
• DescriptiveComplexity.JSRed.jobF (DescriptiveComplexity.JSRed.JTag.pos k f) = ⊥

def DescriptiveComplexity.JSRed.posnF : JTag → SatOcc.satOrd.Formula (Fin 1 × Fin 2)

Defining formula for the bit positions: every tagged pair is one.

Equations

• DescriptiveComplexity.JSRed.posnF (DescriptiveComplexity.JSRed.JTag.pos k f) = ⊤
• DescriptiveComplexity.JSRed.posnF x✝ = ⊥

noncomputable def DescriptiveComplexity.JSRed.bitF : JTag → JTag → SatOcc.satOrd.Formula (Fin 2 × Fin 2)

Defining formula for the bits of the execution times – and of the penalties, which equal them. Only the lowest position of a block – index 0, second coordinate a minimum – ever carries a bit.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.JSRed.bitF x✝¹ x✝ = ⊥

noncomputable def DescriptiveComplexity.JSRed.dbitF {α : Type} (k : Bool) (f : Fin 3) (e y : α) : SatOcc.satOrd.Formula α

Defining formula for the bits of the common deadline, over the tuple of a position: the digit 1 – the bit at the base of the block – in every variable block and in the block of a clause of width two, and the digit 2 – the bit one position up – in the block of a clause of width three. A degenerate input gets the deadline 0.

Equations

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

noncomputable def DescriptiveComplexity.JSRed.dlineF : JTag → JTag → SatOcc.satOrd.Formula (Fin 2 × Fin 2)

Defining formula for the bits of the deadline of a job: the job condition, and the deadline's bit pattern, the same for every job.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.JSRed.dlineF x✝¹ x✝ = ⊥

noncomputable def DescriptiveComplexity.JSRed.bndF : JTag → SatOcc.satOrd.Formula (Fin 1 × Fin 2)

Defining formula for the bits of the penalty bound: the deadline again.

Equations

• DescriptiveComplexity.JSRed.bndF (DescriptiveComplexity.JSRed.JTag.pos k f) = DescriptiveComplexity.JSRed.dbitF k f (0, 0) (0, 1)
• DescriptiveComplexity.JSRed.bndF x✝ = ⊥

def DescriptiveComplexity.JSRed.leKF (t t' : JTag) : SatOcc.satOrd.Formula (Fin 2 × Fin 2)

Defining formula for the order: the key (tag rank, first coordinate, second coordinate, index in the block), read lexicographically. The index comes last, so that the positions of a block are consecutive.

Equations

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

noncomputable def DescriptiveComplexity.JSRed.jInterp : FOInterpretation SatOcc.satOrd FirstOrder.Language.jobSeq JTag 2

The interpretation of a job-sequencing instance in a CNF structure: one job per literal and per slack occurrence, one block of 3 |A| positions per variable and per clause, every deadline and the bound the digit-wise half of the total execution time.

Equations

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

The points of the interpreted structure

def DescriptiveComplexity.JSRed.jPt {A : Type} (t : JTag) (w : Fin 2 → A) : jInterp.Map A

The point of tag t over the pair w.

Equations

• DescriptiveComplexity.JSRed.jPt t w = (t, w)

theorem DescriptiveComplexity.JSRed.jPt_surj {A : Type} (q : jInterp.Map A) : ∃ (t : JTag) (w : Fin 2 → A), q = jPt t w

theorem DescriptiveComplexity.JSRed.jPt_eq_iff {A : Type} {t t' : JTag} {w w' : Fin 2 → A} : jPt t w = jPt t' w' ↔ t = t' ∧ w = w'

@[simp]

theorem DescriptiveComplexity.JSRed.jPt_snd {A : Type} (t : JTag) (w : Fin 2 → A) (j : Fin 2) : (jPt t w).2 j = w j

theorem DescriptiveComplexity.JSRed.tuple₂_ext {A : Type} {w w' : Fin 2 → A} (h0 : w 0 = w' 0) (h1 : w 1 = w' 1) : w = w'

Two 2-tuples with the same coordinates are equal.

def DescriptiveComplexity.JSRed.jLit {A : Type} (a₀ : A) (s : Bool) (x : A) : jInterp.Map A

The job of the literal (x, s).

Equations

• DescriptiveComplexity.JSRed.jLit a₀ s x = DescriptiveComplexity.JSRed.jPt (DescriptiveComplexity.JSRed.JTag.lit s) ![x, a₀]

def DescriptiveComplexity.JSRed.jSlk {A : Type} (s : Bool) (c x : A) : jInterp.Map A

The job of the slack occurrence (x, s) of the clause c.

Equations

• DescriptiveComplexity.JSRed.jSlk s c x = DescriptiveComplexity.JSRed.jPt (DescriptiveComplexity.JSRed.JTag.slk s) ![c, x]

def DescriptiveComplexity.JSRed.jPos {A : Type} (f : Fin 3) (b : Bool × A) (y : A) : jInterp.Map A

The f-th position of the block b.

Equations

• DescriptiveComplexity.JSRed.jPos f b y = DescriptiveComplexity.JSRed.jPt (DescriptiveComplexity.JSRed.JTag.pos b.1 f) ![b.2, y]

def DescriptiveComplexity.JSRed.jLow {A : Type} (a₀ : A) (b : Bool × A) : jInterp.Map A

The lowest position of the block b.

Equations

• DescriptiveComplexity.JSRed.jLow a₀ b = DescriptiveComplexity.JSRed.jPos 0 b a₀

theorem DescriptiveComplexity.JSRed.jPos_eq {A : Type} (f : Fin 3) (k : Bool) (e y : A) : jPos f (k, e) y = jPt (JTag.pos k f) ![e, y]

theorem DescriptiveComplexity.JSRed.jLit_injective {A : Type} (a₀ : A) : Function.Injective fun (p : A × Bool) => jLit a₀ p.2 p.1

theorem DescriptiveComplexity.JSRed.jSlk_injective {A : Type} (c : A) : Function.Injective fun (p : A × Bool) => jSlk p.2 c p.1

theorem DescriptiveComplexity.JSRed.jPos_injective {A : Type} : Function.Injective fun (u : (Bool × A) × Fin 3 × A) => jPos u.2.1 u.1 u.2.2

theorem DescriptiveComplexity.JSRed.jLit_ne_jSlk {A : Type} (a₀ : A) (s s' : Bool) (x c y : A) : jLit a₀ s x ≠ jSlk s' c y

theorem DescriptiveComplexity.JSRed.jLit_eq_iff {A : Type} {a₀ : A} {s s' : Bool} {x x' : A} : jLit a₀ s x = jLit a₀ s' x' ↔ s = s' ∧ x = x'

theorem DescriptiveComplexity.JSRed.jSlk_eq_iff {A : Type} {s s' : Bool} {c c' x x' : A} : jSlk s c x = jSlk s' c' x' ↔ s = s' ∧ c = c' ∧ x = x'

Characterization of the interpreted relations

@[simp]

theorem DescriptiveComplexity.JSRed.jsJob_lit {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (s : Bool) (w : Fin 2 → A) : JSJob (jPt (JTag.lit s) w) ↔ IsBot (w 1)

@[simp]

theorem DescriptiveComplexity.JSRed.jsJob_slk {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (s : Bool) (w : Fin 2 → A) : JSJob (jPt (JTag.slk s) w) ↔ SatOcc.Mid (w 0) (w 1) s

@[simp]

theorem DescriptiveComplexity.JSRed.jsJob_pos {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (k : Bool) (f : Fin 3) (w : Fin 2 → A) : ¬JSJob (jPt (JTag.pos k f) w)

@[simp]

theorem DescriptiveComplexity.JSRed.jsPosn_pos {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (k : Bool) (f : Fin 3) (w : Fin 2 → A) : JSPosn (jPt (JTag.pos k f) w)

@[simp]

theorem DescriptiveComplexity.JSRed.jsPosn_lit {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (s : Bool) (w : Fin 2 → A) : ¬JSPosn (jPt (JTag.lit s) w)

@[simp]

theorem DescriptiveComplexity.JSRed.jsPosn_slk {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (s : Bool) (w : Fin 2 → A) : ¬JSPosn (jPt (JTag.slk s) w)

theorem DescriptiveComplexity.JSRed.jsPen_iff_jsTime {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (i q : jInterp.Map A) : JSPen i q ↔ JSTime i q

The penalty of a job is its execution time: the two are defined by the same formula.

def DescriptiveComplexity.JSRed.jKey {A : Type} (q : jInterp.Map A) : ℕ × A × A × ℕ

The key of a point: tag rank, first coordinate, second coordinate, index in the block.

Equations

• DescriptiveComplexity.JSRed.jKey q = (DescriptiveComplexity.JSRed.tagRk q.1, q.2 0, q.2 1, DescriptiveComplexity.JSRed.subRk q.1)

def DescriptiveComplexity.JSRed.keyLe {A : Type} [LinearOrder A] : ℕ × A × A × ℕ → ℕ × A × A × ℕ → Prop

The order of the interpreted structure, read lexicographically on the keys.

Equations

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

theorem DescriptiveComplexity.JSRed.jsLe_iff {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (t t' : JTag) (w w' : Fin 2 → A) : JSLe (jPt t w) (jPt t' w') ↔ keyLe (jKey (jPt t w)) (jKey (jPt t' w'))

theorem DescriptiveComplexity.JSRed.jKey_injective {A : Type} : Function.Injective jKey

theorem DescriptiveComplexity.JSRed.isLinOrd_jsLe {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] : IsLinOrd JSLe

The interpreted order is a linear order: the lexicographic order of the keys, which are pairwise distinct.

The blocks

def DescriptiveComplexity.JSRed.blkLe {A : Type} [LinearOrder A] : Bool × A → Bool × A → Prop

The order of the blocks: the variable blocks first, then the clause blocks, each group in the order of the input.

Equations

• DescriptiveComplexity.JSRed.blkLe = DescriptiveComplexity.lexRel (fun (x1 x2 : Bool) => x1 ≤ x2) fun (x1 x2 : A) => x1 ≤ x2

theorem DescriptiveComplexity.JSRed.isLinOrd_blkLe {A : Type} [LinearOrder A] : IsLinOrd blkLe

theorem DescriptiveComplexity.JSRed.blkLt_iff {A : Type} [LinearOrder A] {k k' : Bool} {x e : A} : blkLe (k, x) (k', e) ∧ (k, x) ≠ (k', e) ↔ k = k' ∧ x < e ∨ k = false ∧ k' = true

Being strictly below a block.

noncomputable def DescriptiveComplexity.JSRed.blkRank {A : Type} [LinearOrder A] (b : Bool × A) : ℕ

The rank of a block: how many blocks lie strictly below it.

Equations

• DescriptiveComplexity.JSRed.blkRank b = DescriptiveComplexity.bitRank DescriptiveComplexity.JSRed.blkLe (fun (x : Bool × A) => True) b

The bits, and the positions of a block

theorem DescriptiveComplexity.JSRed.jsTime_lit_pos {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (s : Bool) (w : Fin 2 → A) (k : Bool) (f : Fin 3) (w' : Fin 2 → A) : JSTime (jPt (JTag.lit s) w) (jPt (JTag.pos k f) w') ↔ f = 0 ∧ IsBot (w 1) ∧ IsBot (w' 1) ∧ if k = true then SatOcc.OccIn (w' 0) (w 0) s else w' 0 = w 0

theorem DescriptiveComplexity.JSRed.jsTime_slk_pos {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (s : Bool) (w : Fin 2 → A) (k : Bool) (f : Fin 3) (w' : Fin 2 → A) : JSTime (jPt (JTag.slk s) w) (jPt (JTag.pos k f) w') ↔ f = 0 ∧ k = true ∧ SatOcc.Mid (w 0) (w 1) s ∧ IsBot (w' 1) ∧ w' 0 = w 0

@[simp]

theorem DescriptiveComplexity.JSRed.jsTime_pos_left {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (k : Bool) (f : Fin 3) (w : Fin 2 → A) (q : jInterp.Map A) : ¬JSTime (jPt (JTag.pos k f) w) q

@[simp]

theorem DescriptiveComplexity.JSRed.jsTime_job_right {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (t : JTag) (w : Fin 2 → A) (s : Bool) (w' : Fin 2 → A) : ¬JSTime (jPt t w) (jPt (JTag.lit s) w') ∧ ¬JSTime (jPt t w) (jPt (JTag.slk s) w')

theorem DescriptiveComplexity.JSRed.eq_jLow_of_time {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) {i q : jInterp.Map A} (h : JSTime i q) (hq : JSPosn q) : ∃ (b : Bool × A), q = jLow a₀ b

Only the lowest position of a block ever carries a bit of an execution time.

The place values

theorem DescriptiveComplexity.JSRed.jsLe_pos_pos {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (k k' : Bool) (f f' : Fin 3) (w w' : Fin 2 → A) : JSLe (jPt (JTag.pos k f) w) (jPt (JTag.pos k' f') w') ↔ k = false ∧ k' = true ∨ k = k' ∧ (w 0 < w' 0 ∨ w 0 = w' 0 ∧ (w 1 < w' 1 ∨ w 1 = w' 1 ∧ ↑f ≤ ↑f'))

theorem DescriptiveComplexity.JSRed.bitRank_jPos {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {a₀ : A} (ha₀ : IsBot a₀) (f : Fin 3) (k : Bool) (e : A) : bitRank JSLe JSPosn (jPos f (k, e) a₀) = 3 * Nat.card A * blkRank (k, e) + ↑f

The block structure: the rank of the f-th position of a block is 3 |A| times the rank of the block, plus f, so its place value is (2 ^ (3 |A|)) ^ rank · 2 ^ f – one digit of base 2 ^ (3 |A|) per block, whose bits are the positions of that block, in order.

Execution times, as base-2 ^ (3 |A|) numbers

noncomputable def DescriptiveComplexity.JSRed.jbase (A : Type) [Finite A] : ℕ

The base: one digit per block, 3 |A| bits wide, which is above every digit the gadget writes, so digits never carry into the next block.

Equations

• DescriptiveComplexity.JSRed.jbase A = 2 ^ (3 * Nat.card A)

theorem DescriptiveComplexity.JSRed.jbase_pos {A : Type} [Finite A] : 0 < jbase A

theorem DescriptiveComplexity.JSRed.binNum_eq_digit {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {a₀ : A} (ha₀ : IsBot a₀) {p : jInterp.Map A → Prop} {sub : Bool × A → Prop} {g : Bool × A → Fin 3} (hp : ∀ (q : jInterp.Map A), JSPosn q ∧ p q ↔ ∃ (b : Bool × A), sub b ∧ q = jPos (g b) b a₀) : binNum JSLe JSPosn p = digitNum blkLe (fun (x : Bool × A) => True) (jbase A) fun (b : Bool × A) => if sub b then 2 ^ ↑(g b) else 0

A number written by one bit per block, the bit of a block sitting at the height g b inside it, is the base-2 ^ (3 |A|) number with digit 2 ^ g b there.

theorem DescriptiveComplexity.JSRed.jsTimeVal_eq {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {a₀ : A} (ha₀ : IsBot a₀) (i : jInterp.Map A) : JSTimeVal i = digitNum blkLe (fun (x : Bool × A) => True) (jbase A) fun (b : Bool × A) => if JSTime i (jLow a₀ b) then 1 else 0

Every execution time is read digit by digit: the digit of a block is 1 when the job carries a bit at its lowest position, and 0 otherwise.

theorem DescriptiveComplexity.JSRed.sum_times_eq {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {a₀ : A} (ha₀ : IsBot a₀) (S : jInterp.Map A → Prop) : ∑ᶠ (i : jInterp.Map A) (_ : i ∈ {i : jInterp.Map A | S i}), JSTimeVal i = digitNum blkLe (fun (x : Bool × A) => True) (jbase A) fun (b : Bool × A) => {i : jInterp.Map A | S i ∧ JSTime i (jLow a₀ b)}.ncard

The total execution time of a set of jobs, read digit by digit: the digit of a block is the number of selected jobs carrying a bit there.

Counting the jobs of a block

noncomputable def DescriptiveComplexity.JSRed.cnt {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (a₀ : A) (S : jInterp.Map A → Prop) (b : Bool × A) : ℕ

The number of selected jobs carrying a bit in a block: the digit that block contributes to the total execution time of the selection.

Equations

• DescriptiveComplexity.JSRed.cnt a₀ S b = {i : DescriptiveComplexity.JSRed.jInterp.Map A | S i ∧ DescriptiveComplexity.JSTime i (DescriptiveComplexity.JSRed.jLow a₀ b)}.ncard

theorem DescriptiveComplexity.JSRed.sum_times_eq_cnt {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {a₀ : A} (ha₀ : IsBot a₀) (S : jInterp.Map A → Prop) : ∑ᶠ (i : jInterp.Map A) (_ : i ∈ {i : jInterp.Map A | S i}), JSTimeVal i = digitNum blkLe (fun (x : Bool × A) => True) (jbase A) (cnt a₀ S)

theorem DescriptiveComplexity.JSRed.cnt_add_cnt {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] (a₀ : A) {S : jInterp.Map A → Prop} (hS : ∀ (i : jInterp.Map A), S i → JSJob i) (b : Bool × A) : cnt a₀ S b + cnt a₀ (fun (i : jInterp.Map A) => JSJob i ∧ ¬S i) b = cnt a₀ JSJob b

A selection and the jobs it leaves out split every digit.

Which jobs carry a bit in a block

theorem DescriptiveComplexity.JSRed.jLow_eq {A : Type} (a₀ : A) (k : Bool) (e : A) : jLow a₀ (k, e) = jPt (JTag.pos k 0) ![e, a₀]

theorem DescriptiveComplexity.JSRed.time_jLow_var {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (x : A) (i : jInterp.Map A) : JSTime i (jLow a₀ (false, x)) ↔ ∃ (s : Bool), i = jLit a₀ s x

The jobs carrying a bit in a variable block are the two literals of that variable.

theorem DescriptiveComplexity.JSRed.time_jLow_cls {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (c : A) (i : jInterp.Map A) : JSTime i (jLow a₀ (true, c)) ↔ (∃ (p : A × Bool), SatOcc.OccIn c p.1 p.2 ∧ i = jLit a₀ p.2 p.1) ∨ ∃ (p : A × Bool), SatOcc.Mid c p.1 p.2 ∧ i = jSlk p.2 c p.1

The jobs carrying a bit in a clause block are the literals occurring in the clause and its slack jobs.

The digits, block by block

theorem DescriptiveComplexity.JSRed.cnt_var {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (S : jInterp.Map A → Prop) (x : A) : cnt a₀ S (false, x) = {s : Bool | S (jLit a₀ s x)}.ncard

The digit of a variable block counts the selected literals of that variable.

theorem DescriptiveComplexity.JSRed.cnt_cls {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {a₀ : A} (ha₀ : IsBot a₀) (S : jInterp.Map A → Prop) (c : A) : cnt a₀ S (true, c) = {p : A × Bool | p ∈ SatOcc.OccSet c ∧ S (jLit a₀ p.2 p.1)}.ncard + {p : A × Bool | p ∈ SatOcc.MidSet c ∧ S (jSlk p.2 c p.1)}.ncard

The digit of a clause block counts the selected literals occurring in the clause and its selected slack jobs.

theorem DescriptiveComplexity.JSRed.cnt_job_var {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (x : A) : cnt a₀ JSJob (false, x) = 2

Every variable block totals two: a balanced split takes exactly one of the two literals of the variable.

theorem DescriptiveComplexity.JSRed.cnt_job_cls {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {a₀ : A} (ha₀ : IsBot a₀) (c : A) : cnt a₀ JSJob (true, c) = (SatOcc.OccSet c).ncard + (SatOcc.MidSet c).ncard

A clause block totals its occurrences plus its slack occurrences.

The digits stay below the base

theorem DescriptiveComplexity.JSRed.ncard_le_two_card {A : Type} [Finite A] (X : Set (A × Bool)) : X.ncard ≤ 2 * Nat.card A

theorem DescriptiveComplexity.JSRed.cnt_le {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] (a₀ : A) {S : jInterp.Map A → Prop} (hS : ∀ (i : jInterp.Map A), S i → JSJob i) (b : Bool × A) : cnt a₀ S b ≤ cnt a₀ JSJob b

A selection weighs at most as much as all the jobs, digit by digit.

theorem DescriptiveComplexity.JSRed.cnt_job_lt_jbase {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {a₀ : A} (ha₀ : IsBot a₀) (b : Bool × A) : cnt a₀ JSJob b < jbase A

No carry: every digit the gadget writes stays below the base, 3 |A| bits being more than the 4 |A| jobs a block can hold.

The deadline, and the bound

Both are the digit-wise half of the total execution time: one bit per block, at its base when the digit is 1 – a variable block, or the block of a clause of width two – and one position up when it is 2 – the block of a clause of width three.

noncomputable def DescriptiveComplexity.JSRed.dd {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (b : Bool × A) : ℕ

The digit the deadline writes in a block: 1 in every variable block, and in a clause block the width minus one. A degenerate input gets the deadline 0.

Equations

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

noncomputable def DescriptiveComplexity.JSRed.dval (A : Type) [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] : ℕ

The value of the deadline: the digit-wise half.

Equations

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

theorem DescriptiveComplexity.JSRed.dd_deg {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (hdeg : Deg A) (b : Bool × A) : dd b = 0

theorem DescriptiveComplexity.JSRed.dd_var {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (hdeg : ¬Deg A) (x : A) : dd (false, x) = 1

theorem DescriptiveComplexity.JSRed.dd_cls {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (hdeg : ¬Deg A) {c : A} (hc : SatOcc.IsCl c) : dd (true, c) = if ∃ (x : A) (s : Bool), SatOcc.Mid c x s then 2 else 1

theorem DescriptiveComplexity.JSRed.dd_not_cls {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (c : A) (hc : ¬SatOcc.IsCl c) : dd (true, c) = 0

theorem DescriptiveComplexity.JSRed.dd_le_two {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (b : Bool × A) : dd b ≤ 2

theorem DescriptiveComplexity.JSRed.dd_lt_jbase {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (b : Bool × A) : dd b < jbase A

noncomputable def DescriptiveComplexity.JSRed.dht {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (b : Bool × A) : Fin 3

Where the deadline writes its bit in a block: at the base, unless the block totals four.

Equations

• DescriptiveComplexity.JSRed.dht b = if DescriptiveComplexity.JSRed.dd b = 2 then 1 else 0

theorem DescriptiveComplexity.JSRed.dbit_pos {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (k : Bool) (f : Fin 3) (w : Fin 2 → A) : (∃ (b : Bool × A), dd b ≠ 0 ∧ jPt (JTag.pos k f) w = jPos (dht b) b a₀) ↔ IsBot (w 1) ∧ dd (k, w 0) ≠ 0 ∧ dht (k, w 0) = f

theorem DescriptiveComplexity.JSRed.realize_dbitF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} (k : Bool) (f : Fin 3) (e y : α) : (dbitF k f e y).Realize v ↔ IsBot (v y) ∧ (k = false ∧ f = 0 ∨ (k = true ∧ f = 0 ∧ SatOcc.IsCl (v e) ∧ ¬∃ (x : A) (s : Bool), SatOcc.Mid (v e) x s) ∨ k = true ∧ f = 1 ∧ SatOcc.IsCl (v e) ∧ ∃ (x : A) (s : Bool), SatOcc.Mid (v e) x s) ∧ ¬Deg A

What the deadline's bit pattern says, formula-free.

theorem DescriptiveComplexity.JSRed.jsBnd_pos {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (k : Bool) (f : Fin 3) (w : Fin 2 → A) : JSBnd (jPt (JTag.pos k f) w) ↔ IsBot (w 1) ∧ dd (k, w 0) ≠ 0 ∧ dht (k, w 0) = f

@[simp]

theorem DescriptiveComplexity.JSRed.jsBnd_lit {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (s : Bool) (w : Fin 2 → A) : ¬JSBnd (jPt (JTag.lit s) w)

@[simp]

theorem DescriptiveComplexity.JSRed.jsBnd_slk {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (s : Bool) (w : Fin 2 → A) : ¬JSBnd (jPt (JTag.slk s) w)

theorem DescriptiveComplexity.JSRed.jsBound_eq {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {a₀ : A} (ha₀ : IsBot a₀) : JSBound (jInterp.Map A) = dval A

The bound is the digit-wise half: it carries one bit per block, at the height its digit asks for.

theorem DescriptiveComplexity.JSRed.jsDline_iff {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (i q : jInterp.Map A) : JSDline i q ↔ JSJob i ∧ JSBnd q

The deadline of a job is the bound: the two are defined by the same bit pattern.

theorem DescriptiveComplexity.JSRed.jsDlineVal_eq {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {j : jInterp.Map A} (hj : JSJob j) : JSDlineVal j = JSBound (jInterp.Map A)

theorem DescriptiveComplexity.JSRed.jsPenVal_eq {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {j : jInterp.Map A} : JSPenVal j = JSTimeVal j

Every block totals twice the deadline's digit

theorem DescriptiveComplexity.JSRed.two_le_ncard_occSet {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] (hd : ¬Deg A) {c : A} (hc : SatOcc.IsCl c) : 2 ≤ (SatOcc.OccSet c).ncard

A clause of a non-degenerate input has at least two occurrences.

theorem DescriptiveComplexity.JSRed.ncard_midSet_le_one {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] (hwidth : WidthAtMostThree A) (c : A) : (SatOcc.MidSet c).ncard ≤ 1

Under the width bound a clause has at most one slack occurrence.

theorem DescriptiveComplexity.JSRed.two_mul_dd {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {a₀ : A} (ha₀ : IsBot a₀) (hd : ¬Deg A) (hwidth : WidthAtMostThree A) (b : Bool × A) : 2 * dd b = cnt a₀ JSJob b

The deadline is the digit-wise half: every block totals twice the digit the deadline writes there – 2 in a variable block, 2 (w − 1) in the block of a clause of width w ∈ {2, 3}.

theorem DescriptiveComplexity.JSRed.digits_eq_zero {A : Type} [LinearOrder A] [Finite A] {c : Bool × A → ℕ} (hc : ∀ (b : Bool × A), c b < jbase A) (h : digitNum blkLe (fun (x : Bool × A) => True) (jbase A) c = 0) (b : Bool × A) : c b = 0

A number written by digits below the base is zero only if all its digits are.

theorem DescriptiveComplexity.JSRed.sum_eq_dval_iff {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {a₀ : A} (ha₀ : IsBot a₀) {S : jInterp.Map A → Prop} (hS : ∀ (i : jInterp.Map A), S i → JSJob i) : ∑ᶠ (i : jInterp.Map A) (_ : i ∈ {i : jInterp.Map A | S i}), JSTimeVal i = dval A ↔ ∀ (b : Bool × A), cnt a₀ S b = dd b

A selection weighs the deadline exactly when it takes half of every digit, the digits of both staying below the base.

The selection made by an assignment

def DescriptiveComplexity.JSRed.splitSet {A : Type} (a₀ : A) (ν : A → Prop) (M : A → Set (A × Bool)) : jInterp.Map A → Prop

The jobs a not-all-equal assignment selects: those of the true literals, and the slack jobs chosen by M.

Equations

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

theorem DescriptiveComplexity.JSRed.splitSet_jLit {A : Type} {a₀ : A} {ν : A → Prop} {M : A → Set (A × Bool)} (s : Bool) (x : A) : splitSet a₀ ν M (jLit a₀ s x) ↔ SatOcc.LitTrue ν x s

theorem DescriptiveComplexity.JSRed.splitSet_jSlk {A : Type} {a₀ : A} {ν : A → Prop} {M : A → Set (A × Bool)} (s : Bool) (c x : A) : splitSet a₀ ν M (jSlk s c x) ↔ (x, s) ∈ M c

def DescriptiveComplexity.JSRed.TrueSet {A : Type} [FirstOrder.Language.sat.Structure A] (ν : A → Prop) (c : A) : Set (A × Bool)

The true occurrences of a clause under an assignment.

Equations

• DescriptiveComplexity.JSRed.TrueSet ν c = {p : A × Bool | p ∈ DescriptiveComplexity.SatOcc.OccSet c ∧ DescriptiveComplexity.SatOcc.LitTrue ν p.1 p.2}

Correctness of the reduction

theorem DescriptiveComplexity.JSRed.litTrue_iff_sel {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) {S : jInterp.Map A → Prop} (hbal : ∀ (b : Bool × A), 2 * cnt a₀ S b = cnt a₀ JSJob b) (x : A) (s : Bool) : S (jLit a₀ s x) ↔ SatOcc.LitTrue (fun (y : A) => S (jLit a₀ true y)) x s

A balanced split is an assignment: the two literals of a variable split its block, so exactly one of them is selected.

theorem DescriptiveComplexity.JSRed.exists_occ_selected {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {a₀ : A} (ha₀ : IsBot a₀) (hd : ¬Deg A) {S T : jInterp.Map A → Prop} (hcompl : ∀ (i : jInterp.Map A), JSJob i → (S i ↔ ¬T i)) (hbal : ∀ (b : Bool × A), cnt a₀ S b = cnt a₀ T b) {c : A} (hc : SatOcc.IsCl c) : ∃ p ∈ SatOcc.OccSet c, S (jLit a₀ p.2 p.1)

A balanced split satisfies every clause, not all equal: if no occurrence of a clause were selected, its slack – strictly fewer jobs than it has occurrences – would have to make up for all of them.

theorem DescriptiveComplexity.JSRed.naeThreeSatisfiable_iff_hasGoodSchedule (A : Type) [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : NAEThreeSatisfiable A ↔ HasGoodSchedule (jInterp.Map A)

Correctness of the reduction: a CNF structure is a yes-instance of NAE-3SAT iff the interpreted job-sequencing instance has a good schedule.

noncomputable def DescriptiveComplexity.nae3Sat_ordered_fo_reduction_jobSequencing : OrderedFOReduction NAE3SAT JobSequencing

NAE-3SAT ordered-FO-reduces to job sequencing: one job per literal and one per slack occurrence, one digit block of 3 |A| bit positions per variable and per clause, and a common deadline – the bound as well – equal to the digit-wise half of the total execution time. A variable block totals 2 and the block of a clause of width w totals 2 (w − 1), so a schedule whose late jobs stay within the bound is a balanced split of the blocks, that is, a not-all-equal satisfying assignment.

Equations

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