Model Enumeration of Two-Variable Logic with Quadratic Delay Complexity

TL;DR

This paper introduces a new algorithm for enumerating all models of a two-variable first-order logic sentence over finite domains, achieving near-optimal quadratic delay complexity.

Contribution

The paper presents a novel enumeration algorithm for $FO^2$ logic models with quadratic delay, improving efficiency and approaching theoretical optimality.

Findings

Delay complexity is quadratic in domain size, up to logarithmic factors.

The algorithm is nearly optimal given the information-theoretic lower bound.

Provides a practical method for model enumeration in finite domain logic.

Abstract

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.