Algorithmic Meta Theorems for Circuit Classes of Constant and Logarithmic Depth

Abstract

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 (AC0 for decision problems and TC0 for counting
problems) when restricted to input structures of bounded tree depth
and (b) solvable by uniform logarithmic-depth circuit families (NC1
for decision problems and #NC1 for counting problems) when a tree
decomposition of bounded width in term representation is part of the
input. Applications of our theorems include a TC0-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
#NC1. 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 TC0, which encapsulates most of the technical difficulties
surrounding earlier results connecting tree automata and NC1.