Weighted First Order Model Counting for Two-variable Logic with Axioms on Two Relations
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 () and the three-variable fragment (). It is known that WFOMC for \FOthree{} is -hard while polynomial-time algorithms exist for computing WFOMC for and , 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 with two linear order relations and with two acyclic relations are -hard. Conversely, we provide an algorithm in time polynomial in the domain size for WFOMC of with a linear order relation, its successor relation and another successor relation.
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