TR11-128 Authors: Michael Elberfeld, Andreas Jakoby, Till Tantau

Publication: 21st September 2011 21:28

Downloads: 1516

Keywords:

An algorithmic meta theorem for a logic and a class $C$ of structures states that all problems expressible in this logic can be solved efficiently for inputs from $C$. The prime example is Courcelle's Theorem, which states that monadic second-order (MSO) definable problems are linear-time solvable on graphs of bounded tree width. We contribute new algorithmic meta theorems, which state that MSO-definable problems are (a) solvable by uniform constant-depth circuit families (AC$^0$ for decision problems and TC$^0$ for counting problems) when restricted to input structures of bounded tree depth and (b) solvable by uniform logarithmic-depth circuit families (NC$^1$ for decision problems and #NC$^1$ for counting problems) when a tree decomposition of bounded width in term representation is part of the input. Applications of our theorems include a TC$^0$-completeness proof for the unary version of integer linear programming with a fixed number of equations and extensions of a recent result that counting the number of accepting paths of a visible pushdown automaton lies in #NC$^1$. Our main technical contributions are a new tree automata model for unordered, unranked, labeled trees; a method for representing the tree automata's computations algebraically using convolution circuits; and a lemma on computing balanced width-3 tree decompositions of trees in TC$^0$, which encapsulates most of the technical difficulties surrounding earlier results connecting tree automata and NC$^1$.