Longest common subsequence of many strings

AbbreviationLongest-common-subsequence instances#✓fully proved

A longest-common-subsequence instance is a pair \((R, K)\) of a finite list \(R\) of binary strings (finite lists of booleans) and a natural number \(K\).

abbrev LongestCommonSubsequenceInstance := List (List Bool) × ℕ

Used by 2

Used byThe LONGEST COMMON SUBSEQUENCE decision problem · Feasible longest-common-subsequence instances

DefinitionFeasible longest-common-subsequence instances#✓fully proved

A longest-common-subsequence instance \((R, K)\) is feasible when there is a binary string \(w\) of length at least \(K\) that is a subsequence of every string in \(R\), that is, \(w\) is obtained from each string in \(R\) by deleting some of its entries.

def LongestCommonSubsequenceFeasible
    (i : LongestCommonSubsequenceInstance) : Prop :=
  ∃ common : List Bool, i.2 ≤ common.length ∧ ∀ s ∈ i.1, common.Sublist s

Uses 1 · Used by 1

Statement usesLongest-common-subsequence instances

Used byThe LONGEST COMMON SUBSEQUENCE decision problem

DefinitionThe LONGEST COMMON SUBSEQUENCE decision problem#✓fully proved

LONGEST COMMON SUBSEQUENCE is the decision problem that accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to a feasible longest-common-subsequence instance. Bitstrings that do not decode are rejected.

noncomputable def longestCommonSubsequenceDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := LongestCommonSubsequenceInstance) x with
  | some i => decide (LongestCommonSubsequenceFeasible 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 longest-common-subsequence instances · Longest-common-subsequence instances · Decision problems

Used byLONGEST COMMON SUBSEQUENCE is NP-complete

TheoremLONGEST COMMON SUBSEQUENCE is NP-complete#●ready to prove

The LONGEST COMMON SUBSEQUENCE 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 longestCommonSubsequence_npComplete :
    longestCommonSubsequenceDec ∈ MetaMathlibExt.ComplexityTheory.NP ∧
      ∀ L : MetaMathlibExt.ComplexityTheory.DecisionProblem,
        L ∈ MetaMathlibExt.ComplexityTheory.NP →
          Cslib.CookLevin.PolyManyOneRed L longestCommonSubsequenceDec

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), LONGEST COMMON SUBSEQUENCE; D. Maier, "The complexity of some problems on subsequences and supersequences" (1978).

Uses 5

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