Model Enumeration of Two-Variable Logic with Quadratic Delay Complexity

2025/05/26 by Qiaolan Meng, Juhua Pu, Meng, Qiaolan +8
Computer Science · #Advanced Algebra and Logic #Artificial Intelligence (cs.AI) #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #semigroups and automata theory

paper · pdf · doi:10.48550/arxiv.2505.19648

openalex publication_date 2025/05/26 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

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

Citations

• On Exact Sampling in the Two-Variable Fragment of First-Order Logic
• Towards a more efficient approach for the satisfiability of two-variable logic
• Weighted First-Order Model Counting in the Two-Variable Fragment With\n Counting Quantifiers
• Domain Recursion for Lifted Inference with Existential Quantifiers
• Symmetric Weighted First-Order Model Counting
• Solving SAT and SAT Modulo Theories
• First-order queries on structures of bounded degree are computable with constant delay

Related

• Weighted First Order Model Counting for Two-variable Logic with Axioms on Two Relations
• On Exact Sampling in the Two-Variable Fragment of First-Order Logic
• Weighted model counting beyond two-variable logic
• Complexity of Weighted First-Order Model Counting in the Two-Variable Fragment with Counting Quantifiers: A Bound to Beat
• Enumeration Complexity of Poor Man's Propositional Dependence Logic