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

arXiv: https://arxiv.org/abs/2508.11515 · HTML: https://mlsanity.com/paper/2508.11515/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 6 of its 30 references that are in the map.
- First posted on arXiv 15 Aug 2025.

## Builds on (most cited first, 6 of 6)

- [Skolemization for Weighted First-Order Model Counting](https://mlsanity.com/paper/1312.5378/) (2013)
- [Weighted model counting beyond two-variable logic](https://mlsanity.com/paper/1804.10185/) (2018)
- [Lifted Inference with Linear Order Axiom](https://mlsanity.com/paper/2211.01164/) (2022)
- [On Discovering Interesting Combinatorial Integer Sequences](https://mlsanity.com/paper/2302.04606/) (2023)
- [Lifted Inference beyond First-Order Logic](https://mlsanity.com/paper/2308.11738/) (2023)
- [Bridging Weighted First Order Model Counting and Graph Polynomials](https://mlsanity.com/paper/2407.11877/) (2024)

## Built on by (most cited first, 1 of 1)

- [Solving Combinatorial Counting Problems with Weighted First-Order Model Counting](https://mlsanity.com/paper/2605.24845/) (2026)

## Abstract (arXiv)

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.