Algorithmic compression of finite tree languages by rigid acyclic grammars

Sebastian Eberhard, Gabriel Ebner, Stefan Hetzl

Research output: Contribution to JournalArticleAcademicpeer-review


We present an algorithm to optimally compress a finite set of terms using a vectorial totally rigid acyclic tree grammar. This class of grammars has a tight connection to proof theory, and the grammar compression problem considered in this article has applications in automated deduction. The algorithm is based on a polynomial-time reduction to the MaxSAT optimization problem. The crucial step necessary to justify this reduction consists of applying a term rewriting relation to vectorial totally rigid acyclic tree grammars. Our implementation of this algorithm performs well on a large real-world dataset.

Original languageEnglish
Article number26
JournalACM Transactions on Computational Logic
Issue number4
Publication statusPublished - 1 Sep 2017
Externally publishedYes


  • Finite tree languages
  • Grammar-based compression
  • MaxSAT

Cite this