# Tractable Weighted First-Order Model Counting with Bounded Treewidth Binary Evidence

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 13 of its 28 references that are in the map.
- First posted on arXiv 12 Nov 2025.

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

- [Symmetric Weighted First-Order Model Counting](https://mlsanity.com/paper/1412.1505/) (2014)
- [Weighted First-Order Model Counting in the Two-Variable Fragment With Counting Quantifiers](https://mlsanity.com/paper/2007.05619/) (2020)
- [Skolemization for Weighted First-Order Model Counting](https://mlsanity.com/paper/1312.5378/) (2013)
- [Lifted Inference with Linear Order Axiom](https://mlsanity.com/paper/2211.01164/) (2022)
- [Lifted Algorithms for Symmetric Weighted First-Order Model Sampling](https://mlsanity.com/paper/2308.08828/) (2023)
- [On the Complexity and Approximation of Binary Evidence in Lifted Inference](https://mlsanity.com/paper/1311.6591/) (2013)
- [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)
- [Complexity of Weighted First-Order Model Counting in the Two-Variable Fragment with Counting Quantifiers: A Bound to Beat](https://mlsanity.com/paper/2404.12905/) (2024)
- [Stable Dinner Party Seating Arrangements](https://mlsanity.com/paper/2305.09549/) (2023)
- [Hedonic Seat Arrangement Problems](https://mlsanity.com/paper/2002.10898/) (2020)
- [Topological Distance Games](https://mlsanity.com/paper/2211.11000/) (2022)

## 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. Conditioning WFOMC on evidence -- fixing the truth values of a set of ground literals -- has been shown impossible in time polynomial in the domain size (unless mathsf#P subseteq FP) even for fragments of logic that are otherwise tractable for WFOMC without evidence. In this work, we address the barrier by restricting the binary evidence to the case where the underlying Gaifman graph has bounded treewidth. We present a polynomial-time algorithm in the domain size for computing WFOMC for the two-variable fragments FO2 and C2 conditioned on such binary evidence. Furthermore, we show the applicability of our algorithm in combinatorial problems by solving the stable seating arrangement problem on bounded-treewidth graphs of bounded degree, which was an open problem. We also conducted experiments to show the scalability of our algorithm compared to the existing model counting solvers.