Linear programming feasibility

DefinitionSigned integer from a magnitude–sign pair#✓fully proved

The integer decoded from a pair \((k, s)\) of a natural number \(k\) and a boolean \(s\) is \(k\) if \(s\) is true and \(-k\) if \(s\) is false.

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

Used by 1

Used byRational linear-program feasibility

DefinitionRational linear-program feasibility#✓fully proved

The decision problem of rational linear-program feasibility accepts a bitstring \(w\) exactly when \(w\) decodes, under the canonical bitstring encoding, to a pair \((A, b)\) of a list \(A\) of \(m\) rows, each a list of magnitude–sign pairs, and a list \(b\) of \(m'\) magnitude–sign pairs, such that every row of \(A\) has the length \(n\) of the first row (\(n = 0\) when \(m = 0\)), \(m' = m\), and some \(x \in \mathbb{Q}^n\) satisfies \(\sum_{j\lt n} A_{rj} x_j \le b_r\) for every \(r < m\). Here a magnitude–sign pair \((k, s)\) of a natural number \(k\) and a boolean \(s\) stands for the integer \(k\) if \(s\) is true and \(-k\) if \(s\) is false, \(A_{rj}\) is the integer given by the \(j\)-th entry of the \(r\)-th row and \(b_r\) is the integer given by the \(r\)-th entry of \(b\). Bitstrings that do not decode are rejected.

noncomputable def lpDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := List (List (ℕ × Bool)) × List (ℕ × Bool)) x with
  | some i => decide (
      (∀ row ∈ i.1, row.length = (i.1.getD 0 []).length) ∧
      i.2.length = i.1.length ∧
      ∃ x : List ℚ, x.length = (i.1.getD 0 []).length ∧
        ∀ r < i.1.length,
          (Finset.range (i.1.getD 0 []).length).sum (fun j =>
            (decodeInt ((i.1.getD r []).getD j (0, true)) : ℚ) * x.getD j 0) ≤
              (decodeInt (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 · Signed integer from a magnitude–sign pair · Decision problems

Used byLinear programming is in P (Khachiyan)

TheoremLinear programming is in P (Khachiyan)#●ready to prove

The decision problem of rational linear-program feasibility is in the complexity class P. This problem accepts exactly the bitstrings that decode, under the canonical bitstring encoding, to a list \(A\) of \(m\) rows of integers, all of the same length \(n\), and a list \(b\) of \(m\) integers, for which some \(x \in \mathbb{Q}^n\) satisfies \(\sum_{j\lt n} A_{rj} x_j \le b_r\) for every \(r < m\), where \(A_{rj}\) is the \(j\)-th entry of the \(r\)-th row of \(A\) and \(b_r\) is the \(r\)-th entry of \(b\). Each integer is given as a magnitude–sign pair \((k, s)\) of a natural number \(k\) and a boolean \(s\), standing for \(k\) if \(s\) is true and \(-k\) if \(s\) is false.

public theorem_wanted lp_in_p :
    lpDec ∈ MetaMathlibExt.ComplexityTheory.P

Sources

• L. G. Khachiyan, "A polynomial algorithm in linear programming", Soviet Mathematics Doklady 20 (1979), 191-194.

Uses 4

Statement usesRational linear-program feasibility · 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.