一句话：提出 FO2 模型枚举算法，在固定句子下延迟复杂度为 O(n² polylog n)，接近理论下界。
论文研究无量词、有限域片段二变量一阶逻辑（FO2）的模型枚举问题：给定 FO2 句子 Γ 和正整数 n，枚举 Γ 在大小为 n 的域上的所有模型。作者设计了一种新算法，并分析其延迟复杂度，即连续输出两个模型之间的时间。当句子固定时，该算法的延迟复杂度为域大小 n 的二次时间（忽略对数因子）。由于任何模型中二元谓词的解释至少需要 Ω(n²) 比特表示，这一复杂度几乎最优。该工作为 FO2 模型枚举提供了接近下界的理论算法。
We study the model enumeration problem of the function-free, finite domain fragment of first-order logic with two variables (FO2). Specifically, given an FO2sentence Γ 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 Ω(n2) bits to represent.
DOI 原文 ·
@inproceedings{paperbot8647,
title = {Model Enumeration of Two-Variable Logic with Quadratic Delay Complexity},
author = {Qiaolan Meng and Juhua Pu and Hongting Niu and Yuyi Wang and Yuanhong Wang and Ondřej Kuželka},
booktitle = {LICS},
year = {2025},
doi = {10.1109/lics65433.2025.00030}
}