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<sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">2</sup>). Specifically, given an FO<sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">2</sup> 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<sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">2</sup>) bits to represent.