Numerical 3-dimensional matching

AbbreviationNumerical 3-dimensional matching instances#✓fully proved

An instance of NUMERICAL 3-DIMENSIONAL MATCHING is a quadruple \((A, B, C, t)\) of three finite lists \(A\), \(B\), \(C\) of natural numbers and a natural number \(t\), the target.

abbrev Numerical3DMInstance := List ℕ × List ℕ × List ℕ × ℕ

Used by 3

Used byNUMERICAL 3-DIMENSIONAL MATCHING as a decision problem · Feasible numerical 3-dimensional matching instances · Well-formed numerical 3-dimensional matching instances

DefinitionWell-formed numerical 3-dimensional matching instances#✓fully proved

An instance \((A, B, C, t)\) of NUMERICAL 3-DIMENSIONAL MATCHING is well formed when the lists \(B\) and \(C\) have the same length as the list \(A\).

def WellFormed (i : Numerical3DMInstance) : Prop :=
  i.2.1.length = i.1.length ∧ i.2.2.1.length = i.1.length

Uses 1 · Used by 1

Statement usesNumerical 3-dimensional matching instances

Used byNUMERICAL 3-DIMENSIONAL MATCHING as a decision problem

DefinitionFeasible numerical 3-dimensional matching instances#✓fully proved

Let \((A, B, C, t)\) be an instance and let \(n\) be the length of \(A\), with lists indexed from \(0\). The instance is feasible when there are permutations \(p\) and \(q\) of the numbers \(0\) through \(n-1\) such that \(A_j + B_{p(j)} + C_{q(j)} = t\) for every \(j < n\), where an entry of \(B\) or \(C\) at an index past the end of its list counts as \(0\).

def Numerical3DMFeasible
    (i : Numerical3DMInstance) : Prop :=
  ∃ p : List ℕ, p.Perm (List.range i.1.length) ∧
    ∃ q : List ℕ, q.Perm (List.range i.1.length) ∧
    ∀ j < i.1.length, i.1.getD j 0 + i.2.1.getD (p.getD j 0) 0 +
      i.2.2.1.getD (q.getD j 0) 0 = i.2.2.2

Uses 1 · Used by 1

Statement usesNumerical 3-dimensional matching instances

Used byNUMERICAL 3-DIMENSIONAL MATCHING as a decision problem

DefinitionNUMERICAL 3-DIMENSIONAL MATCHING as a decision problem#✓fully proved

The decision problem NUMERICAL 3-DIMENSIONAL MATCHING accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding (natural numbers in binary), to an instance \((A, B, C, t)\) that is well formed and feasible: the lists \(B\) and \(C\) have the same length \(n\) as the list \(A\), and there are permutations \(p\) and \(q\) of the numbers \(0\) through \(n-1\) such that \(A_j + B_{p(j)} + C_{q(j)} = t\) for every \(j < n\), with lists indexed from \(0\). Every other bitstring is rejected.

noncomputable def numerical3DMDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := Numerical3DMInstance) x with
  | some i => decide (WellFormed i ∧ Numerical3DMFeasible 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 numerical 3-dimensional matching instances · Numerical 3-dimensional matching instances · Well-formed numerical 3-dimensional matching instances · Decision problems

Used byNUMERICAL 3-DIMENSIONAL MATCHING is NP-complete

TheoremNUMERICAL 3-DIMENSIONAL MATCHING is NP-complete#●ready to prove

The decision problem NUMERICAL 3-DIMENSIONAL MATCHING belongs to NP, and every decision problem in NP reduces to it by a polynomial-time many-one reduction.

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

Sources

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

Uses 5

Statement usesPolynomial-time many-one reduction · NUMERICAL 3-DIMENSIONAL MATCHING 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.