Weighted First Order Model Counting for Two-variable Logic with Axioms on Two Relations
Kuang, Qipeng, Kůla, Václav, Kuželka, Ondřej, Wang, Yuanhong, Wang, Yuyi
–arXiv.org Artificial Intelligence
The Weighted First-Order Model Counting Problem (WFOMC) asks to compute the weighted sum of models of a given first-order logic sentence over a given domain. The boundary between fragments for which WFOMC can be computed in polynomial time relative to the domain size lies between the two-variable fragment ($\text{FO}^2$) and the three-variable fragment ($\text{FO}^3$). It is known that WFOMC for \FOthree{} is $\mathsf{\#P_1}$-hard while polynomial-time algorithms exist for computing WFOMC for $\text{FO}^2$ and $\text{C}^2$, possibly extended by certain axioms such as the linear order axiom, the acyclicity axiom, and the connectedness axiom. All existing research has concentrated on extending the fragment with axioms on a single distinguished relation, leaving a gap in understanding the complexity boundary of axioms on multiple relations. In this study, we explore the extension of the two-variable fragment by axioms on two relations, presenting both negative and positive results. We show that WFOMC for $\text{FO}^2$ with two linear order relations and $\text{FO}^2$ with two acyclic relations are $\mathsf{\#P_1}$-hard. Conversely, we provide an algorithm in time polynomial in the domain size for WFOMC of $\text{C}^2$ with a linear order relation, its successor relation and another successor relation.
arXiv.org Artificial Intelligence
Aug-18-2025
- Country:
- Asia > China
- Hong Kong (0.04)
- Jilin Province > Changchun (0.04)
- Europe
- Belgium > Flanders
- Flemish Brabant > Leuven (0.04)
- Czechia > Prague (0.04)
- United Kingdom > England
- Cambridgeshire > Cambridge (0.04)
- Belgium > Flanders
- Asia > China
- Genre:
- Research Report > New Finding (0.66)
- Technology: