Minimum test set

AbbreviationMinimum test set instance#✓fully proved

An instance of MINIMUM TEST SET is a triple \((n, C, K)\) of a natural number \(n\) (the number of elements), a finite list \(C\) of finite lists of natural numbers (the tests) and a natural number \(K\) (the bound).

abbrev MinimumTestSetInstance := ℕ × List (List ℕ) × ℕ

Used by 3

Used byThe MINIMUM TEST SET decision problem · Feasible minimum test set instance · Well-formed minimum test set instance

DefinitionWell-formed minimum test set instance#✓fully proved

An instance \((n, C, K)\) of MINIMUM TEST SET is well formed when every test in the list \(C\) is a list of numbers below \(n\) without repeated entries, so that each test lists a subset of \(\{0, \dots, n-1\}\), each element once.

def WellFormed (i : MinimumTestSetInstance) : Prop :=
  ∀ s ∈ i.2.1, s.Nodup ∧ ∀ x ∈ s, x < i.1

Uses 1 · Used by 1

Statement usesMinimum test set instance

Used byThe MINIMUM TEST SET decision problem

DefinitionFeasible minimum test set instance#✓fully proved

An instance \((n, C, K)\) of MINIMUM TEST SET is feasible when some sublist \(T\) of \(C\) (obtained by deleting entries of \(C\)) has length at most \(K\) and distinguishes every pair: for all distinct \(a, b < n\) some test in \(T\) contains exactly one of \(a\) and \(b\).

def MinimumTestSetFeasible
    (i : MinimumTestSetInstance) : Prop :=
  ∃ T : List (List ℕ), T.Sublist i.2.1 ∧ T.length ≤ i.2.2 ∧
    ∀ a < i.1, ∀ b < i.1, a ≠ b →
      ∃ s ∈ T, (a ∈ s ∧ b ∉ s) ∨ (a ∉ s ∧ b ∈ s)

Uses 1 · Used by 1

Statement usesMinimum test set instance

Used byThe MINIMUM TEST SET decision problem

DefinitionThe MINIMUM TEST SET decision problem#✓fully proved

It accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to a triple \((n, C, K)\) of a natural number \(n\), a list \(C\) of lists of natural numbers (the tests) and a natural number \(K\) with the following properties: every test is a list of numbers below \(n\) without repeated entries, and some sublist \(T\) of \(C\), obtained by deleting entries of \(C\), has length at most \(K\) and distinguishes every pair, that is, for all distinct \(a, b < n\) some test in \(T\) contains exactly one of \(a\) and \(b\). Bitstrings that do not decode are rejected.

noncomputable def minimumTestSetDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := MinimumTestSetInstance) x with
  | some i => decide (WellFormed i ∧ MinimumTestSetFeasible 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 minimum test set instance · Minimum test set instance · Well-formed minimum test set instance · Decision problems

Used byMINIMUM TEST SET is NP-complete

TheoremMINIMUM TEST SET is NP-complete#●ready to prove

The MINIMUM TEST SET decision problem lies in NP, and every decision problem in NP has a polynomial-time many-one reduction to it.

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), MINIMUM TEST COLLECTION; A. De Bonis, L. Gargano, and U. Vaccaro, "Generalized framework for test set problems" (1997).

Uses 5

Statement usesPolynomial-time many-one reduction · The MINIMUM TEST SET 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.