# Skolemization for Weighted First-Order Model Counting

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

## Key facts

- Cited by 15 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 19 Dec 2013.

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

- [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)
- [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)
- [On Exact Sampling in the Two-Variable Fragment of First-Order Logic](https://mlsanity.com/paper/2302.02730/) (2023)
- [Faster Lifting for Ordered Domains with Predecessor Relations](https://mlsanity.com/paper/2507.19182/) (2025)
- [Weighted First Order Model Counting with Directed Acyclic Graph Axioms](https://mlsanity.com/paper/2302.09830/) (2023)
- [Synthesising Recursive Functions for First-Order Model Counting: Challenges, Progress, and Conjectures](https://mlsanity.com/paper/2306.04189/) (2023)
- [Towards Practical First-Order Model Counting](https://mlsanity.com/paper/2502.12278/) (2025)
- [Polynomial-Time Relational Probabilistic Inference in Open Universes](https://mlsanity.com/paper/2505.04115/) (2025)
- [Weighted First Order Model Counting for Two-variable Logic with Axioms on Two Relations](https://mlsanity.com/paper/2508.11515/) (2025)
- [An epistemic approach to model uncertainty in data-graphs](https://mlsanity.com/paper/2109.14112/) (2021)
- [Tractable Weighted First-Order Model Counting with Bounded Treewidth Binary Evidence](https://mlsanity.com/paper/2511.09174/) (2025)
- [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 emerged recently as a novel reasoning task, at the core of efficient algorithms for probabilistic logics. We present a Skolemization algorithm for model counting problems that eliminates existential quantifiers from a first-order logic theory without changing its weighted model count. For certain subsets of first-order logic, lifted model counters were shown to run in time polynomial in the number of objects in the domain of discourse, where propositional model counters require exponential time. However, these guarantees apply only to Skolem normal form theories (i.e., no existential quantifiers) as the presence of existential quantifiers reduces lifted model counters to propositional ones. Since textbook Skolemization is not sound for model counting, these restrictions precluded efficient model counting for directed models, such as probabilistic logic programs, which rely on existential quantification. Our Skolemization procedure extends the applicability of first-order model counters to these representations. Moreover, it simplifies the design of lifted model counting algorithms.