Model Enumeration of Two-Variable Logic with Quadratic Delay Complexity
This addresses a computational logic problem for researchers in automated reasoning and database theory, but it is incremental as it builds on known lower bounds and focuses on a specific logic fragment.
The paper tackles the model enumeration problem for the two-variable fragment of first-order logic (FO^2) by devising a novel algorithm with quadratic delay complexity in domain size n, which is almost optimal as it matches the Ω(n^2) lower bound for representing binary predicates.
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.