Exploiting bounded treewidth with datalog (a survey)

Abstract

Many intractable problems have been shown to become tractable if the treewidth of the underlying structure is bounded by a constant. An important tool for deriving such results is Courcelle's Theorem, which states that all properties definable by Monadic Second Order (MSO) sentences are fixed-parameter tractable with respect to the treewidth. In principle, algorithms can be generated automatically from the MSO definition of a problem by exploiting the correspondence between MSO and finite tree automata (FTA). However, this approach has turned out to be problematic, since even relatively simple MSO formulae may lead to a "state explosion" of the FTA. Recently, monadic datalog (i.e., datalog where all intensional predicate symbols are unary) has been proposed as an alternative method to tackle this class of fixed-parameter tractable problems. On the one hand, if some property of finite structures is expressible in MSO then this property can also be expressed by means of a monadic datalog program. Moreover, the resulting fragment of datalog can be evaluated in linear time (both with respect to the program size and with respect to the data size). In this survey, we present the main ideas of this approach and its extension to counting and enumeration problems. © 2011 Springer-Verlag.