Space and Circuit Complexity of Monadic Second-Order Definable Problems on Tree-Decomposable Structures

A famous theorem of Courcelle states that every problem that is definable in monadic second-order (MSO) logic can be solved in linear time on input structures of bounded tree width. While Courcelle’s result is optimal from the algorithmic point of view, this thesis shows how to solve monadic second- order definable decision, counting, and optimization problems on tree-width-bounded structures optimally from the complexity theoretic point of view. Beside bounded tree width, the related notion of bounded tree depth is considered. <br><br> A first set of results covers input structures of bounded tree width, which admit tree decompositions of bounded width. It is shown that all MSO-definable decision, counting, and optimization problems are solvable in deterministic logarithmic space (logspace) in this setting. Transferring the powerful framework of MSO-definability to logspace allows one to settle the complexity of problems related to finding paths and matchings in graphs: It is shown that answering reachability queries and counting the number of perfect matchings in graphs of bounded tree width can be done in logspace. Moreover, by solving problems on tree-width-bounded graphs as subroutines, problems on inputs of unbounded tree width are solvable in logspace; like deciding whether undirected loop-free graphs have cycles whose length is a multiple of any constant. These results rest on the new technique of constructing width-bounded tree decompositions in logspace. <br><br> Once tree decompositions are available, a task shown to be complete for logspace, actually solving MSO-definable decision and counting problems can be done by logarithmic-depth Boolean and arithmetic circuits, respectively. This finding itself unifies many automaton evaluation tasks studied in the area of logarithmic-depth circuits in an elegant manner using MSO-formulæ. To let logarithmic-depth circuits work on tree decompositions whose underlying trees have arbitrary depth, a preprocessing step is used that balances them using constant-depth threshold circuits. <br><br> The second set of results spans input structures of bounded tree depth, which admit tree decompositions of bounded width whose underlying trees have bounded depth. The logspace results are transferred to this setting to solve MSO-definable decision, counting, and optimization problems by constant-depth Boolean, arithmetic, and threshold circuits, respectively. These theorems apply to number problems like solving systems of any constant number of linear equations whose coefficients are given in unary. For their proofs input structures are turned into trees of bounded depth and unbounded degree. Translating MSO-formulæ to just the right automaton model for this situation and representing automata computations algebraically by arithmetic circuits lies at the heart of the proofs of these results. <br><br> In terms of computational power, constant-depth circuits are equivalent to first-order formulæ that have access to ordering and arithmetic predicates defined on the input’s universe. It is shown that these build-in predicates are not needed to evaluate MSO-formulæ once input structures are extracted from their string encodings: First-order formulæ and MSO-formulæ define the same problems on any class of structures of bounded tree depth. The main building block in the proof of this result is a new constructive Feferman–Vaught-type composition theorem for unbounded partitions.