针对有序域的前驱关系，提出高效推理算法，速度提升一个数量级。
Faster Lifting for Ordered Domains with Predecessor Relations
- 将前驱关系作为公理原生支持，避免传统编码带来的计算开销。
- 对一阶和二阶前驱关系实现指数级加速，通用k阶前驱也有效。
- 适合需要高效逻辑推理的自动化系统与组合数学问题求解者。
本文研究在具有前驱关系的有序域上的提升推理（lifted inference）。域中元素遵循全序（循环）关系，每个元素有唯一的顺时针前驱。现有方法通过加权一阶模型计数（WFOMC）处理该问题，通常用线性序公理引入二元谓词以建立域元素的线性排序，再由该谓词定义直接和第二前驱关系。尽管理论可解，现有算法在涉及前驱关系时效率低下。本文将前驱关系视为公理的原生部分，设计新算法，天然支持这些关系。实验表明，该算法对直接和第二前驱关系实现指数级加速，并可推广至一般k阶前驱。在提升推理任务与组合数学问题上的大量实验验证了其高效性，速度提升达一个数量级。
原文摘要 · Abstract (English)
We investigate lifted inference on ordered domains with predecessor relations, where the elements of the domain respect a total (cyclic) order, and every element has a distinct (clockwise) predecessor. Previous work has explored this problem through weighted first-order model counting (WFOMC), which computes the weighted sum of models for a given first-order logic sentence over a finite domain. In WFOMC, the order constraint is typically encoded by the linear order axiom introducing a binary predicate in the sentence to impose a linear ordering on the domain elements. The immediate and second predecessor relations are then encoded by the linear order predicate. Although WFOMC with the linear order axiom is theoretically tractable, existing algorithms struggle with practical applications, particularly when the predecessor relations are involved. In this paper, we treat predecessor relations as a native part of the axiom and devise a novel algorithm that inherently supports these relations. The proposed algorithm not only provides an exponential speedup for the immediate and second predecessor relations, which are known to be tractable, but also handles the general k-th predecessor relations. The extensive experiments on lifted inference tasks and combinatorics math problems demonstrate the efficiency of our algorithm, achieving speedups of a full order of magnitude.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。