Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Low rank MSO

Mikołaj Bojańczyk, Michał Pilipczuk, Wojciech Przybyszewski, Marek Sokołowski, Giannos Stamoulis

TL;DR

This work defines low rank MSO, a dense-graph analogue of separator logic by restricting set quantification to vertex sets with bounded cutrank $ ext{rk}(X)\le r$. It develops a general definability framework and proves three central equivalences: LRMSO coincides with separator logic on weakly sparse classes, with flip-connectivity logic on classes of bounded VC-dimension, and with flip-reachability logic on all graphs, implying polynomial-time decidability for undirected graphs. The authors establish a Low Rank Definability Property and a Robust Low Rank Structure Theorem, using definable flips and seeds to translate rank-bounded quantifications into the target logics. These results unify dense and sparse graph logics through a common framework and suggest rich directions for extending tractability, including directed graphs and other combinatorial structures.

Abstract

We introduce a new logic for describing properties of graphs, which we call low rank MSO. This is the fragment of monadic second-order logic in which set quantification is restricted to vertex sets of bounded cutrank. We prove the following statements about the expressive power of low rank MSO. - Over any class of graphs that is weakly sparse, low rank MSO has the same expressive power as separator logic. This equivalence does not hold over all graphs. - Over any class of graphs that has bounded VC dimension, low rank MSO has the same expressive power as flip-connectivity logic. This equivalence does not hold over all graphs. - Over all graphs, low rank MSO has the same expressive power as flip-reachability logic. Here, separator logic is an extension of first-order logic by basic predicates for checking connectivity, which was proposed by Bojańczyk [ArXiv 2107.13953] and by Schirrmacher, Siebertz, and Vigny [ACM ToCL 2023]. Flip-connectivity logic and flip-reachability logic are analogues of separator logic suited for non-sparse graphs, which we propose in this work. In particular, the last statement above implies that every property of undirected graphs expressible in low rank MSO can be decided in polynomial time.

Low rank MSO

TL;DR

This work defines low rank MSO, a dense-graph analogue of separator logic by restricting set quantification to vertex sets with bounded cutrank . It develops a general definability framework and proves three central equivalences: LRMSO coincides with separator logic on weakly sparse classes, with flip-connectivity logic on classes of bounded VC-dimension, and with flip-reachability logic on all graphs, implying polynomial-time decidability for undirected graphs. The authors establish a Low Rank Definability Property and a Robust Low Rank Structure Theorem, using definable flips and seeds to translate rank-bounded quantifications into the target logics. These results unify dense and sparse graph logics through a common framework and suggest rich directions for extending tractability, including directed graphs and other combinatorial structures.

Abstract

We introduce a new logic for describing properties of graphs, which we call low rank MSO. This is the fragment of monadic second-order logic in which set quantification is restricted to vertex sets of bounded cutrank. We prove the following statements about the expressive power of low rank MSO. - Over any class of graphs that is weakly sparse, low rank MSO has the same expressive power as separator logic. This equivalence does not hold over all graphs. - Over any class of graphs that has bounded VC dimension, low rank MSO has the same expressive power as flip-connectivity logic. This equivalence does not hold over all graphs. - Over all graphs, low rank MSO has the same expressive power as flip-reachability logic. Here, separator logic is an extension of first-order logic by basic predicates for checking connectivity, which was proposed by Bojańczyk [ArXiv 2107.13953] and by Schirrmacher, Siebertz, and Vigny [ACM ToCL 2023]. Flip-connectivity logic and flip-reachability logic are analogues of separator logic suited for non-sparse graphs, which we propose in this work. In particular, the last statement above implies that every property of undirected graphs expressible in low rank MSO can be decided in polynomial time.

Paper Structure

This paper contains 14 sections, 34 theorems, 35 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Definitions and basic properties
  3. A general framework for proving equivalence with low rank mso
  4. Relation to separator logic
  5. Relation to flip-connectivity logic
  6. Negative result
  7. VC dimension and related notions
  8. Positive result
  9. Relation to flip-reachability logic
  10. Combinatorics of sets of low rank
  11. Sets of low rank described as suffixes of flips
  12. Parameterizing suffixes of flips
  13. Proof of the equivalence
  14. Conclusions

Key Result

Theorem 1.1

Let ${\mathscr C}$ be a weakly sparse class of graphs. Then for every formula of low rank mso there exists a formula of separator logic such that the two formulas are equivalent on all graphs from ${\mathscr C}$.

Figures (3)

  • Figure 1: A separation.
  • Figure 2: Example graph $G$ and construction of the digraph $H_{\bar{a}}$ from an admissible tuple $\bar{a}$.
  • Figure 3: Situation in the proof of \ref{['cl:small-upper-covering']}.

Theorems & Definitions (85)

  • Theorem 1.1
  • Theorem 1.2
  • Theorem 1.3
  • Theorem 1.4
  • Corollary 1.5
  • Lemma 2.1
  • proof
  • Lemma 2.2
  • proof
  • Definition 2.3: Flip-reachability logic
  • ...and 75 more