∑math20

Theoretical computer science · Result 128

A factor-two approximation for shortest common superstring

1 paperLean

Gives a deterministic polynomial-time algorithm constructing a common superstring of length at most twice the optimum for every finite family of explicitly represented strings. The running time is polynomial in the full encoded input length, including symbol labels.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 1

First page of A Polynomial-Time 2-Approximation for Shortest Common Superstring

A Polynomial-Time 2-Approximation for Shortest Common Superstring

OpenAI · September 24, 2026

We give a deterministic algorithm that, for every finite family of explicitly represented ordinary strings, outputs a common superstring of length at most twice the optimum in time polynomial in the total encoded input size, including symbol labels. The guarantee applies to the algorithm constructed here, not the classical maximum-overlap Greedy procedure.

Read PDF Download Source

Cite
@misc{OAI:A-Polynomial-Time-2-Approximation-for-Shortest-Common-Superstring-September-24-2026,
  author = {{OpenAI}},
  title = {{A Polynomial-Time 2-Approximation for Shortest Common Superstring}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-Polynomial-Time-2-Approximation-for-Shortest-Common-Superstring-September-24-2026/paper.pdf}{OAI:A-Polynomial-Time-2-Approximation-for-Shortest-Common-Superstring-September-24-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The shortest common superstring problem asks for the shortest string containing each input string as a contiguous substring. The formalized result gives one deterministic polynomial-time algorithm whose output is a common superstring of length at most twice the unrestricted optimum. It applies to every finite list of explicitly encoded strings, with running time measured in input bits and the approximation ratio measured in symbol length.

Comparator links

ResultComparator statement
Polynomial-time 2-approximation for shortest common superstringSuperstring.lean

Scope note on GitHub →