pith. sign in

arxiv: 2604.08707 · v1 · submitted 2026-04-09 · 💻 cs.AI · cs.CC

Parameterized Complexity Of Representing Models Of MSO Formulas

Petr Ku\v{c}era , Petr Martinek This is my paper

Pith reviewed 2026-05-10 16:56 UTC · model grok-4.3

classification 💻 cs.AI cs.CC
keywords parameterized complexitymonadic second-order logicCourcelle's theoremsentential decision diagramsordered binary decision diagramstreewidthpathwidth
0
0 comments X

The pith

MSO2 formula models on graphs can be represented by sentential decision diagrams whose size is linear in treewidth and formula size.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper extends Courcelle's theorem, which solves the decision problem for MSO2 properties in parameterized linear time, to the task of explicitly representing all models of formulas that may have free variables. It establishes that these models can be encoded as sentential decision diagrams with size growing only linearly in the treewidth of the input graph and the length of the formula. A parallel linear-size bound is shown for ordered binary decision diagrams, but only when the parameter is pathwidth rather than treewidth. The work also proves that no such linear bound exists for ordered binary decision diagrams under treewidth alone, using an existing lower-bound construction. This supplies an explicit, compact encoding that links the classical parameterized result to techniques from knowledge representation.

Core claim

We show a parameterized linear upper bound on the size of a sentential decision diagram representing the models of an MSO2 formula when the parameter is treewidth together with formula size. We show a parameterized linear upper bound on the size of an ordered binary decision diagram when the parameter is pathwidth. Building on Razgon's 2014 lower bound, we exhibit an MSO2 formula and a class of bounded-treewidth graphs that admit no ordered binary decision diagram of size parameterized by treewidth.

What carries the argument

Dynamic-programming tables computed on a tree decomposition, compiled into a sentential decision diagram or ordered binary decision diagram without super-linear size increase.

If this is right

  • Courcelle's theorem now yields not only a yes/no answer but an explicit, compact listing of all models.
  • Further queries or manipulations of the models can be performed directly on the decision diagram without restarting the computation.
  • Knowledge-representation systems can ingest MSO2-specified graph constraints and obtain a diagram representation whose size tracks the natural parameters.
  • Pathwidth admits linear-size ordered binary decision diagrams while treewidth does not, separating the two width measures for this representation task.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Graphs whose treewidth and pathwidth are close may admit particularly compact ordered binary decision diagram encodings.
  • The same compilation technique could be tested on other decision-diagram formalisms to see which ones preserve linearity under treewidth.
  • When the diagram is small, standard diagram operations such as marginalization or sampling become feasible for MSO2-defined model sets.

Load-bearing premise

The tables produced by dynamic programming on a tree decomposition can be turned into a decision diagram without a super-linear blow-up in size.

What would settle it

An MSO2 formula and a family of graphs with bounded treewidth such that every sentential decision diagram representing the models has size growing super-linearly with the treewidth.

Figures

Figures reproduced from arXiv: 2604.08707 by Petr Ku\v{c}era, Petr Martinek.

Figure 1
Figure 1. Figure 1: An example of an OBDD that computes function (a ∧ ¬b) ∨ (b ∧ c). Definition 5 (Ordered binary decision diagram). Let < be a strict linear ordering on the set of decision variables. A decision diagram A is said to respect <, if xc < xd for every node c and its descendant d labeled with variables xc and xd respectively. If a binary decision diagram respects any ordering of decision variables, we call it an o… view at source ↗
Figure 2
Figure 2. Figure 2: An example of an SDD (on the left) and a v-tree it respects (on the right). Unlike in OBDDs, the decisions in SDDs are made based on sentences which form a partition. Definition 7 (Boolean partition). A set of boolean functions {p1, p2, . . . , pk} forms a boolean parti￾tion, if both of the following properties hold: • pi ∧ pj ≡ false for i ̸= j • Wk i=1 pi ≡ true We are now ready to define sentential deci… view at source ↗
Figure 3
Figure 3. Figure 3: An example of a forget node context when forgetting node v1 and all of its incident edges. set of edges that are being forgotten in p. We define the context of node p, denoted CTX φ,T (p), to be the following subset of Dφ,G: {[x = u] | x is a free vertex object variable in φ} ∪ {[x = e] | x is a free edge object variable in φ and e ∈ EF } ∪ {[u ∈ X] | X is a free vertex set variable in φ} ∪ {[e ∈ X] | X is… view at source ↗
Figure 4
Figure 4. Figure 4: Example of four out of eight possible assignment SDDs for variables x, y, and z 5.1.2 State Tables As SDDs The decision procedure uses state tables to calculate states for the forget and join nodes. In this subsection, we will derive a way to construct state-SDD mappings which correspond to these state tables. The construction will be used both for the join nodes and the forget nodes, and the respective su… view at source ↗
Figure 5
Figure 5. Figure 5: Example of an SSD for a single state from C Finally, we define the full state-SDD mapping gC as: gC (c) := αc This state-SDD mapping respects node(tA, node(tB, x)). An example of the construction of gC for a single state can be seen in [PITH_FULL_IMAGE:figures/full_fig_p028_5.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 2 minor

Summary. The paper extends Courcelle's theorem from decision to explicit model representation for MSO2 formulas with free variables. It claims parameterized linear upper bounds on the size of SDDs parameterized by treewidth and formula size, and on OBDDs parameterized by pathwidth and formula size, via dynamic programming on decompositions. It also shows that no such parameterized linear OBDD bound exists for treewidth, by reduction from Razgon's 2014 OBDD lower bound on a suitable MSO2 formula and bounded-treewidth graph family.

Significance. If the upper-bound constructions hold, the work supplies the first explicit, linearly sized decision-diagram representations of MSO2 models, directly connecting Courcelle-style FPT algorithms to knowledge-representation formalisms and enabling enumeration or counting tasks that pure decision procedures do not. The separation result cleanly separates the representational power of SDDs versus OBDDs under treewidth.

major comments (1)
  1. [Construction of the decision diagrams (upper bounds)] The central upper-bound claims rest on a dynamic-programming construction that converts a tree decomposition into an SDD (treewidth case) or OBDD (pathwidth case) while preserving linear dependence on the parameters. The manuscript does not exhibit the state encoding or the precise size analysis showing that the diagram size remains O(f(|φ|)·tw) rather than incurring an extra factor exponential in the number of states or formula size; this step is load-bearing for both linear bounds.
minor comments (2)
  1. [Abstract] The abstract and introduction use the phrase 'parameterized linear' without stating the exact functional form (e.g., whether the hidden function of |φ| is single-exponential or worse).
  2. [Lower bound section] The lower-bound argument invokes Razgon (2014) but does not restate the precise graph family or the MSO2 formula used to obtain the separation; a short self-contained sketch would improve readability.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful review and for highlighting the need for greater clarity in the dynamic-programming construction. We have revised the manuscript to address this point directly by expanding the relevant sections with explicit state encodings and size analyses.

read point-by-point responses

  1. Referee: The central upper-bound claims rest on a dynamic-programming construction that converts a tree decomposition into an SDD (treewidth case) or OBDD (pathwidth case) while preserving linear dependence on the parameters. The manuscript does not exhibit the state encoding or the precise size analysis showing that the diagram size remains O(f(|φ|)·tw) rather than incurring an extra factor exponential in the number of states or formula size; this step is load-bearing for both linear bounds.

    Authors: We agree that the original presentation of the DP construction was insufficiently detailed on the state encoding and the precise size analysis. In the revised manuscript we have added a new subsection (Section 4.2) that explicitly defines the states as the standard MSO2 types over the bag (i.e., the equivalence classes of assignments to the free variables and the quantified sets, whose number is bounded by a function g(|φ|) of the formula size alone). The transition function between bags is realized by a constant-size SDD/OBDD fragment per bag vertex; because each bag contributes at most O(g(|φ|)) nodes and there are O(tw) bags in a nice decomposition, the total diagram size is O(g(|φ|)·tw). We also include a formal induction proving that no additional exponential blow-up occurs when the fragments are composed. This establishes the claimed linear dependence on the parameters. revision: yes

Circularity Check

0 steps flagged

No significant circularity in derivation chain

full rationale

The paper extends Courcelle's theorem (an external, well-established result) by constructing decision-diagram representations of MSO2 models via dynamic programming on tree decompositions, yielding linear-size SDDs (parameterized by treewidth) and OBDDs (parameterized by pathwidth). The lower-bound separation for OBDDs explicitly invokes Razgon (2014), an independent external citation with no author overlap. No self-citations are load-bearing, no parameters are fitted and then renamed as predictions, and no ansatz or uniqueness claim reduces to prior work by the same authors. The central claims rest on standard FPT techniques and an external lower bound, remaining self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The result rests on the standard correctness of Courcelle's theorem and the algebraic properties of SDDs and OBDDs; no free parameters or new postulated entities are introduced.

axioms (2)
  • domain assumption Courcelle's theorem: MSO2 properties are decidable in linear time parameterized by treewidth and formula size
    The paper explicitly extends this theorem to model representation.
  • standard math Standard size and semantics of sentential decision diagrams and ordered binary decision diagrams
    Used to state the upper bounds on diagram size.

pith-pipeline@v0.9.0 · 5510 in / 1410 out tokens · 73892 ms · 2026-05-10T16:56:05.970456+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

8 extracted references · 8 canonical work pages

  1. [1]

    Connecting Width and Structure in Knowledge Compilation

    Amarilli, A., M. Monet, and P. Senellart (2018). “Connecting Width and Structure in Knowledge Compilation”. In:21st International Conference on Database Theory (ICDT 2018). Ed. by B. Kimelfeld and Y. Amsterdamer. Vol

    work page 2018

  2. [2]

    Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl, Germany: Schloss Dagstuhl – Leibniz-Zentrum f¨ ur Informatik, 6:1–6:17.isbn: 978-3- 95977-063-7.doi:10.4230/LIPIcs.ICDT.2018.6.url:https://drops.dagstuhl.de/entities/ document/10.4230/LIPIcs.ICDT.2018.6. Bollob´ as, B. (1998).Modern Graph Theory. Vol

    work page doi:10.4230/lipics.icdt.2018.6.url:https://drops.dagstuhl.de/entities/ 2018

  3. [3]

    SDDs Are Exponentially More Succinct than OBDDs

    Graduate Texts in Mathematics. Springer. Bova, S. (Feb. 2016). “SDDs Are Exponentially More Succinct than OBDDs”. In:Proceedings of the AAAI Conference on Artificial Intelligence30.1.doi:10.1609/aaai.v30i1.10107.url:https: //ojs.aaai.org/index.php/AAAI/article/view/10107. Bryant, R. E. (1986). “Graph-based algorithms for boolean function manipulation”. In...

    work page doi:10.1609/aaai.v30i1.10107.url:https: 2016

  4. [4]

    A knowledge compilation map

    Darwiche, A. and P. Marquis (2002). “A knowledge compilation map”. In:Journal of Artificial Intelli- gence Research17, pp. 229–264. Edmund M. Clarke, J., O. Grumberg, and D. A. Peled (1999).Model checking. Cambridge, MA, USA: MIT Press.isbn: 0-262-03270-8. Flum, J. and M. Grohe (2006).Parameterized complexity theory. 1st. Vol

    work page 2002

  5. [5]

    Mona: Monadic second-order logic in practice

    Texts in Theoretical Computer Science. An EATCS Series. Springer-Verlag Berlin Heidelberg. Henriksen, J. G. et al. (1995). “Mona: Monadic second-order logic in practice”. In:Tools and Algorithms for the Construction and Analysis of Systems: First International Workshop, TACAS’95 Aarhus, Denmark, May 19–20, 1995 Selected Papers

    work page 1995

  6. [6]

    A Practical Approach to Courcelle’s Theorem

    Springer, pp. 89–110. Kloks, T. (1994).Treewidth: computations and approximations. Springer. 37 Kneis, J. and A. Langer (2009). “A Practical Approach to Courcelle’s Theorem”. In:Electronic Notes in Theoretical Computer Science251. Proceedings of the International Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2008), ...

    work page 1994

  7. [7]

    Evaluation of an MSO-solver

    Ed. by O. Beyersdorff and C. M. Wintersteiger. Cham: Springer International Publishing, pp. 235–252.isbn: 978-3-319-94144-8. Langer, A. et al. (2012). “Evaluation of an MSO-solver”. In:2012 Proceedings of the Meeting on Algo- rithm Engineering and Experiments (ALENEX). SIAM, pp. 55–63.doi:10.1137/1.9781611972924

    work page doi:10.1137/1.9781611972924 2012

  8. [8]

    On OBDDs for CNFs of bounded treewidth

    eprint:https : / / epubs . siam . org / doi / pdf / 10 . 1137 / 1 . 9781611972924 . 5.url:https : //epubs.siam.org/doi/abs/10.1137/1.9781611972924.5. Razgon, I. (2014). “On OBDDs for CNFs of bounded treewidth”. In. Shou, O., K. Jun, and M. Shin-ichi (June 2023). “On construction of decision diagrams represent- ing Boolean functions given as monadic second...

    work page doi:10.1137/1.9781611972924.5 2014