Model Enumeration of Two-Variable Logic with Quadratic Delay Complexity
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866916759225761792 |
|---|---|
| author | Meng, Qiaolan Pu, Juhua Niu, Hongting Wang, Yuyi Wang, Yuanhong Kuželka, Ondřej |
| author_facet | Meng, Qiaolan Pu, Juhua Niu, Hongting Wang, Yuyi Wang, Yuanhong Kuželka, Ondřej |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_19648 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Model Enumeration of Two-Variable Logic with Quadratic Delay Complexity Meng, Qiaolan Pu, Juhua Niu, Hongting Wang, Yuyi Wang, Yuanhong Kuželka, Ondřej Logic in Computer Science Artificial Intelligence 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. |
| title | Model Enumeration of Two-Variable Logic with Quadratic Delay Complexity |
| topic | Logic in Computer Science Artificial Intelligence |
| url | https://arxiv.org/abs/2505.19648 |