# Model Enumeration of Two-Variable Logic with Quadratic Delay Complexity

arXiv: https://arxiv.org/abs/2505.19648 · HTML: https://mlsanity.com/paper/2505.19648/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 8 of its 31 references that are in the map.
- First posted on arXiv 26 May 2025.

## Builds on (most cited first, 8 of 8)

- [Symmetric Weighted First-Order Model Counting](https://mlsanity.com/paper/1412.1505/) (2014)
- [Weighted First-Order Model Counting in the Two-Variable Fragment With Counting Quantifiers](https://mlsanity.com/paper/2007.05619/) (2020)
- [Domain Recursion for Lifted Inference with Existential Quantifiers](https://mlsanity.com/paper/1707.07763/) (2017)
- [Implementing Efficient All Solutions SAT Solvers](https://mlsanity.com/paper/1510.00523/) (2015)
- [Lifted Algorithms for Symmetric Weighted First-Order Model Sampling](https://mlsanity.com/paper/2308.08828/) (2023)
- [On Exact Sampling in the Two-Variable Fragment of First-Order Logic](https://mlsanity.com/paper/2302.02730/) (2023)
- [Towards a more efficient approach for the satisfiability of two-variable logic](https://mlsanity.com/paper/2104.10621/) (2021)
- [Enumerating Answers to First-Order Queries over Databases of Low Degree](https://mlsanity.com/paper/2010.08382/) (2020)

## Built on by (most cited first, 1 of 1)

- [A Fast Model Counting Algorithm for Two-Variable Logic with Counting and Modulo Counting Quantifiers](https://mlsanity.com/paper/2605.03391/) (2026)

## Abstract (arXiv)

We study the model enumeration problem of the function-free, finite domain fragment of first-order logic with two variables (FO2). Specifically, given an FO2 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(n2) bits to represent.