Model Enumeration of Two-Variable Logic with Quadratic Delay Complexity

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 $\Gamma$ and a positive integer $n$, how can one enumerate all the models of $\Gamma$ 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 $\Omega(n^2)$ bits to represent.

@article{meng2025_2505.19648,
  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 },
  journal={arXiv preprint arXiv:2505.19648},
  year={ 2025 }
}