Algorithmic Meta Theorems for Circuit Classes of Constant and Logarithmic Depth

摘要

An algorithmic meta theorem for a logic and a class C of structuresstates that all problems expressible in this logic can be solvedefficiently for inputs from $C$. The prime example is Courcelleu27sTheorem, which states that monadic second-order (MSO) definableproblems are linear-time solvable on graphs of bounded tree width. Wecontribute new algorithmic meta theorems, which state thatMSO-definable problems are (a) solvable by uniform constant-depthcircuit families (AC0 for decision problems and TC0 for countingproblems) when restricted to input structures of bounded tree depthand (b) solvable by uniform logarithmic-depth circuit families (NC1for decision problems and #NC1 for counting problems) when a treedecomposition of bounded width in term representation is part of theinput. Applications of our theorems include a TC0-completeness prooffor the unary version of integer linear programming with a fixednumber of equations and extensions of a recent result that countingthe number of accepting paths of a visible pushdown automaton lies in#NC1. Our main technical contributions are a new tree automata modelfor unordered, unranked, labeled trees; a method for representing thetree automatau27s computations algebraically using convolution circuits;and a lemma on computing balanced width-3 tree decompositions of treesin TC0, which encapsulates most of the technical difficultiessurrounding earlier results connecting tree automata and NC1.