English

Weighted First Order Model Counting for Two-variable Logic with Axioms on Two Relations

Logic in Computer Science 2025-08-18 v1 Artificial Intelligence

Abstract

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 (FO2\text{FO}^2) and the three-variable fragment (FO3\text{FO}^3). It is known that WFOMC for \FOthree{} is #P1\mathsf{\#P_1}-hard while polynomial-time algorithms exist for computing WFOMC for FO2\text{FO}^2 and C2\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 FO2\text{FO}^2 with two linear order relations and FO2\text{FO}^2 with two acyclic relations are #P1\mathsf{\#P_1}-hard. Conversely, we provide an algorithm in time polynomial in the domain size for WFOMC of C2\text{C}^2 with a linear order relation, its successor relation and another successor relation.

Keywords

Cite

@article{arxiv.2508.11515,
  title  = {Weighted First Order Model Counting for Two-variable Logic with Axioms on Two Relations},
  author = {Qipeng Kuang and Václav Kůla and Ondřej Kuželka and Yuanhong Wang and Yuyi Wang},
  journal= {arXiv preprint arXiv:2508.11515},
  year   = {2025}
}

Comments

24 pages, 5 figures

R2 v1 2026-07-01T04:52:00.050Z