0-1 integer programming: definition

0-1 INTEGER PROGRAMMING (Karp 1972): given a matrix C and a vector d, is there a 0-1 vector x with C x = d? It is the multi-row form of Knapsack, and like it is written in binary (DescriptiveComplexity.Numbers.BinRel), 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.zeroOneIP carries

• col j, row r and posn p, the columns (the 0-1 variables), the rows (the equations) and the bit positions;
• coef r j p, “the entry of row r in column j has bit 1 at position p”, the only ternary symbol of the catalog;
• rhs r p, the bits of the right-hand side of row r;
• le, a linear order fixing the place values, folded into the yes-instances (DescriptiveComplexity.IsLinOrd) as everywhere in the binary encoding.

Entries are natural numbers: Karp states the problem over the integers, and the restriction formalized here is the one his reduction produces – a special case, so its NP-hardness gives his problem's a fortiori, while membership in NP for signed entries would need the two sides of each equation weighed separately and is not claimed.

@[reducible, inline]

abbrev FirstOrder.Language.ipRhs : Language.zeroOneIP.Relations 2

rhs r p: the right-hand side of row r has bit 1 at p.

Equations

• FirstOrder.Language.ipRhs = FirstOrder.Language.zeroOneIPRel.rhs

inductive FirstOrder.Language.zeroOneIPRel : ℕ → Type

The relation symbols of the language.

• col : zeroOneIPRel 1

  col j: j is a column, that is, a 0-1 variable.

• row : zeroOneIPRel 1

  row r: r is a row, that is, an equation.

• posn : zeroOneIPRel 1

  posn p: p is a bit position.

• coef : zeroOneIPRel 3

  coef r j p: the entry of row r in column j has bit 1 at p.

• rhs : zeroOneIPRel 2

  rhs r p: the right-hand side of row r has bit 1 at p.

• le : zeroOneIPRel 2

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

@[reducible, inline]

abbrev FirstOrder.Language.ipRow : Language.zeroOneIP.Relations 1

row r: r is a row, that is, an equation.

Equations

• FirstOrder.Language.ipRow = FirstOrder.Language.zeroOneIPRel.row

def FirstOrder.Language.instDecidableEqZeroOneIPRel.decEq {a✝ : ℕ} (x✝ x✝¹ : zeroOneIPRel a✝) : Decidable (x✝ = x✝¹)

Equations

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

@[reducible, inline]

abbrev FirstOrder.Language.ipCol : Language.zeroOneIP.Relations 1

col j: j is a column, that is, a 0-1 variable.

Equations

• FirstOrder.Language.ipCol = FirstOrder.Language.zeroOneIPRel.col

@[reducible, inline]

abbrev FirstOrder.Language.ipPosn : Language.zeroOneIP.Relations 1

posn p: p is a bit position.

Equations

• FirstOrder.Language.ipPosn = FirstOrder.Language.zeroOneIPRel.posn

@[instance_reducible]

instance FirstOrder.Language.instDecidableEqZeroOneIPRel {a✝ : ℕ} : DecidableEq (zeroOneIPRel a✝)

Equations

• FirstOrder.Language.instDecidableEqZeroOneIPRel = FirstOrder.Language.instDecidableEqZeroOneIPRel.decEq

def FirstOrder.Language.zeroOneIP : Language

The relational language of 0-1 integer programs: columns, rows and bit positions, the bits of each entry and of each right-hand side, and a linear order.

Equations

• FirstOrder.Language.zeroOneIP = { Functions := fun (x : ℕ) => Empty, Relations := FirstOrder.Language.zeroOneIPRel }

@[reducible, inline]

abbrev FirstOrder.Language.ipLe : Language.zeroOneIP.Relations 2

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

Equations

• FirstOrder.Language.ipLe = FirstOrder.Language.zeroOneIPRel.le

@[reducible, inline]

abbrev FirstOrder.Language.ipCoef : Language.zeroOneIP.Relations 3

coef r j p: the entry of row r in column j has bit 1 at p.

Equations

• FirstOrder.Language.ipCoef = FirstOrder.Language.zeroOneIPRel.coef

instance FirstOrder.Language.instIsRelationalZeroOneIP : Language.zeroOneIP.IsRelational

The shorthands of the vocabulary

def DescriptiveComplexity.IPCoef {A : Type} [FirstOrder.Language.zeroOneIP.Structure A] (a0 a1 a2 : A) : Prop

coef r j p: the entry of row r in column j has bit 1 at p.

Equations

• DescriptiveComplexity.IPCoef a0 a1 a2 = FirstOrder.Language.Structure.RelMap FirstOrder.Language.ipCoef ![a0, a1, a2]

def DescriptiveComplexity.IPRhs {A : Type} [FirstOrder.Language.zeroOneIP.Structure A] (a0 a1 : A) : Prop

rhs r p: the right-hand side of row r has bit 1 at p.

Equations

• DescriptiveComplexity.IPRhs a0 a1 = FirstOrder.Language.Structure.RelMap FirstOrder.Language.ipRhs ![a0, a1]

def DescriptiveComplexity.IPRow {A : Type} [FirstOrder.Language.zeroOneIP.Structure A] (a0 : A) : Prop

row r: r is a row, that is, an equation.

Equations

• DescriptiveComplexity.IPRow a0 = FirstOrder.Language.Structure.RelMap FirstOrder.Language.ipRow ![a0]

def DescriptiveComplexity.IPLe {A : Type} [FirstOrder.Language.zeroOneIP.Structure A] (a0 a1 : A) : Prop

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

Equations

• DescriptiveComplexity.IPLe a0 a1 = FirstOrder.Language.Structure.RelMap FirstOrder.Language.ipLe ![a0, a1]

def DescriptiveComplexity.IPPosn {A : Type} [FirstOrder.Language.zeroOneIP.Structure A] (a0 : A) : Prop

posn p: p is a bit position.

Equations

• DescriptiveComplexity.IPPosn a0 = FirstOrder.Language.Structure.RelMap FirstOrder.Language.ipPosn ![a0]

def DescriptiveComplexity.IPCol {A : Type} [FirstOrder.Language.zeroOneIP.Structure A] (a0 : A) : Prop

col j: j is a column, that is, a 0-1 variable.

Equations

• DescriptiveComplexity.IPCol a0 = FirstOrder.Language.Structure.RelMap FirstOrder.Language.ipCol ![a0]

noncomputable def DescriptiveComplexity.IPCoefVal {A : Type} [FirstOrder.Language.zeroOneIP.Structure A] (r j : A) : ℕ

The entry of a row in a column, decoded.

Equations

• DescriptiveComplexity.IPCoefVal r j = DescriptiveComplexity.binNum DescriptiveComplexity.IPLe DescriptiveComplexity.IPPosn (DescriptiveComplexity.IPCoef r j)

noncomputable def DescriptiveComplexity.IPRhsVal {A : Type} [FirstOrder.Language.zeroOneIP.Structure A] (r : A) : ℕ

The right-hand side of a row, decoded.

Equations

• DescriptiveComplexity.IPRhsVal r = DescriptiveComplexity.binNum DescriptiveComplexity.IPLe DescriptiveComplexity.IPPosn (DescriptiveComplexity.IPRhs r)

The problem

def DescriptiveComplexity.HasZeroOneSolution (A : Type) [FirstOrder.Language.zeroOneIP.Structure A] : Prop

A 0-1 integer program is a yes-instance when its order is a linear order and some set of columns – the variables set to 1 – makes every equation hold.

Equations

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

theorem DescriptiveComplexity.hasZeroOneSolution_iso {A B : Type} [FirstOrder.Language.zeroOneIP.Structure A] [FirstOrder.Language.zeroOneIP.Structure B] (e : FirstOrder.Language.zeroOneIP.Equiv A B) : HasZeroOneSolution A ↔ HasZeroOneSolution B

Being a yes-instance of 0-1 integer programming is isomorphism-invariant.

def DescriptiveComplexity.ZeroOneIP : DecisionProblem FirstOrder.Language.zeroOneIP

0-1 INTEGER PROGRAMMING, as a problem on 0-1 integer programs: is there a set of columns whose entries sum, row by row, exactly to the right-hand sides? The entries are written in binary, which is what makes the problem NP-hard rather than polynomial-time.

Equations

• DescriptiveComplexity.ZeroOneIP = { Holds := fun (A : Type) (inst : FirstOrder.Language.zeroOneIP.Structure A) => DescriptiveComplexity.HasZeroOneSolution A, iso_invariant := ⋯ }