# Synthesising Recursive Functions for First-Order Model Counting: Challenges, Progress, and Conjectures

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 9 of its 29 references that are in the map.
- First posted on arXiv 7 Jun 2023.

## 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)
- [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)
- [Manthan: A Data Driven Approach for Boolean Function Synthesis](https://mlsanity.com/paper/2005.06922/) (2020)
- [Weighted Model Counting in FO2 with Cardinality Constraints and Counting Quantifiers: A Closed Form Formula](https://mlsanity.com/paper/2110.05992/) (2021)
- [Approximate Weighted First-Order Model Counting: Exploiting Fast Approximate Model Counters and Symmetry](https://mlsanity.com/paper/2001.05263/) (2020)
- [Approximate Lifted Inference with Probabilistic Databases](https://mlsanity.com/paper/1412.1069/) (2014)

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

- [Towards Practical First-Order Model Counting](https://mlsanity.com/paper/2502.12278/) (2025)

## Abstract (arXiv)

First-order model counting (FOMC) is a computational problem that asks to count the models of a sentence in finite-domain first-order logic. In this paper, we argue that the capabilities of FOMC algorithms to date are limited by their inability to express many types of recursive computations. To enable such computations, we relax the restrictions that typically accompany domain recursion and generalise the circuits used to express a solution to an FOMC problem to directed graphs that may contain cycles. To this end, we adapt the most well-established (weighted) FOMC algorithm ForcLift to work with such graphs and introduce new compilation rules that can create cycle-inducing edges that encode recursive function calls. These improvements allow the algorithm to find efficient solutions to counting problems that were previously beyond its reach, including those that cannot be solved efficiently by any other exact FOMC algorithm. We end with a few conjectures on what classes of instances could be domain-liftable as a result.