Hardness of monadic second-order formulae over succinct graphs

TL;DR

This paper demonstrates that most nontrivial monadic second-order properties over succinctly represented graphs are computationally hard, contrasting with Courcelle's theorem, and explores the complexity when certain conditions are relaxed.

Contribution

It establishes a complexity dichotomy for MSO properties over succinct graphs and analyzes the impact of dropping cw-nontriviality on logical decision problems.

Findings

Every cw-nontrivial MSO property is NP-hard or coNP-hard over succinct graphs.

The complexity dichotomy fails when cw-nontriviality is dropped, assuming a reasonable complexity hypothesis.

The results contrast with Courcelle's meta-theorem by considering succinct graph representations.

Abstract

Our main result is a succinct counterpoint to Courcelle's meta-theorem as follows: every cw-nontrivial monadic second-order (MSO) property is either NP-hard or coNP-hard over graphs given by succinct representations. Succint representations are Boolean circuits computing the adjacency relation. Cw-nontrivial properties are those which have infinitely many models and infinitely many countermodels with bounded cliquewidth. Moreover, we explore what happens when the cw-nontriviality condition is dropped and show that, under a reasonable complexity assumption, the previous dichotomy fails, even for questions expressible in first-order logic.