0-1 integer programming is in NP

The certificate guesses the 0-1 vector and, for each row, a ripple-carry walk along the columns:

• x j, the columns set to 1;
• ps r j p, the bits of the running total of the row r over the chosen columns up to j;
• cy r j p, the carries of the step appending j to that total,

and the kernel asks that each row's walk be a ripple-carry addition ending on that row's right-hand side. It is Knapsack's certificate (DescriptiveComplexity.Problems.Knapsack.Membership) with a row argument threaded through the two arithmetic relations and a guard row r in front of every clause: the rows do not interact, so the walks are independent and the semantic work is DescriptiveComplexity.chain_sound and DescriptiveComplexity.exists_chain (DescriptiveComplexity.Problems.Knapsack.Chain) applied once per row – the reason those two are stated over an arbitrary walk order and item predicate rather than over one vocabulary.

Unlike Partition, the walks run on the instance's own positions: each row's total is its right-hand side, which is written there, so it fits.

@[reducible, inline]

abbrev DescriptiveComplexity.zoLeSym : zoSOLang.Relations 2

The le symbol over the sum.

Equations

• DescriptiveComplexity.zoLeSym = Sum.inl FirstOrder.Language.ipLe

def DescriptiveComplexity.zoPSRel : zeroOneIPGuessBlock.lang.Relations 3

The pS relation variable.

Equations

• DescriptiveComplexity.zoPSRel = ⟨DescriptiveComplexity.ZeroOneIPGuessBlockIx.pS, DescriptiveComplexity.zoPSRel._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.zoColSym : zoSOLang.Relations 1

The col symbol over the sum.

Equations

• DescriptiveComplexity.zoColSym = Sum.inl FirstOrder.Language.ipCol

def DescriptiveComplexity.zoXRel : zeroOneIPGuessBlock.lang.Relations 1

The x relation variable.

Equations

• DescriptiveComplexity.zoXRel = ⟨DescriptiveComplexity.ZeroOneIPGuessBlockIx.x, DescriptiveComplexity.zoXRel._proof_1⟩

def DescriptiveComplexity.zeroOneIPGuessBlock : SOBlock

The single existential block of the Σ₁ definition of 0-1 integer programming: the columns set to 1 (unary), and the running partial sums and the carries (ternary: a row, a column and a bit position).

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance DescriptiveComplexity.instFintypeZeroOneIPGuessBlockIx : Fintype ZeroOneIPGuessBlockIx

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqZeroOneIPGuessBlockIx : DecidableEq ZeroOneIPGuessBlockIx

Equations

• DescriptiveComplexity.instDecidableEqZeroOneIPGuessBlockIx x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[reducible, inline]

abbrev DescriptiveComplexity.zoPSSym : zoSOLang.Relations 3

The pS symbol over the sum.

Equations

• DescriptiveComplexity.zoPSSym = Sum.inr DescriptiveComplexity.zoPSRel

@[reducible, inline]

abbrev DescriptiveComplexity.zoRowSym : zoSOLang.Relations 1

The row symbol over the sum.

Equations

• DescriptiveComplexity.zoRowSym = Sum.inl FirstOrder.Language.ipRow

@[reducible, inline]

abbrev DescriptiveComplexity.zoSOLang : FirstOrder.Language

The vocabulary of the kernel: the instance expanded by the block.

Equations

• DescriptiveComplexity.zoSOLang = FirstOrder.Language.zeroOneIP.sum DescriptiveComplexity.zeroOneIPGuessBlock.lang

inductive DescriptiveComplexity.ZeroOneIPGuessBlockIx : Type

The relation variables of the block.

• x : ZeroOneIPGuessBlockIx

  The columns set to 1.

• pS : ZeroOneIPGuessBlockIx

  The running partial sums: pS r j p is the bit p of the total of the row r up to the column j.

• cy : ZeroOneIPGuessBlockIx

  The carries of the step appending a column to a row's total.

@[reducible, inline]

abbrev DescriptiveComplexity.zoCySym : zoSOLang.Relations 3

The cy symbol over the sum.

Equations

• DescriptiveComplexity.zoCySym = Sum.inr DescriptiveComplexity.zoCyRel

@[reducible, inline]

abbrev DescriptiveComplexity.zoCoefSym : zoSOLang.Relations 3

The coef symbol over the sum.

Equations

• DescriptiveComplexity.zoCoefSym = Sum.inl FirstOrder.Language.ipCoef

@[reducible, inline]

abbrev DescriptiveComplexity.zoRhsSym : zoSOLang.Relations 2

The rhs symbol over the sum.

Equations

• DescriptiveComplexity.zoRhsSym = Sum.inl FirstOrder.Language.ipRhs

@[reducible, inline]

abbrev DescriptiveComplexity.zoPosnSym : zoSOLang.Relations 1

The posn symbol over the sum.

Equations

• DescriptiveComplexity.zoPosnSym = Sum.inl FirstOrder.Language.ipPosn

def DescriptiveComplexity.zoCyRel : zeroOneIPGuessBlock.lang.Relations 3

The cy relation variable.

Equations

• DescriptiveComplexity.zoCyRel = ⟨DescriptiveComplexity.ZeroOneIPGuessBlockIx.cy, DescriptiveComplexity.zoCyRel._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.zoXSym : zoSOLang.Relations 1

The x symbol over the sum.

Equations

• DescriptiveComplexity.zoXSym = Sum.inr DescriptiveComplexity.zoXRel

Formula builders

def DescriptiveComplexity.zoColF {α : Type} (x : α) : zoSOLang.Formula α

x is a column, as a formula.

Equations

• DescriptiveComplexity.zoColF x = DescriptiveComplexity.zoColSym.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.zoRowF {α : Type} (x : α) : zoSOLang.Formula α

x is a row, as a formula.

Equations

• DescriptiveComplexity.zoRowF x = DescriptiveComplexity.zoRowSym.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.zoPosnF {α : Type} (x : α) : zoSOLang.Formula α

x is a bit position, as a formula.

Equations

• DescriptiveComplexity.zoPosnF x = DescriptiveComplexity.zoPosnSym.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.zoCoefF {α : Type} (r j p : α) : zoSOLang.Formula α

The entry of the row r in the column j has bit 1 at p, as a formula.

Equations

• DescriptiveComplexity.zoCoefF r j p = DescriptiveComplexity.zoCoefSym.formula ![FirstOrder.Language.var r, FirstOrder.Language.var j, FirstOrder.Language.var p]

def DescriptiveComplexity.zoRhsF {α : Type} (r p : α) : zoSOLang.Formula α

The right-hand side of the row r has bit 1 at p, as a formula.

Equations

• DescriptiveComplexity.zoRhsF r p = DescriptiveComplexity.zoRhsSym.formula₂ (FirstOrder.Language.var r) (FirstOrder.Language.var p)

def DescriptiveComplexity.zoLeF {α : Type} (x y : α) : zoSOLang.Formula α

x ≤ y, as a formula.

Equations

• DescriptiveComplexity.zoLeF x y = DescriptiveComplexity.zoLeSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

def DescriptiveComplexity.zoEqF {α : Type} (x y : α) : zoSOLang.Formula α

x = y, as a formula.

Equations

• DescriptiveComplexity.zoEqF x y = (FirstOrder.Language.var x).equal (FirstOrder.Language.var y)

def DescriptiveComplexity.zoXF {α : Type} (x : α) : zoSOLang.Formula α

The column x is set to 1, as a formula.

Equations

• DescriptiveComplexity.zoXF x = DescriptiveComplexity.zoXSym.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.zoPSF {α : Type} (r j p : α) : zoSOLang.Formula α

Bit p of the running total of the row r at the column j, as a formula.

Equations

• DescriptiveComplexity.zoPSF r j p = DescriptiveComplexity.zoPSSym.formula ![FirstOrder.Language.var r, FirstOrder.Language.var j, FirstOrder.Language.var p]

def DescriptiveComplexity.zoCyF {α : Type} (r j p : α) : zoSOLang.Formula α

The carry at p of the step appending the column j to the total of the row r, as a formula.

Equations

• DescriptiveComplexity.zoCyF r j p = DescriptiveComplexity.zoCySym.formula ![FirstOrder.Language.var r, FirstOrder.Language.var j, FirstOrder.Language.var p]

def DescriptiveComplexity.zoAddF {α : Type} (r j p : α) : zoSOLang.Formula α

The bit that the column j contributes to the row r at p: the entry's bit, if the column is set to 1.

Equations

• DescriptiveComplexity.zoAddF r j p = DescriptiveComplexity.zoXF j ⊓ DescriptiveComplexity.zoCoefF r j p

def DescriptiveComplexity.zoXor3F {α : Type} (x y z : zoSOLang.Formula α) : zoSOLang.Formula α

The exclusive or of three formulas, as x ↔ (y ↔ z).

Equations

• DescriptiveComplexity.zoXor3F x y z = x.iff (y.iff z)

def DescriptiveComplexity.zoMaj3F {α : Type} (x y z : zoSOLang.Formula α) : zoSOLang.Formula α

The majority of three formulas.

Equations

• DescriptiveComplexity.zoMaj3F x y z = x ⊓ y ⊔ (x ⊓ z ⊔ y ⊓ z)

noncomputable def DescriptiveComplexity.zoMinColF {α : Type} (j : α) : zoSOLang.Formula α

j is the first column, as a formula.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.zoMaxColF {α : Type} (j : α) : zoSOLang.Formula α

j is the last column, as a formula.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.zoSuccColF {α : Type} (i j : α) : zoSOLang.Formula α

j is the column right after i, as a formula.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.zoMinPosnF {α : Type} (p : α) : zoSOLang.Formula α

p is the lowest position, as a formula.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.zoMaxPosnF {α : Type} (p : α) : zoSOLang.Formula α

p is the highest position, as a formula.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.zoSuccPosnF {α : Type} (p q : α) : zoSOLang.Formula α

q is the position right above p, as a formula.

Equations

• One or more equations did not get rendered due to their size.

The clauses

Every clause of a walk is guarded by row r: the rows do not interact, so the kernel is Knapsack's read once per row.

noncomputable def DescriptiveComplexity.zeroOneIPKernel : zoSOLang.Sentence

The first-order kernel of the Σ₁ definition of 0-1 integer programming.

Equations

• One or more equations did not get rendered due to their size.

Realization

def DescriptiveComplexity.ZX {A : Type} (ρ : zeroOneIPGuessBlock.Assignment A) (j : A) : Prop

The columns set to 1, read off an assignment of the block.

Equations

• DescriptiveComplexity.ZX ρ j = ρ DescriptiveComplexity.ZeroOneIPGuessBlockIx.x ![j]

def DescriptiveComplexity.ZPS {A : Type} (ρ : zeroOneIPGuessBlock.Assignment A) (r j p : A) : Prop

The running total of a row, read off an assignment of the block.

Equations

• DescriptiveComplexity.ZPS ρ r j p = ρ DescriptiveComplexity.ZeroOneIPGuessBlockIx.pS ![r, j, p]

def DescriptiveComplexity.ZCy {A : Type} (ρ : zeroOneIPGuessBlock.Assignment A) (r j p : A) : Prop

The carries of a row, read off an assignment of the block.

Equations

• DescriptiveComplexity.ZCy ρ r j p = ρ DescriptiveComplexity.ZeroOneIPGuessBlockIx.cy ![r, j, p]

Membership

theorem DescriptiveComplexity.zeroOneIP_sigmaSODefinable : SigmaSODefinable 1 ZeroOneIP

0-1 integer programming is Σ₁-definable: guess the 0-1 vector and, for each row, the running totals and the carries of a ripple-carry addition, and check first-order that every row's walk ends on that row's right-hand side. Since NP is defined as Σ₁-definability, this is the membership half of the NP-completeness of 0-1 integer programming.