Integer programming in fixed dimension

DefinitionInteger from magnitude and sign#✓fully proved

A pair \((n, s)\) of a natural number \(n\) and a Boolean sign \(s\) decodes to the integer \(n\) if \(s\) is true and to \(-n\) if \(s\) is false.

def decodeIntILP (p : ℕ × Bool) : ℤ :=
  if p.2 then (p.1 : ℤ) else -(p.1 : ℤ)

Used by 1

Used byInteger linear-programming feasibility in fixed dimension

DefinitionInteger linear-programming feasibility in fixed dimension#✓fully proved

For a natural number \(d\), this decision problem accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring decoding, to a pair \((A, b)\) such that \(A\) is a list of rows, each a list of exactly \(d\) integers, \(b\) is a list of integers with as many entries as \(A\) has rows, and there is an integer vector \(y \in \mathbb{Z}^d\) with \(\sum_{j < d} A_{rj} y_j \le b_r\) for every row index \(r\). Each integer entry is given as a pair \((n, s)\) of a natural number and a sign, standing for \(n\) if \(s\) is true and \(-n\) otherwise. Every other bitstring is rejected.

noncomputable def ilpFixedDec (d : ℕ) :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := List (List (ℕ × Bool)) × List (ℕ × Bool)) x with
  | some i => decide (
      (∀ row ∈ i.1, row.length = d) ∧ i.2.length = i.1.length ∧
      ∃ x : List ℤ, x.length = d ∧
        ∀ r < i.1.length,
          (Finset.range d).sum (fun j =>
            decodeIntILP ((i.1.getD r []).getD j (0, true)) * x.getD j 0) ≤
              decodeIntILP (i.2.getD r (0, true)))
  | none => false

Uses 10 · 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 · Integer from magnitude and sign · Decision problems

Used byInteger linear programming in fixed dimension is in P (Lenstra)

TheoremInteger linear programming in fixed dimension is in P (Lenstra)#●ready to prove

For every natural number \(d\), integer linear-programming feasibility in dimension \(d\) is in the complexity class P.

public theorem_wanted ilp_fixed_dim_in_p :
    ∀ d : ℕ, ilpFixedDec d ∈ MetaMathlibExt.ComplexityTheory.P

Sources

• H. W. Lenstra Jr., "Integer programming with a fixed number of variables", Mathematics of Operations Research 8 (1983), 538-548.

Uses 4

Statement usesInteger linear-programming feasibility in fixed dimension · Complexity classes · Decision problems · The complexity class P

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.