# Solving Combinatorial Counting Problems with Weighted First-Order Model Counting

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 10 of its 33 references that are in the map.
- First posted on arXiv 24 May 2026.

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

- [Measuring Mathematical Problem Solving With the MATH Dataset](https://mlsanity.com/paper/2103.03874/) (2021)
- [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)
- [New Liftable Classes for First-Order Probabilistic Inference](https://mlsanity.com/paper/1610.08445/) (2016)
- [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)
- [Lifted Algorithms for Symmetric Weighted First-Order Model Sampling](https://mlsanity.com/paper/2308.08828/) (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)
- [Weighted First Order Model Counting for Two-variable Logic with Axioms on Two Relations](https://mlsanity.com/paper/2508.11515/) (2025)

## Abstract (arXiv)

Combinatorial counting problems pervade artificial intelligence, statistics, and discrete mathematics. Whether the task is enumerating subsets, multisets, permutations, partitions, or compositions under structural and arithmetic constraints, solving it remains a stubbornly manual exercise. Closed-form derivations are powerful but brittle, while naive encodings to propositional model counting or constraint satisfaction destroy the exchangeability that makes counting tractable in the first place. We present Cofola (COmbinatorial counting LAnguage with First-Order logic), a typed declarative language whose primitives are the combinatorial objects that recur in everyday counting questions, including sets, bags, tuples, sequences, circles, partitions, and compositions, together with natural relational and arithmetic constraints over them. A denotational semantics maps every Cofola program to a well-defined combinatorial counting problem, and a three-phase compilation pipeline (preprocessing, decomposition, and symmetry-preserving encoding) reduces this problem to a weighted first-order model counting (WFOMC) instance augmented with coefficient-extraction constraints. To stay inside known domain-liftable fragments whenever possible, the encoding groups indistinguishable entities, breaks the symmetry of unordered groupings lexicographically, and encodes sequences and circles via order axioms. On a suite of representative combinatorial counting problems, ranging from textbook math problems to multi-object scenarios that the closest prior framework cannot express, Cofola produces concise specifications and a uniform solving pipeline that is practical end-to-end.