AI 中文总结
本研究针对有序域提出带线性序公理的WFOMC多项式时间算法，还分析双线性序场景的WFOMC复杂度，推进了该问题的难解性边界。
AI 中文摘要
加权一阶模型计数问题（WFOMC）要求计算一阶逻辑句子在某个论域上的模型的加权和，它是统计关系学习中的基础问题，应用范围延伸至枚举组合学和图多项式。计算三变量片段的WFOMC是#P₁困难的，而对于两变量片段及其添加基数约束和计数量词的扩展，存在多项式时间算法。在本研究中，我们探索在线性有序域上以多项式时间计算WFOMC，从而实现涉及序列的推理场景和组合问题的易处理推理。由于在标准一阶逻辑中编码线性序需要三个变量，这会破坏我们的多项式时间目标，因此我们直接将线性序公理添加到语言中，强制一个谓词对论域元素施加全序。我们首先证明，带有线性序公理的WFOMC可以在论域大小的多项式时间内求解。随后我们将该结果扩展到可访问后继关系的有序域，当后继关系通过线性序显式定义时该结论成立，我们还展示了一种替代的隐式方法，其中后继关系是公理的一部分，这种隐式方法在所有测试实例上都表现出显著更好的性能，有时可提供指数级的运行时间改进。最后，我们分析带有两个不同线性序的场景，证明带有两个线性序的两变量片段上的WFOMC是#P₁困难的，但我们开发了一种带有一个线性序和另一个后继关系的WFOMC的多项式时间算法，进一步推进了难解性边界，不过仍留下了能接近第二个完整线性序的程度的问题。
英文摘要
The Weighted First-Order Model Counting Problem (WFOMC) asks for the weighted sum of models of a first-order logical sentence over a domain. It is a fundamental problem in statistical relational learning, with applications extending to enumerative combinatorics and graph polynomials. Computing WFOMC for the three-variable fragment is $\mathsf{\#P}_1$-hard, whereas polynomial-time algorithms exist for the two-variable fragment and its extensions by cardinality constraints and counting quantifiers. In this work, we explore computing WFOMC in polynomial time over linearly ordered domains, enabling tractable reasoning across inference scenarios and combinatorial problems involving sequences. Because encoding a linear order in standard first-order logic requires three variables, negating our polynomial-time aspirations, we add a linear order axiom directly to the language. This forces one predicate to impose a total ordering on domain elements. We first prove that WFOMC with the linear order axiom can be solved in time polynomial in the domain size. We then extend this result to ordered domains with access to successor relations. While this holds when successors are explicitly defined via the linear order, we demonstrate an alternative implicit approach where successor relations are part of the axiom. This implicit method exhibits significantly better performance on all tested instances, sometimes providing exponential runtime improvements. Finally, we analyze scenarios with two distinct linear orders. We show that WFOMC over the two-variable fragment with two linear orders is $\mathsf{\#P}_1$-hard. However, we develop a polynomial-time algorithm for WFOMC with one linear order and a successor relation of another, pushing the intractability barrier further, yet still leaving the question of how close to a second full linear order one can get.
CommentsSubmitted to JAIR
