cs.AIApr 9, 2026

Parameterized Complexity Of Representing Models Of MSO Formulas

Authors: Petr Kučera, Petr Martinek

Organizations: Department of Theoretical Computer Science and Mathematical Logic, Faculty of Mathematics and Physics, Charles University, Prague, Czech Republic

Read PDF
Ask AI
Cite

Copy citation

DOINot available for this paper

Abstract

Monadic second order logic (MSO2) plays an important role in parameterized complexity due to the Courcelle's theorem. This theorem states that the problem of checking if a given graph has a property specified by a given MSO2 formula can be solved by a parameterized linear time algorithm with respect to the treewidth of the graph and the size of the formula. We extend this result by showing that models of MSO2 formula with free variables can be represented with a decision diagram whose size is parameterized linear in the above mentioned parameter. In particular, we show a parameterized linear upper bound on the size of a sentential decision diagram (SDD) when treewidth is considered and a parameterized linear upper bound on the size of an ordered binary decision diagram (OBDD) when considering the pathwidth in the parameter. In addition, building on a lower bound on the size of OBDD by Razgon (2014), we show that there is an MSO2 formula and a class of graphs with bounded treewidth which do not admit an OBDD with the size parameterized by the treewidth. Our result offers a new perspective on the Courcelle's theorem and connects it to the area of knowledge representation.

Figures & tables

Figure 1: An example of an OBDD that computes function (a∧¬b)∨(b∧c)(a\wedge\neg b)\vee(b\wedge c) .
Figure 2: An example of an SDD (on the left) and a v-tree it respects (on the right).
Figure 3: An example of a forget node context when forgetting node v1v_{1} and all of its incident edges.
Figure 4: Example of four out of eight possible assignment SDDs for variables xx , yy , and zz
Figure 5: Example of an SSD for a single state from CC
More in this topic

Parameterized Complexity

Parameterized complexity studies whether hard problems become tractable when runtime depends on a small structural parameter.

See all 19 papers

Explore similar work

CardsList

  1. A canonical generalization of OBDD

    Apr 7, 2026Florent Capelli, YooJung Choi, Stefan Mengel +2

    Univ. Artois, CNRS, UMR 8188, CRIL, F-62300 Lens, France · Arizona State University · University of California, Los Angeles

  2. Monadic Second-Order Logic in HOL: Deep and Shallow with Automated Faithfulness (Extended Preprint)

    Sep 7, 2026Christoph Benzmueller, Daniel KirchnerInteractive Theorem Proving

    University of Bamberg, Bamberg, Germany · Freie Universität Berlin, Berlin, Germany

  3. A Fast Model Counting Algorithm for Two-Variable Logic with Counting and Modulo Counting Quantifiers

    May 5, 2026Shixin Sun, Astrid Klipfel, Ondřej Kuželka +2Efficient Inference

    School of Artificial Intelligence, Jilin University, Changchun 130012, China · CRIL, Université d’Artois, Lens 62307, France · Czech Technical University, Prague 160 00, Czechia +1