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.

翻译：一元二阶逻辑(MSO2)因库尔塞勒定理在参数化复杂度中扮演重要角色。该定理指出，验证给定图是否满足给定MSO2公式所指定性质的问题，可通过关于图树宽和公式规模的参数化线性时间算法求解。我们通过证明带有自由变量的MSO2公式模型可用决策图表示，且其规模在所述参数上呈参数化线性关系，从而扩展了这一结果。特别地，我们证明了在考虑树宽时，语句决策图(SDD)规模存在参数化线性上界；在考虑路径宽作为参数时，有序二元决策图(OBDD)规模亦存在参数化线性上界。此外，基于Razgon(2014)关于OBDD规模的下界结论，我们证明存在某个MSO2公式及一类具有有界树宽的图，它们不承认OBDD的规模可由树宽参数化。本研究为库尔塞勒定理提供了新视角，并将其与知识表示领域联系起来。