Closest string

AbbreviationClosest-string instances#✓fully proved

A closest-string instance is a pair \((S, d)\) of a finite list \(S\) of bitstrings (finite lists of booleans) and a natural number \(d\), the distance bound.

The bitstrings are not required to have equal length; that is the well-formedness condition.

abbrev ClosestStringInstance := List (List Bool) × ℕ

Used by 3

Used byThe CLOSEST STRING decision problem · Feasible closest-string instances · Well-formed closest-string instances

DefinitionWell-formed closest-string instances#✓fully proved

A closest-string instance \((S, d)\) is well formed when all bitstrings in the list \(S\) have the same length.

def WellFormed (i : ClosestStringInstance) : Prop :=
  ∀ s ∈ i.1, ∀ t ∈ i.1, s.length = t.length

Uses 1 · Used by 1

Statement usesClosest-string instances

Used byThe CLOSEST STRING decision problem

DefinitionFeasible closest-string instances#✓fully proved

Write \(\ell(x)\) for the length of a bitstring \(x\). A closest-string instance \((S, d)\) is feasible when there is a bitstring \(c\) with \(\ell(c) = \ell(s_1)\), where \(s_1\) is the first bitstring of \(S\) (and \(\ell(c) = 0\) if \(S\) is empty), such that for every \(s\) in \(S\) the number of positions \(j < \min(\ell(c), \ell(s))\) at which \(c\) and \(s\) differ is at most \(d\).

If all bitstrings of \(S\) have length \(\ell(c)\), this number is the Hamming distance between \(c\) and \(s\).

def ClosestStringFeasible
    (i : ClosestStringInstance) : Prop :=
  ∃ center : List Bool, center.length = (i.1.getD 0 []).length ∧
    ∀ s ∈ i.1, ((List.zip center s).filter (fun p => !(p.1 == p.2))).length ≤ i.2

Uses 1 · Used by 1

Statement usesClosest-string instances

Used byThe CLOSEST STRING decision problem

DefinitionThe CLOSEST STRING decision problem#✓fully proved

The decision problem CLOSEST STRING accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding of closest-string instances, to an instance that is well formed and feasible. Bitstrings that do not decode to a closest-string instance are rejected.

noncomputable def closestStringDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := ClosestStringInstance) x with
  | some i => decide (WellFormed i ∧ ClosestStringFeasible 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 closest-string instances · Closest-string instances · Well-formed closest-string instances · Decision problems

Used byCLOSEST STRING is NP-complete

TheoremCLOSEST STRING is NP-complete#●ready to prove

The CLOSEST STRING decision problem belongs to NP, and every decision problem in NP has a polynomial-time many-one reduction to it.

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

Sources

• J. K. Lanctot et al., "Distinguishing string selection problems" (2003); M. Frances and A. Litman, "On covering problems of codes" (1997).

Uses 5

Statement usesPolynomial-time many-one reduction · The CLOSEST STRING 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.