Shortest common supersequence

AbbreviationShortest common supersequence instances#✓fully proved

An instance of SHORTEST COMMON SUPERSEQUENCE is a pair \((R, K)\) of a list \(R\) of binary strings (lists of booleans) and a natural number \(K\), the length bound.

abbrev ShortestCommonSupersequenceInstance := List (List Bool) × ℕ

Used by 2

Used byThe SHORTEST COMMON SUPERSEQUENCE decision problem · Feasible shortest common supersequence instances

DefinitionFeasible shortest common supersequence instances#✓fully proved

An instance \((R, K)\) of SHORTEST COMMON SUPERSEQUENCE, a list \(R\) of lists of booleans together with a natural number \(K\), is feasible when there is a list \(w\) of booleans of length at most \(K\) such that every list in \(R\) is a subsequence of \(w\) (its entries occur in \(w\) in the same order, not necessarily consecutively).

def ShortestCommonSupersequenceFeasible
    (i : ShortestCommonSupersequenceInstance) : Prop :=
  ∃ super : List Bool, super.length ≤ i.2 ∧ ∀ s ∈ i.1, s.Sublist super

Uses 1 · Used by 1

Statement usesShortest common supersequence instances

Used byThe SHORTEST COMMON SUPERSEQUENCE decision problem

DefinitionThe SHORTEST COMMON SUPERSEQUENCE decision problem#✓fully proved

SHORTEST COMMON SUPERSEQUENCE is the decision problem that accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to a pair \((R, K)\) of a list \(R\) of lists of booleans and a natural number \(K\) for which some list of booleans of length at most \(K\) has every list in \(R\) as a subsequence. Bitstrings that do not decode to such a pair are rejected.

noncomputable def shortestCommonSupersequenceDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := ShortestCommonSupersequenceInstance) x with
  | some i => decide (ShortestCommonSupersequenceFeasible 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 · Feasible shortest common supersequence instances · Shortest common supersequence instances · Decision problems

Used bySHORTEST COMMON SUPERSEQUENCE is NP-complete

TheoremSHORTEST COMMON SUPERSEQUENCE is NP-complete#●ready to prove

The SHORTEST COMMON SUPERSEQUENCE decision problem over binary strings belongs to NP, and every decision problem in NP reduces to it by a polynomial-time many-one reduction.

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

Sources

• K.-J. Räihä and E. Ukkonen, "The shortest common supersequence problem over binary alphabet is NP-complete", Theoretical Computer Science 16 (1981), 187-198. (D. Maier, "The complexity of some problems on subsequences and supersequences", JACM 25 (1978), 322-336, proves SCS only for a five- symbol alphabet; the binary case is Räihä-Ukkonen.)

Uses 5

Statement usesPolynomial-time many-one reduction · The SHORTEST COMMON SUPERSEQUENCE 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.