Monadic Second Order Logic on Graphs with Local Cardinality Constraints

Stefan Szeider

ACM Transactions on Computational Logic, vol. 12, no. 2, article 12, 2011.

A a preliminary and shorter version of the paper appeard in the Proceedings of MFCS 2008, 33rd International Symposium on Mathematical Foundations of Computer Science, Lecture Notes in Computer Science, vol. 5162, pp. 601-612, Springer-Verlag, 2008.

Abstract:

We introduce the class of MSO-LCC problems which are problems of the following form:

INSTANCE: A graph G and for each vertex v of G a set α(v) of non-negative integers.
QUESTION: Is there a set S of vertices or edges of G such that S satisfies a fixed property expressible in monadic second order logic, and for each vertex v of G the number of vertices/edges in S adjacent/incident with v belongs to the set α(v)?

We demonstrate that several hard combinatorial problems such as Lovász's General Factor Problem can be naturally formulated as MSO-LCC problems. Our main result is the polynomial-time tractability of MSO-LCC problems for graph of bounded treewidth. We obtain this result by means of a tree-automata approach.

In way of contrast we show that a more general class of MSO-LCC problems where cardinality constraints are applied to second-order variables that are arbitrarily quantified does not admit polynomial-time tractability for graphs of bounded treewidth unless P=NP.

Download: [paper pdf]