Exact-cardinality subset sum

AbbreviationExact-cardinality subset-sum instances#✓fully proved

An exact-cardinality subset-sum instance is a triple \((a, K, T)\) consisting of a list \(a\) of natural numbers, a natural number \(K\) (the cardinality) and a natural number \(T\) (the target).

abbrev CardinalitySubsetSumInstance := List ℕ × ℕ × ℕ

Used by 2

Used byExact-cardinality subset sum as a decision problem · Feasibility of an exact-cardinality subset-sum instance

DefinitionFeasibility of an exact-cardinality subset-sum instance#✓fully proved

An exact-cardinality subset-sum instance \((a, K, T)\) is feasible when some subsequence of the list \(a\) (entries kept in order, not necessarily contiguous) has exactly \(K\) entries and sum \(T\).

def CardinalitySubsetSumFeasible
    (i : CardinalitySubsetSumInstance) : Prop :=
  ∃ s : List ℕ, s.Sublist i.1 ∧ s.length = i.2.1 ∧ s.sum = i.2.2

Uses 1 · Used by 1

Statement usesExact-cardinality subset-sum instances

Used byExact-cardinality subset sum as a decision problem

DefinitionExact-cardinality subset sum as a decision problem#✓fully proved

The decision problem EXACT-CARDINALITY SUBSET SUM accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to an exact-cardinality subset-sum instance that is feasible; it rejects every bitstring that does not decode.

noncomputable def cardinalitySubsetSumDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := CardinalitySubsetSumInstance) x with
  | some i => decide (CardinalitySubsetSumFeasible 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 · Feasibility of an exact-cardinality subset-sum instance · Exact-cardinality subset-sum instances · Decision problems

Used byEXACT-CARDINALITY SUBSET SUM is NP-complete

TheoremEXACT-CARDINALITY SUBSET SUM is NP-complete#●ready to prove

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

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), SUBSET SUM; NP-completeness via the zero-padding reduction from ordinary subset sum.

Uses 5

Statement usesPolynomial-time many-one reduction · Exact-cardinality subset sum as a 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.