3-partition problem

Abbreviation3-partition instances#✓fully proved

An instance of 3-PARTITION is a pair \((a, B)\) of a finite list \(a\) of natural numbers and a natural number \(B\), the target sum.

abbrev ThreePartitionInstance := List ℕ × ℕ

Used by 3

Used by3-PARTITION as a decision problem · Feasible 3-partition instances · Well-formed 3-partition instances

DefinitionWell-formed 3-partition instances#✓fully proved

A 3-partition instance \((a, B)\) is well formed when the length of the list \(a\) is a multiple of \(3\).

def WellFormed (i : ThreePartitionInstance) : Prop :=
  i.1.length % 3 = 0

Uses 1 · Used by 1

Statement uses3-partition instances

Used by3-PARTITION as a decision problem

DefinitionFeasible 3-partition instances#✓fully proved

Let \((a, B)\) be a 3-partition instance with \(a = (a_0, \dots, a_{N-1})\), and let \(m = \lfloor N/3 \rfloor\). The instance is feasible when there is a map \(g : \{0, \dots, N-1\} \to \{0, \dots, m-1\}\) such that for every \(t < m\) exactly three indices \(j\) satisfy \(g(j) = t\), and the sum of \(a_j\) over these indices equals \(B\).

def ThreePartitionFeasible
    (i : ThreePartitionInstance) : Prop :=
  ∃ assign : List ℕ, assign.length = i.1.length ∧
    (∀ j < i.1.length, assign.getD j 0 < i.1.length / 3) ∧
    ∀ t < i.1.length / 3,
      ((List.range i.1.length).filter (fun j => assign.getD j 0 == t)).length = 3 ∧
      (Finset.range i.1.length).sum
        (fun j => if assign.getD j 0 = t then i.1.getD j 0 else 0) = i.2

Uses 1 · Used by 1

Statement uses3-partition instances

Used by3-PARTITION as a decision problem

Definition3-PARTITION as a decision problem#✓fully proved

The decision problem 3-PARTITION accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to a 3-partition instance \((a, B)\) that is well formed (the length of the list \(a\) is a multiple of \(3\)) and feasible (the entries of \(a\) can be split into triples each summing to \(B\)). Bitstrings that do not decode to an instance are rejected.

noncomputable def threePartitionDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := ThreePartitionInstance) x with
  | some i => decide (WellFormed i ∧ ThreePartitionFeasible i)
  | none => false

Uses 12 · 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 3-partition instances · 3-partition instances · Well-formed 3-partition instances · Decision problems

Used by3-PARTITION is NP-complete

Theorem3-PARTITION is NP-complete#●ready to prove

The decision problem 3-PARTITION on bitstrings is in NP, and every decision problem in NP reduces to it by a polynomial-time many-one reduction.

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), 3-PARTITION (strongly NP-complete).

Uses 5

Statement usesPolynomial-time many-one reduction · 3-PARTITION as a decision problem · Complexity classes · Decision problems · The complexity class NP

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.