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.

inductive FirstOrder.Language.zeroOneIPRel : ℕ → Type

Relation symbols of 0-1 integer programs.

• 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.

@[instance_reducible]

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

Equations

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

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.

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 }

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

@[reducible, inline]

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

The column symbol.

Equations

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

@[reducible, inline]

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

The row symbol.

Equations

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

@[reducible, inline]

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

The position symbol.

Equations

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

@[reducible, inline]

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

The entry symbol.

Equations

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

@[reducible, inline]

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

The right-hand side symbol.

Equations

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

@[reducible, inline]

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

The order symbol.

Equations

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

The shorthands of the vocabulary

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

Being a column, that is, a 0-1 variable.

Equations

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

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

Being a row, that is, an equation.

Equations

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

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

Being a bit position.

Equations

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

def DescriptiveComplexity.IPCoef {A : Type} [FirstOrder.Language.zeroOneIP.Structure A] (r j p : A) : Prop

The bit of an entry at a position.

Equations

• DescriptiveComplexity.IPCoef r j p = FirstOrder.Language.Structure.RelMap FirstOrder.Language.ipCoef ![r, j, p]

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

The bits of a right-hand side.

Equations

• DescriptiveComplexity.IPRhs r p = FirstOrder.Language.Structure.RelMap FirstOrder.Language.ipRhs ![r, p]

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

The order carrying the place values.

Equations

• DescriptiveComplexity.IPLe a b = FirstOrder.Language.Structure.RelMap FirstOrder.Language.ipLe ![a, b]

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 := ⋯ }