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

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