arXiv Open Access 2025

Model Enumeration of Two-Variable Logic with Quadratic Delay Complexity

Qiaolan Meng Juhua Pu Hongting Niu Yuyi Wang Yuanhong Wang +1 lainnya

Lihat Sumber

Abstrak

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.

Topik & Kata Kunci

cs.LO cs.AI

Penulis (6)

Qiaolan Meng

Juhua Pu

Hongting Niu

Yuyi Wang

Yuanhong Wang

Ondřej Kuželka

Format Sitasi

APA MLA BibTeX

Meng, Q., Pu, J., Niu, H., Wang, Y., Wang, Y., Kuželka, O. (2025). Model Enumeration of Two-Variable Logic with Quadratic Delay Complexity. https://arxiv.org/abs/2505.19648

Akses Cepat

Lihat di Sumber

Informasi Jurnal

Tahun Terbit: 2025
Bahasa: en
Sumber Database: arXiv
Akses: Open Access ✓