Multiway number partitioning

AbbreviationMultiway number partition instances#✓fully proved

A multiway number partition instance is a pair \((a, K)\) consisting of a list \(a\) of natural numbers and a natural number \(K\) (the number of parts).

abbrev MultiwayPartitionInstance := List ℕ × ℕ

Used by 2

Used byThe MULTIWAY NUMBER PARTITION decision problem · Feasible multiway number partition instances

DefinitionFeasible multiway number partition instances#✓fully proved

Let \((a, K)\) be a multiway number partition instance with \(a = (a_0, \dots, a_{m-1})\). It is feasible when \(K \ge 1\) and there is a map \(f\) from \(\{0, \dots, m-1\}\) onto \(\{0, \dots, K-1\}\) such that the sums \(\sum_{j < m,\, f(j) = p} a_j\) for \(p = 0, \dots, K-1\) are all equal. In other words, the entries of \(a\), counted with repetition, can be split into \(K\) nonempty parts with equal sums.

def MultiwayPartitionFeasible
    (i : MultiwayPartitionInstance) : Prop :=
  ∃ assign : List ℕ, assign.length = i.1.length ∧ 0 < i.2 ∧
    (∀ j < i.1.length, assign.getD j 0 < i.2) ∧
    (∀ p < i.2, ∃ j < i.1.length, assign.getD j 0 = p) ∧
    ∃ T, ∀ p < i.2, (Finset.range i.1.length).sum
      (fun j => if assign.getD j 0 = p then i.1.getD j 0 else 0) = T

Uses 1 · Used by 1

Statement usesMultiway number partition instances

Used byThe MULTIWAY NUMBER PARTITION decision problem

DefinitionThe MULTIWAY NUMBER PARTITION decision problem#✓fully proved

MULTIWAY NUMBER PARTITION is the decision problem on bitstrings that accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to a multiway number partition instance \((a, K)\) that is feasible. Bitstrings that do not decode to a multiway number partition instance are rejected.

noncomputable def multiwayPartitionDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := MultiwayPartitionInstance) x with
  | some i => decide (MultiwayPartitionFeasible i)
  | none => false

Uses 11 · 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 · Feasible multiway number partition instances · Multiway number partition instances · Decision problems

Used byMULTIWAY NUMBER PARTITION is NP-complete

TheoremMULTIWAY NUMBER PARTITION is NP-complete#●ready to prove

Let MULTIWAY NUMBER PARTITION be the decision problem that accepts exactly the bitstrings decoding to a feasible multiway number partition instance: a list of natural numbers and a number \(K \ge 1\) such that the entries of the list, counted with repetition, can be split into \(K\) nonempty parts with equal sums. Then MULTIWAY NUMBER PARTITION is in NP, and every decision problem in NP reduces to it by a polynomial-time many-one reduction.

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), MULTIWAY NUMBER PARTITION (the K = 2 slice is PARTITION).

Uses 5

Statement usesPolynomial-time many-one reduction · The MULTIWAY NUMBER PARTITION decision problem · Complexity classes · Decision problems · The complexity class NP

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.