Zero-one integer programming

ZeroOneIP is the feasibility problem of zero-one integer programming in equality form: a system of linear equations ∑ j, a j * x j = t with natural coefficients and right-hand sides, encoded in binary, has a solution with every x j ∈ {0, 1}. Each equation c : ZeroOneIP.Equation stores the coefficients c.coeffs of the variables 0, 1, … (with missing coefficients zero) and the right-hand side c.rhs.

Karp states zero-one integer programming with integer coefficients and inequalities [Kar72]; the equality form with natural coefficients is the special case used here, and it is already NP-complete. A subset sum instance is a single equation, so SubsetSum reduces to ZeroOneIP, and composing with Sipser's digit construction reduces ThreeSAT to ZeroOneIP.

Main definitions

• Cslib.Complexity.ZeroOneIP.Equation, Cslib.Complexity.ZeroOneIP.encEquation: equality constraints and their binary encoding.
• Cslib.Complexity.ZeroOneIP, Cslib.Complexity.encZeroOneIP.
• Cslib.Complexity.ZeroOneIP.verifier.
• Cslib.Complexity.SubsetSum.toZeroOneIP.

Main results

• Cslib.Complexity.ZeroOneIP.mem_NP: ZeroOneIP ∈ NP encZeroOneIP.
• Cslib.Complexity.polyTimeReducible_SubsetSum_ZeroOneIP, Cslib.Complexity.polyTimeReducible_ThreeSAT_ZeroOneIP, Cslib.Complexity.ZeroOneIP_npHard, Cslib.Complexity.ZeroOneIP_npComplete: ZeroOneIP is NP-complete.

References

• R. M. Karp, Reducibility among combinatorial problems

structure Cslib.Complexity.ZeroOneIP.Equation : Type

A linear equality constraint ∑ j, coeffs[j] * x j = rhs in a zero-one integer program, with missing coefficients treated as zero.

• coeffs : List ℕ

  The coefficients of variables 0, 1, ….

• rhs : ℕ

  The right-hand side target.

def Cslib.Complexity.ZeroOneIP.instDecidableEqEquation.decEq (x✝ x✝¹ : Equation) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Complexity.ZeroOneIP.instDecidableEqEquation : DecidableEq Equation

@[instance_reducible]

instance Cslib.Complexity.ZeroOneIP.instReprEquation : Repr Equation

def Cslib.Complexity.ZeroOneIP.instReprEquation.repr : Equation → ℕ → Std.Format

@[simp]

theorem Cslib.Complexity.ZeroOneIP.encEquation_apply (a : Equation) : encEquation a = encEquationFields (a.coeffs, a.rhs)

def Cslib.Complexity.ZeroOneIP.encEquation : Equation ↪ List Bool

Binary encoding of a zero-one linear equation as (coeffs, rhs).

theorem Cslib.Complexity.ZeroOneIP.encEquation_coeffs_inO : Turing.MultiTapeTM.ComputableInO Equation.coeffs encEquation (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) (fun (a : Equation) => (encEquation a).length) fun (a : Equation) => (encEquation a).length

theorem Cslib.Complexity.ZeroOneIP.encEquation_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → List ℕ} {x1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInPolyTime x0 encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) (h1 : Turing.MultiTapeTM.ComputableInPolyTime x1 encIn Turing.MultiTapeTM.encNat) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => { coeffs := x0 x, rhs := x1 x }) encIn encEquation

@[reducible, inline]

abbrev Cslib.Complexity.ZeroOneIP.encEquationFields : List ℕ × ℕ ↪ List Bool

The tuple of the fields of encEquation.

theorem Cslib.Complexity.ZeroOneIP.encEquation_rhs_deg : Turing.MultiTapeTM.ComputableInDegree Equation.rhs encEquation Turing.MultiTapeTM.encNat 1 1

theorem Cslib.Complexity.ZeroOneIP.encEquation_mk_deg : Turing.MultiTapeTM.ComputableInDegree (fun (p : List ℕ × ℕ) => { coeffs := p.1, rhs := p.2 }) encEquationFields encEquation 1 1

theorem Cslib.Complexity.ZeroOneIP.encEquation_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget : γ → ℕ} {x0 : γ → List ℕ} {x1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInSpace x0 encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) budget) (h1 : Turing.MultiTapeTM.ComputableInSpace x1 encIn Turing.MultiTapeTM.encNat budget) : Turing.MultiTapeTM.ComputableInSpace (fun (x : γ) => { coeffs := x0 x, rhs := x1 x }) encIn encEquation budget

theorem Cslib.Complexity.ZeroOneIP.encEquation_rhs_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Equation} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encEquation S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).rhs) encIn✝ Turing.MultiTapeTM.encNat S✝

theorem Cslib.Complexity.ZeroOneIP.encEquation_rhs_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Equation} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encEquation → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).rhs) encIn✝ Turing.MultiTapeTM.encNat

theorem Cslib.Complexity.ZeroOneIP.encEquation_coeffs_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Equation} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encEquation → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).coeffs) encIn✝ (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

theorem Cslib.Complexity.ZeroOneIP.encEquation_rhs_inO : Turing.MultiTapeTM.ComputableInO Equation.rhs encEquation Turing.MultiTapeTM.encNat (fun (a : Equation) => (encEquation a).length) fun (a : Equation) => (encEquation a).length

theorem Cslib.Complexity.ZeroOneIP.encEquation_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → List ℕ} {T0 S0 x1 T1 S1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInO x0 encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) T0 S0) (h1 : Turing.MultiTapeTM.ComputableInO x1 encIn Turing.MultiTapeTM.encNat T1 S1) : Turing.MultiTapeTM.ComputableInO (fun (x : γ) => { coeffs := x0 x, rhs := x1 x }) encIn encEquation (fun (x : γ) => T0 x + T1 x) fun (x : γ) => S0 x + S1 x

theorem Cslib.Complexity.ZeroOneIP.encEquation_coeffs_deg : Turing.MultiTapeTM.ComputableInDegree Equation.coeffs encEquation (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) 1 1

theorem Cslib.Complexity.ZeroOneIP.encEquation_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : Equation) => (a.coeffs, a.rhs)) encEquation encEquationFields 1 1

theorem Cslib.Complexity.ZeroOneIP.encEquation_coeffs_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Equation} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encEquation S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).coeffs) encIn✝ (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) S✝

def Cslib.Complexity.ZeroOneIP : Set (List ZeroOneIP.Equation)

The systems of linear equations with natural coefficients that have a zero-one solution, the equality form of Karp's zero-one integer programming [Kar72]. An equation c asks for ∑ j < c.coeffs.length, c.coeffs[j] * x j = c.rhs.

@[reducible, inline]

abbrev Cslib.Complexity.encZeroOneIP : List ZeroOneIP.Equation ↪ List Bool

Instances of ZeroOneIP: the equations (coeffs, rhs), each framed, an equation being its list coeffs of coefficients, framed, each coefficient framed, then its right-hand side rhs; all numbers in binary.

def Cslib.Complexity.ZeroOneIP.verifier (x : List Equation × List Bool) : Bool

The verifier for ZeroOneIP: the certificate, read as the values of the variables, satisfies every equation.

theorem Cslib.Complexity.ZeroOneIP.isVerifier : IsVerifier encZeroOneIP Polynomial.X verifier ZeroOneIP

ZeroOneIP.verifier verifies ZeroOneIP with certificates as long as the encoded system.

theorem Cslib.Complexity.ZeroOneIP.computableInPolyTime_verifier : Turing.MultiTapeTM.ComputableInPolyTime verifier (Turing.MultiTapeTM.encPair encZeroOneIP Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

The ZeroOneIP verifier is polynomial-time.

theorem Cslib.Complexity.ZeroOneIP.mem_NP : ZeroOneIP ∈ NP encZeroOneIP

ZeroOneIP belongs to NP.

def Cslib.Complexity.SubsetSum.toZeroOneIP (x : SubsetSumInstance) : List ZeroOneIP.Equation

A subset sum instance as a single equation.

theorem Cslib.Complexity.SubsetSum.toZeroOneIP_mem_iff (x : SubsetSumInstance) : toZeroOneIP x ∈ ZeroOneIP ↔ x ∈ SubsetSum

Correctness of the reduction to ZeroOneIP.

theorem Cslib.Complexity.SubsetSum.computableInPolyTime_toZeroOneIP : Turing.MultiTapeTM.ComputableInPolyTime toZeroOneIP encSubsetSum encZeroOneIP

The reduction to ZeroOneIP is polynomial-time.

theorem Cslib.Complexity.polyTimeReducible_SubsetSum_ZeroOneIP : PolyTimeReducible encSubsetSum encZeroOneIP SubsetSum ZeroOneIP

SubsetSum reduces to ZeroOneIP in polynomial time.

theorem Cslib.Complexity.polyTimeReducible_ThreeSAT_ZeroOneIP : PolyTimeReducible encCNF encZeroOneIP ThreeSAT ZeroOneIP

ThreeSAT reduces to ZeroOneIP in polynomial time, through Sipser's digit construction.

theorem Cslib.Complexity.ZeroOneIP_npHard : NPHard encZeroOneIP ZeroOneIP

ZeroOneIP is NP-hard.

theorem Cslib.Complexity.ZeroOneIP_npComplete : NPComplete encZeroOneIP ZeroOneIP

Zero-one integer programming is NP-complete, in equality form with natural coefficients in binary [Kar72].