# Counting solutions to extended MSO formulas, and sampling — do these appear in the literature?

I am trying to determine if the literature contains various extensions of Courcelle's theorem. Since I haven't been able to find these in the literature, I guess that these are folklore results, or else false, since it seems that their proofs are only a few steps away from what appears in the literature already.

Background:

1) $$EMS$$ is an extension of $$MSO$$ that, among other things, allows the comparison of the cardinality of set variables. See the discussion around definition 3.4 of this paper for a more precise description.

It is proven in the previously linked paper (Theorem 5.4) that $$EMS$$ decision problems are $$XP$$ in the tree-width.

2) It is proven in the same paper (Theorem 5.7) that $$MSO$$ counting problems are $$FPT$$ in the tree-width. (The definition of an enumeration problem appears on the top of page 317.)

Question 1: I think it is also true that $$EMS$$ counting problems are $$XP$$ in the tree-width. Does anyone know if this is explicitly stated anywhere in the literature?

Proof sketch for the claim of question 1: The broad steps of the argument should be the same as the proof of Theorem 5.7: one can polynomial time interpret the class of graphs of tree-width $$\leq m$$ into the class of rooted binary trees as described theorem 4.5. The transformation of an EMS problem $$P$$ on graphs into a corresponding EMS problem over binary trees induces a bijective correspondence of solution sets (remarks on page 322). Then, similarly to what is described prior to Theorem 5.7, the evaluation of the $$MSO$$ formula tree-automata on the labelled tree will be modified keep track of counts for the number of occurrences of all possible pairs of $$(\text{tree automata state}, \text{evaluations})$$ at each node of the tree. The total number of solutions can then be read off of the root by summing up the counts of all of the $$(\text{tree automata state}, \text{evaluations})$$ pairs at the root node that satisfy the $$EMS$$ formula. This will be pseudopolynomial in the total (multiplicative) height of the coefficients of the evaluations, since one will need a tree-automata-states-many counters for each possible sub-evaluation. (The number of tree-automata-states is constant, since it is determined by the $$MSO$$ formula, but the number of sub-evaluations grows pseudopolynomially.)

Similarly:

Question 2: Likewise, one should obtain in the same way an algorithm for computing generating functions for the set of solutions to an EMS formula over some given weights, as in this paper by Courcelle et al.. Does this appear in the literature anywhere?

Question 3: The same general kind of argument would show that it is possible to count the number of solutions to some formula $$\phi(X,A,B)$$ where $$X$$ is a free variable, and $$A$$ and $$B$$ are set-valued parameters, $$FPT$$ in tree-width if $$\phi \in MSO_2$$ or $$XP$$ in tree-width if $$\phi \in EMS$$ (with a constant that depends on the tree-width and $$\phi$$, not the choice of $$A$$ and $$B$$). In particular, by defining $$\phi(X,A,B) = \psi(X) \wedge ( A \cap X = \emptyset) \wedge ( B \subseteq A)$$, where $$\psi \in MSO$$ (resp. EMS), this means that one can make the necessary marginal counts in order to uniformly sample from the set of solutions to $$\psi$$ $$FTP$$ in tree-width (resp. $$XP$$ in tree-width). Similar (pseudopolynomial) statements for sampling from distributions of sets where probabilities are proportional to multiplying node/edge weights over the subset also ought to exist by similar reasoning. Does a statement like this about tree-width FPT/XP algorithms for MSO/EMS sampling problems appear in the literature anywhere?