Model Enumeration of Two-Variable Logic with Quadratic Delay Complexity

TL;DR

This work studies model enumeration for the two-variable fragment of first-order logic ($\mathbf{FO}^2$) over a finite domain, fixed sentence, and variable domain size $n$. It introduces a refined domain-recursion approach that enumerates unary and binary substructures separately, achieving a delay of $\tilde{O}(n^2)$ between consecutive models (for a fixed $\Gamma$), which is near-optimal given the $\Omega(n^2)$ bits needed to specify binary predicates. The key technical engine converts substructure consistency checks into a configuration decision problem via domain reduction, Tseitin encoding, and unary encoding of binary facts, enabling constant-time qualification of configurations and a quadratic-delay overall enumeration. The method extends to $\mathbf{FO}^2$ with equality, and empirical results show stable, low-delay performance, outperforming all-SAT-based approaches. This establishes fixed-parameter tractability for FO$^2$ model enumeration and suggests avenues for extending the approach to other tractable fragments and multi-sorted logics.

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 $Γ$ 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.

Figures (4)

• Figure 1: An example of enumerating satisfiable configurations from a template configuration $(6,4,6,4)$, where $\delta = 6$ and $n = 21$.
• Figure 2: The process of model enumeration of the sentence $\Gamma_G$ over the domain $\Delta = \{v_1,v_2,v_3\}$. Arrows between graphs and their numbers show the recursion and backtracking path. The solid and dashed edges in graphs represent the 2-types $\pi_E$ and $\pi_{\neg E}$ respectively, and the green and red represent non-isolated and isolated vertices respectively. The double circle represents the chosen target vertex. The sets next to the graphs indicate the partial binary substructure determined so far. The cross indicates that the substructure of this step is not $\Delta$-consistent. We mark the determined 2-types in gray, and also mark the vertex whose 2-types have been determined in gray, indicating that they will not change in subsequent processing. When all 2-types of vertex pairs are processed, we yield a binary substructure, as shown in the last column.
• Figure 3: An example of $m=2$: Start by arbitrarily choosing $2$ elements to form $S$ and specifying them as witnesses for elements in $T$. For instance, element $a$ is assigned as the new $\beta_1$-witness of $b$ (blue line) in the step 2. Then, when processing the witnesses of $a$, we may find element $b$ as the original $\beta_2$-witness of $a$ (red line) and $\beta_1(b,a)$ and $\beta_2(a,b)$ are different. We resolve the conflict by finding the original $\beta_1$-witness of $b$ and add it to $S'$.
• Figure 4: The $m$ new internal witnesses for $e_1$, $e_{m+1}$, $e_{m+2}$ and $e_{2m+1}$ are $\{e_2, e_3, \dots, e_{m+1}\}$, $\{e_{m+2}, \dots, e_{2m+1}\}$, $\{e_{m+3}, \dots, e_{2m+1}, e_1\}$ and $\{e_1, \dots, e_m\}$, respectively.

Theorems & Definitions (36)

• Theorem 1
• Theorem 2
• Definition 1: Types
• Example 1
• Definition 2: Derivation Relation
• Proposition 1
• Proposition 2
• Remark 1
• Theorem 3
• Corollary 1