提出一种高效枚举二元一阶逻辑模型的算法，延迟仅随数据规模平方增长。
Model Enumeration of Two-Variable Logic with Quadratic Delay Complexity
- 基于新算法设计，固定公式时模型间生成延迟为O(n²)（含对数因子）
- 延迟复杂度接近理论下界，因二元谓词需至少Ω(n²)位存储
- 适合逻辑推理、形式验证等需要完整模型枚举的场景
本文研究无函数、有限域的二变量一阶逻辑（FO²）的模型枚举问题。给定一个FO²句子Γ和正整数n，如何枚举所有在大小为n的域上的Γ模型？本文提出一种新算法，当公式固定时，其延迟复杂度（连续生成两个模型所需时间）在域大小n上为二次方（含对数因子）。该复杂度几乎最优，因为任何模型中二元谓词的解释至少需要Ω(n²)比特表示。
原文摘要 · Abstract (English)
We study the model enumeration problem of the function-free, finite domain fragment of first-order logic with two variables ($FO^2$). Specifically, given an $FO^2$ sentence $Γ$ and a positive integer $n$, how can one enumerate all the models of $Γ$ over a domain of size $n$? In this paper, we devise a novel algorithm to address this problem. The delay complexity, the time required between producing two consecutive models, of our algorithm is quadratic in the given domain size $n$ (up to logarithmic factors) when the sentence is fixed. This complexity is almost optimal since the interpretation of binary predicates in any model requires at least $Ω(n^2)$ bits to represent.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。