Papers › Model Enumeration of Two-Variable Logic with Quadratic Delay Complexity
Model Enumeration of Two-Variable Logic with Quadratic Delay Complexity
Qiaolan Meng, Juhua Pu, Hongting Niu, Yuyi Wang, Yuanhong Wang, Ondřej Kuželka
We study the model enumeration problem of the function-free, finite domain fragment of first-order logic with two variables (FO²). Specifically, given an FO² 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²) bits to represent.
Code
Repository list and official/mentioned flags are the archive's, frozen 2025-07-28. Reachability, where shown, is from one Syntology probe window (2026-09-16 to 2026-09-18); repositories not probed show nothing. GitHub stars are not tracked.
Code Syntology ran Syntology
Not run by Syntology. Nothing on this page verifies that the listed code works.
Tasks
Results from the paper archive 2025-07-28
No leaderboard rows for this paper in the archive.
Report a problem or propose a change · a person checks every report against the paper or source before anything changes; decisions are listed on /corrections