0-1 integer programming

Abbreviation0-1 integer programming instances#✓fully proved

A 0-1 integer programming instance is a triple \((n, A, b)\) consisting of a natural number \(n\) (the number of variables), a coefficient matrix \(A\) given as a list of rows, each row a list of pairs of natural numbers, and a right-hand side \(b\) given as a list of pairs of natural numbers. A pair \((p, q)\) is read as the integer \(p - q\), so coefficients and right-hand side entries are stored by positive and negative parts.

abbrev ZeroOneILPInstance := ℕ × List (List (ℕ × ℕ)) × List (ℕ × ℕ)

Used by 3

Used byWell-formed 0-1 integer programming instances · 0-1 integer programming feasibility as a decision problem · Feasible 0-1 integer programs

DefinitionWell-formed 0-1 integer programming instances#✓fully proved

A 0-1 integer programming instance \((n, A, b)\) is well formed when the right-hand side list \(b\) has as many entries as there are rows of the coefficient matrix \(A\), and every row of \(A\) has exactly \(n\) entries.

def WellFormed (i : ZeroOneILPInstance) : Prop :=
  i.2.1.length = i.2.2.length ∧ ∀ row ∈ i.2.1, row.length = i.1

Uses 1 · Used by 1

Statement uses0-1 integer programming instances

Used by0-1 integer programming feasibility as a decision problem

DefinitionFeasible 0-1 integer programs#✓fully proved

Let \((n, A, b)\) be a 0-1 integer programming instance whose coefficient matrix has the rows \(A_0, \dots, A_{m-1}\), with list entries indexed from \(0\). For \(r < m\) and \(j < n\), let \(a_{rj}\) be the integer \(p - q\) if row \(A_r\) has a \(j\)-th entry \((p, q)\), and \(a_{rj} = 0\) otherwise; let \(b_r\) be the integer \(p' - q'\) if \(b\) has an \(r\)-th entry \((p', q')\), and \(b_r = 0\) otherwise. The instance is feasible when there is \(x \in \{0, 1\}^n\) such that \(\sum_{j < n} a_{rj} x_j \le b_r\) in \(\mathbb{Z}\) for every \(r < m\).

def ZeroOneILPFeasible
    (i : ZeroOneILPInstance) : Prop :=
  ∃ x : List Bool, x.length = i.1 ∧
    ∀ r < i.2.1.length,
      ((Finset.range i.1).sum (fun j =>
        ((((i.2.1.getD r []).getD j (0, 0)).1 : ℤ) -
        (((i.2.1.getD r []).getD j (0, 0)).2 : ℤ)) *
        (if x.getD j false then (1 : ℤ) else 0))) ≤
      (((i.2.2.getD r (0, 0)).1 : ℤ) - ((i.2.2.getD r (0, 0)).2 : ℤ))

Uses 1 · Used by 1

Statement uses0-1 integer programming instances

Used by0-1 integer programming feasibility as a decision problem

Definition0-1 integer programming feasibility as a decision problem#✓fully proved

The decision problem 0-1 INTEGER PROGRAMMING FEASIBILITY accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to a 0-1 integer programming instance that is well formed and feasible; it rejects every bitstring that does not decode to such an instance.

noncomputable def zeroOneILPDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := ZeroOneILPInstance) x with
  | some i => decide (WellFormed i ∧ ZeroOneILPFeasible i)
  | none => false

Uses 12 · Used by 1

Statement usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Well-formed 0-1 integer programming instances · Feasible 0-1 integer programs · 0-1 integer programming instances · Decision problems

Used by0-1 INTEGER PROGRAMMING FEASIBILITY is NP-complete

Theorem0-1 INTEGER PROGRAMMING FEASIBILITY is NP-complete#●ready to prove

The decision problem 0-1 INTEGER PROGRAMMING FEASIBILITY belongs to NP, and every decision problem in NP has a polynomial-time many-one reduction to it.

public theorem_wanted zeroOneILP_npComplete :
    zeroOneILPDec ∈ MetaMathlibExt.ComplexityTheory.NP ∧
      ∀ L : MetaMathlibExt.ComplexityTheory.DecisionProblem,
        L ∈ MetaMathlibExt.ComplexityTheory.NP →
          Cslib.CookLevin.PolyManyOneRed L zeroOneILPDec

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), 0-1 INTEGER PROGRAMMING; R. M. Karp, "Reducibility among combinatorial problems" (1972).

Uses 5

Statement usesPolynomial-time many-one reduction · 0-1 integer programming feasibility as a decision problem · Complexity classes · Decision problems · The complexity class NP

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.