用决策图高效表示可满足的MSO公式模型，提升参数化推理效率。
Parameterized Complexity Of Representing Models Of MSO Formulas
- 用SDD和OBDD表示带自由变量的MSO2公式模型，大小与树宽/路径宽线性相关。
- 给出SDD大小的参数化线性上界，且对某些图类，OBDD无法实现参数化压缩。
- 揭示了柯尔塞尔定理与知识表示的联系，适合参数复杂性与逻辑推理研究者。
一阶二元逻辑（MSO2）在参数化复杂性中具有重要地位，因其柯尔塞尔定理：给定图的性质由特定MSO2公式描述时，可通过以图的树宽和公式大小为参数的线性时间算法判定。本文拓展该结果，证明带自由变量的MSO2公式的模型可用决策图表示，其大小与上述参数呈线性关系。具体而言，在考虑树宽时，句子决策图（SDD）大小有参数化线性上界；在路径宽下，有序二叉决策图（OBDD）也存在类似上界。此外，基于Razgon（2014）关于OBDD大小的下界，我们证明存在一类有界树宽图，其上的某些MSO2公式无法用以树宽为参数的OBDD有效表示。本成果为柯尔塞尔定理提供了新视角，并将其与知识表示领域相连接。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。