Monadic datalog over finite structures with bounded treewidth

ABSTRACT

Bounded treewidth and Monadic Second Order (MSO) logic have proved to be key concepts in establishing fixed-para-meter tractability results. Indeed, by Courcelle's Theorem we know: Any property of finite structures, which is expressible by an MSO sentence, can be decided in linear time (data complexity) if the structures have bounded treewidth.

In principle, Courcelle's Theorem can be applied directly to construct concrete algorithms by transforming the MSO evaluation problem into a tree language recognition problem. The latter can then be solved via a finite tree automaton (FTA). However, this approach has turned out to be problematical, since even relatively simple MSO formulae may lead to a "state explosion" of the FTA.

In this work we propose monadic datalog (i.e., data log where all intentional predicate symbols are unary) as an alternative method to tackle this class of fixed-parameter tractable problems. We show that if some property of finite structures is expressible in MSO then this property can also be expressed by means of a monadic datalog program over the structure plus the treedecomposition. Moreover, we show that the resulting fragment of datalogcan be evaluated in linear time (both w.r.t. the program size and w.r.t. the data size). This new approach is put to work by devising a new algorithm for the PRIMALITY problem (i.e., testing if some attribute in a relational schema is part of a key). We also report on experimental results with a prototype implementation.

REFERENCES

• 1: Serge Abiteboul , Richard Hull , Victor Vianu, Foundations of Databases: The Logical Level, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1995
• 2: Stefan Arnborg , Jens Lagergren , Detlef Seese, Easy problems for tree-decomposable graphs, Journal of Algorithms, v.12 n.2, p.308-340, June 1991 [doi>10.1016/0196-6774(91)90006-K]
• 3: Hans L. Bodlaender, A Linear-Time Algorithm for Finding Tree-Decompositions of Small Treewidth, SIAM Journal on Computing, v.25 n.6, p.1305-1317, Dec. 1996 [doi>10.1137/S0097539793251219]
• 4: Stefano Ceri , Georg Gottlob , Letizia Tanca, Logic programming and databases, Springer-Verlag New York, Inc., New York, NY, 1990
• 5: Brouno Courcelle, Graph rewriting: an algebraic and logic approach, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 6: J. Doner. Tree acceptors and some of their applications. J. Comput. Syst. Sci., 4(5):406--451, 1970.
• 7: W. F. Dowling and J. H. Gallier. Linear-Time Algorithms for Testing the Satisfiability of Propositional Horn Formulae. J. Log. Program., 1(3):267--284, 1984.
• 8: R. G. Downey and M. R. Fellows. Parameterized Complexity. Springer, New York, 1999.
• 9: H. -D. Ebbinghaus and J. Flum. Finite Model Theory, 2nd edition. Springer Monographs in Mathematics. Springer, 1999.
• 10: Thomas Eiter , Georg Gottlob, The complexity of logic-based abduction, Journal of the ACM (JACM), v.42 n.1, p.3-42, Jan. 1995 [doi>10.1145/200836.200838]
• 11: Thomas Eiter , Georg Gottlob , Helmut Veith, Generalized Quantifiers in Logic Programs, Revised Lectures from the 9th European Summer School on Logic, Language, and Information: Generalized Quantifiers and Computation, p.72-98, August 11-22, 1997
• 12: Thomas Eiter , Georg Gottlob , Helmut Veith, Modular Logic Programming and Generalized Quantifiers, Proceedings of the 4th International Conference on Logic Programming and Nonmonotonic Reasoning, p.290-309, July 28-31, 1997
• 13: Jörg Flum , Markus Frick , Martin Grohe, Query evaluation via tree-decompositions, Journal of the ACM (JACM), v.49 n.6, p.716-752, November 2002 [doi>10.1145/602220.602222]
• 14: J. Flum , M. Grohe, Parameterized Complexity Theory (Texts in Theoretical Computer Science. An EATCS Series), Springer-Verlag New York, Inc., Secaucus, NJ, 2006
• 15: Georg Gottlob , Christoph Koch, Monadic datalog and the expressive power of languages for Web information extraction, Journal of the ACM (JACM), v.51 n.1, p.74-113, January 2004 [doi>10.1145/962446.962450]
• 16: G. Gottlob, R. Pichler, and F. Wei. Bounded Treewidth as a Key to Tractability of Knowledge Representation and Reasoning. In Proc. AAAI 2006, pages 250--256. AAAI Press, 2006.
• 17: Georg Gottlob , Reinhard Pichler , Fang Wei, Tractable database design through bounded treewidth, Proceedings of the twenty-fifth ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, June 26-28, 2006, Chicago, IL, USA [doi>10.1145/1142351.1142370]
• 18: Martin Grohe, Descriptive and Parameterized Complexity, Proceedings of the 13th International Workshop and 8th Annual Conference of the EACSL on Computer Science Logic, p.14-31, September 20-25, 1999
• 19: Nils Klarlund , Anders Møller , Michael I. Schwartzbach, MONA Implementation Secrets, Revised Papers from the 5th International Conference on Implementation and Application of Automata, p.182-194, July 24-25, 2000
• 20: Leonid Libkin, Elements Of Finite Model Theory (Texts in Theoretical Computer Science. An Eatcs Series), SpringerVerlag, 2004
• 21: Heikki Mannila , Kari-Jouko Räihä, The design of relational databases, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1992
• 22: H. Maryns. On the Implementation of Tree Automata: Limitations of the Naive Approach. In Proc. 5th Int. Treebanks and Linguistic Theories Conference (TLT 2006), pages 235--246, 2006.
• 23: M. Minoux, LTUR: a simplified linear-time unit resolution algorithm for Horn formulae and computer implementation, Information Processing Letters, v.29 n.1, p.1-12, Sept. 15, 1988 [doi>10.1016/0020-0190(88)90124-X]
• 24: Frank Neven , Thomas Schwentick, Query automata over finite trees, Theoretical Computer Science, v.275 n.1-2, p.633-674, March 28 2002 [doi>10.1016/S0304-3975(01)00301-2]
• 25: J. W. Thatcher and J. B. Wright. Generalized Finite Automata Theory with an Application to a Decision Problem of Second-Order Logic. Mathematical Systems Theory, 2(1):57--81, 1968.
• 26: Jeffrey D. Ullman, Principles of database and knowledge-base systems, Vol. I, Computer Science Press, Inc., New York, NY, 1988
• 27: Moshe Y. Vardi, The complexity of relational query languages (Extended Abstract), Proceedings of the fourteenth annual ACM symposium on Theory of computing, p.137-146, May 05-07, 1982, San Francisco, California, United States [doi>10.1145/800070.802186]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Complexity of proof procedures

Additional Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Computations on discrete structures
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Computational logic

General Terms:
Algorithms, Performance, Theory

Keywords:
datalog, fixed-parameter tractability, monadic second order logic, tree decomposition, treewidth