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

TL;DR

This paper investigates the complexity of weighted first-order model counting in two-variable logic with axioms on two relations, identifying both hardness results and a polynomial-time algorithm for specific cases.

Contribution

It extends the understanding of WFOMC complexity to two relations, providing new hardness results and a polynomial-time algorithm for certain axiomatic extensions.

Findings

WFOMC with two linear order relations is #P_1-hard.

WFOMC with two acyclic relations is #P_1-hard.

Polynomial-time algorithm for C^2 with linear and successor 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 ($\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.