Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Complexity of Weighted First-Order Model Counting in the Two-Variable Fragment with Counting Quantifiers: A Bound to Beat

Jan Tóth, Ondřej Kuželka

TL;DR

This paper analyzes the time complexity of weighted first-order model counting (WFOMC) in the two-variable fragment with counting quantifiers (C^2). It first reviews existing domain-liftable bounds, showing that the polynomial degree depends exponentially on counting-quantifier parameters. The authors then introduce a novel encoding based on canonical models that reduces the counting-parameter growth from exponential to quadratic, yielding a substantial, super-exponential speedup in practice. They prove an improved upper bound and validate it with extensive experiments on k-regular graphs, colored and directed variants, and Markov Logic Networks, demonstrating notable performance gains over prior encodings. The work opens the path toward even tighter bounds and broader applicability of lifted WFOMC in counting-heavy logical settings.

Abstract

We study the time complexity of the weighted first-order model counting (WFOMC) over the logical language with two variables and counting quantifiers. The problem is known to be solvable in time polynomial in the domain size. However, the degree of the polynomial, which turns out to be relatively high for most practical applications, has never been properly addressed. First, we formulate a time complexity bound for the existing techniques for solving WFOMC with counting quantifiers. The bound is already known to be a polynomial with its degree depending on the number of cells of the input formula. We observe that the number of cells depends, in turn, exponentially on the parameter of the counting quantifiers appearing in the formula. Second, we propose a new approach to dealing with counting quantifiers, reducing the exponential dependency to a quadratic one, therefore obtaining a tighter upper bound. It remains an open question whether the dependency of the polynomial degree on the counting quantifiers can be reduced further, thus making our new bound a bound to beat.

Complexity of Weighted First-Order Model Counting in the Two-Variable Fragment with Counting Quantifiers: A Bound to Beat

TL;DR

This paper analyzes the time complexity of weighted first-order model counting (WFOMC) in the two-variable fragment with counting quantifiers (C^2). It first reviews existing domain-liftable bounds, showing that the polynomial degree depends exponentially on counting-quantifier parameters. The authors then introduce a novel encoding based on canonical models that reduces the counting-parameter growth from exponential to quadratic, yielding a substantial, super-exponential speedup in practice. They prove an improved upper bound and validate it with extensive experiments on k-regular graphs, colored and directed variants, and Markov Logic Networks, demonstrating notable performance gains over prior encodings. The work opens the path toward even tighter bounds and broader applicability of lifted WFOMC in counting-heavy logical settings.

Abstract

We study the time complexity of the weighted first-order model counting (WFOMC) over the logical language with two variables and counting quantifiers. The problem is known to be solvable in time polynomial in the domain size. However, the degree of the polynomial, which turns out to be relatively high for most practical applications, has never been properly addressed. First, we formulate a time complexity bound for the existing techniques for solving WFOMC with counting quantifiers. The bound is already known to be a polynomial with its degree depending on the number of cells of the input formula. We observe that the number of cells depends, in turn, exponentially on the parameter of the counting quantifiers appearing in the formula. Second, we propose a new approach to dealing with counting quantifiers, reducing the exponential dependency to a quadratic one, therefore obtaining a tighter upper bound. It remains an open question whether the dependency of the polynomial degree on the counting quantifiers can be reduced further, thus making our new bound a bound to beat.
Paper Structure (25 sections, 12 theorems, 64 equations, 5 figures, 3 tables, 1 algorithm)

This paper contains 25 sections, 12 theorems, 64 equations, 5 figures, 3 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Background
  3. First-Order Logic
  4. FOL Fragments
  5. Weighted First-Order Model Counting
  6. Solving WFOMC with Counting Quantifiers
  7. An Upper Bound for Existing Techniques
  8. A Worked Example on Removing Counting
  9. Deriving the Upper Bound
  10. Improving the Upper Bound
  11. Canonical Models
  12. The New Encoding
  13. The Improved Upper Bound
  14. Experiments
  15. Performance Measurements
  16. ...and 10 more sections

Key Result

Theorem 1

Let $\Gamma$ be an $\textup{$\textbf{FO}^2${}}$ sentence with $p$ valid cells. Let $\Upsilon=\bigwedge_{i=1}^m\left(|R_i|=k_i\right)$ be $m$ cardinality constraints, where $R_1, R_2, \ldots, R_m$ are some predicates from the language of $\Gamma$ and each $k_i\in\mathds{N}$. For any $n\in\mathds{N}$

Figures (5)

  • Figure 1: Runtime for counting $k$-regular graphs
  • Figure 2: Runtime for counting $k$-regular $l$-colored graphs
  • Figure 3: Runtime for counting $k$-regular digraphs
  • Figure 4: Runtimes of tasks performed on BA(3)
  • Figure 5: Probability of $m$ smokers

Theorems & Definitions (23)

  • Definition 1
  • Definition 2
  • Definition 3
  • Example 1
  • Theorem 1
  • Lemma 1
  • Lemma 2
  • Lemma 3
  • Lemma 4
  • Lemma 5
  • ...and 13 more