Counting and Enumeration Problems with Bounded Treewidth

By Courcelle's Theorem we know that any property of finite structures definable in monadic second-order logic (MSO) becomes tractable over structures with bounded treewidth. This result was extended to counting problems by Arnborg et al. and to enumeration problems by Flum et al. Despite the undisputed importance of these results for proving fixed-parameter tractability, they do not directly yield implementable algorithms. Recently, Gottlob et al. presented a new approach using monadic datalog to close the gap between theoretical tractability and practical computability for MSO-definable decision problems. In the current work we show how counting and enumeration problems can be tackled by an appropriate extension of the datalog approach.

• Type: Journal
• Year: 2010
• Where: LPAR
• Authors: Reinhard Pichler, Stefan Rümmele, Stefan Woltran
• Keywords: Automated Reasoning, LPAR 2010, Monadic Second-order Logic, MSO-definable Decision Problems, Problems