在受限图结构下，高效计算带证据的逻辑模型计数。
Tractable Weighted First-Order Model Counting with Bounded Treewidth Binary Evidence
- 限定二元证据的图结构为有界树宽，突破原有不可行性
- 对两个变量逻辑片段实现域大小多项式时间求解
- 适用于有界度图上的稳定座位安排等组合问题
加权一阶模型计数（WFOMC）旨在计算给定一阶逻辑句在指定域上的加权模型总和。在证据条件下（固定一组基原子真值）进行WFOMC已被证明在域大小上多项式时间内不可行（除非#P ⊆ FP），即使对原本可解的逻辑片段也是如此。本文通过将二元证据限制在底层Gaifman图具有有界树宽的情形，突破这一障碍。我们为两个变量逻辑片段FO²和C²设计了域大小多项式时间的算法。此外，展示了该算法在组合问题中的应用，解决了有界度且有界树宽图上的稳定座位安排问题（此前未解决）。实验表明，该算法在可扩展性上优于现有模型计数求解器。
原文摘要 · Abstract (English)
The Weighted First-Order Model Counting Problem (WFOMC) asks to compute the weighted sum of models of a given first-order logic sentence over a given domain. Conditioning WFOMC on evidence -- fixing the truth values of a set of ground literals -- has been shown impossible in time polynomial in the domain size (unless $\mathsf{\#P \subseteq FP}$) even for fragments of logic that are otherwise tractable for WFOMC without evidence. In this work, we address the barrier by restricting the binary evidence to the case where the underlying Gaifman graph has bounded treewidth. We present a polynomial-time algorithm in the domain size for computing WFOMC for the two-variable fragments $\text{FO}^2$ and $\text{C}^2$ conditioned on such binary evidence. Furthermore, we show the applicability of our algorithm in combinatorial problems by solving the stable seating arrangement problem on bounded-treewidth graphs of bounded degree, which was an open problem. We also conducted experiments to show the scalability of our algorithm compared to the existing model counting solvers.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。