# Towards Practical First-Order Model Counting

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

## Key facts

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

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

- [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)
- [Weighted Model Counting in FO2 with Cardinality Constraints and Counting Quantifiers: A Closed Form Formula](https://mlsanity.com/paper/2110.05992/) (2021)
- [Lifted Algorithms for Symmetric Weighted First-Order Model Sampling](https://mlsanity.com/paper/2308.08828/) (2023)
- [On Discovering Interesting Combinatorial Integer Sequences](https://mlsanity.com/paper/2302.04606/) (2023)
- [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)
- [Synthesising Recursive Functions for First-Order Model Counting: Challenges, Progress, and Conjectures](https://mlsanity.com/paper/2306.04189/) (2023)

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

- [A Fast Model Counting Algorithm for Two-Variable Logic with Counting and Modulo Counting Quantifiers](https://mlsanity.com/paper/2605.03391/) (2026)

## Abstract (arXiv)

First-order model counting (FOMC) is the problem of counting the number of models of a sentence in first-order logic. Since lifted inference techniques rely on reductions to variants of FOMC, the design of scalable methods for FOMC has attracted attention from both theoreticians and practitioners over the past decade. Recently, a new approach based on first-order knowledge compilation was proposed. This approach, called Crane, instead of simply providing the final count, generates definitions of (possibly recursive) functions that can be evaluated with different arguments to compute the model count for any domain size. However, this approach is not fully automated, as it requires manual evaluation of the constructed functions. The primary contribution of this work is a fully automated compilation algorithm, called Crane2, which transforms the function definitions into C++ code equipped with arbitrary-precision arithmetic. These additions allow the new FOMC algorithm to scale to domain sizes over 500,000 times larger than the current state of the art, as demonstrated through experimental results.