Subset product

AbbreviationSUBSET PRODUCT instances#✓fully proved

An instance of SUBSET PRODUCT is a pair \((a, T)\) of a finite list \(a\) of natural numbers and a target natural number \(T\).

abbrev SubsetProductInstance := List ℕ × ℕ

Used by 3

Used bySUBSET PRODUCT as a decision problem · Feasible SUBSET PRODUCT instances · Well-formed SUBSET PRODUCT instances

DefinitionWell-formed SUBSET PRODUCT instances#✓fully proved

An instance \((a, T)\) of SUBSET PRODUCT, with \(a\) a finite list of natural numbers and \(T\) a natural number, is well formed when every entry of \(a\) is positive.

def WellFormed (i : SubsetProductInstance) : Prop :=
  ∀ a ∈ i.1, 0 < a

Uses 1 · Used by 1

Statement usesSUBSET PRODUCT instances

Used bySUBSET PRODUCT as a decision problem

DefinitionFeasible SUBSET PRODUCT instances#✓fully proved

An instance \((a, T)\) of SUBSET PRODUCT, with \(a\) a finite list of natural numbers and \(T\) a natural number, is feasible when some sublist of \(a\) (a list obtained from \(a\) by deleting entries and keeping the order of the rest) has product exactly \(T\).

def SubsetProductFeasible
    (i : SubsetProductInstance) : Prop :=
  ∃ s : List ℕ, s.Sublist i.1 ∧ s.prod = i.2

Uses 1 · Used by 1

Statement usesSUBSET PRODUCT instances

Used bySUBSET PRODUCT as a decision problem

DefinitionSUBSET PRODUCT as a decision problem#✓fully proved

The decision problem SUBSET PRODUCT accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding of pairs of a finite list of natural numbers and a natural number, to an instance \((a, T)\) that is well formed (every entry of \(a\) is positive) and feasible (some sublist of \(a\) has product exactly \(T\)). It rejects every bitstring that does not decode to an instance.

noncomputable def subsetProductDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := SubsetProductInstance) x with
  | some i => decide (WellFormed i ∧ SubsetProductFeasible 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 SUBSET PRODUCT instances · SUBSET PRODUCT instances · Well-formed SUBSET PRODUCT instances · Decision problems

Used bySUBSET PRODUCT is NP-complete

TheoremSUBSET PRODUCT is NP-complete#●ready to prove

The decision problem SUBSET PRODUCT lies in NP, and every decision problem in NP has a polynomial-time many-one reduction to SUBSET PRODUCT.

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), SUBSET PRODUCT.

Uses 5

Statement usesPolynomial-time many-one reduction · SUBSET PRODUCT 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.