DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2026.13

Verification of the Garsia-Wachs Algorithm

Authors: Makoto Kanazawa

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

Abstract

The Garsia-Wachs algorithm is an algorithm for finding a leaf-labeled binary tree whose leaf sequence exactly matches the input weight sequence and whose cost is as small as possible, where the cost is the sum of the weights labeling the leaves multiplied by their levels. The algorithm, along with a proof of correctness due to Kingston, is presented in Knuth’s The Art of Computer Programming, Vol. 3. The algorithm comes in two versions, the naive and the optimized. Both versions have quadratic time complexity, but the optimized version can be fine-tuned with a suitable data structure to yield an O(n log n)-time algorithm. I implement and verify a variant of each version of the algorithm in the verification-aware programming language Dafny. Unlike all previous presentations of the algorithm, these variants construct the desired optimum tree directly, without detour through a "nonalphabetic" tree whose leaf sequence is a rearrangement of the input sequence.

Cite as

Makoto Kanazawa. Verification of the Garsia-Wachs Algorithm. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 13:1-13:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{kanazawa:LIPIcs.ITP.2026.13,
  author =	{Kanazawa, Makoto},
  title =	{{Verification of the Garsia-Wachs Algorithm}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{13:1--13:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.13},
  URN =		{urn:nbn:de:0030-drops-269877},
  doi =		{10.4230/LIPIcs.ITP.2026.13},
  annote =	{Keywords: Garsia-Wachs algorithm, Dafny}
}

Search Results

Documents authored by Kanazawa, Makoto

Verification of the Garsia-Wachs Algorithm

Abstract

Cite as

Thanks for your feedback!

Could not send message