Efficient counting with bounded treewidth using datalog

Abstract

Bounded treewidth has proven to be a key concept in identifying tractable fragments of inherently intractable problems. An important result in this context is Courcelle's Theorem, stating that any property of finite structures definable in monadic second-order logic (MSO), becomes tractable if the treewidth of the structure is bounded by a constant. An extension of this result to counting problems was done by Arnborg et al. But both proofs did not yield an implementable algorithm.<br />Recently Gottlob et al.\ presented a new approach using monadic datalog to close this gap for decision problems. The goal of this work is to extend this method in order to handle counting problems as well. We show that the monadic datalog approach indeed is applicable for all MSO definable counting problems. Furthermore we propose concrete algorithms with fixed-parameter linear running time for the problems #SAT, #CIRCUMSCRIPTION and #HORN-ABDUCTION.