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 computational complexity of weighted first-order model counting in the two-variable fragment with counting quantifiers, proposing a new approach that reduces the exponential dependency to quadratic, thus tightening the upper bound.

Contribution

The paper introduces a novel method that significantly reduces the complexity bound for WFOMC with counting quantifiers, improving from exponential to quadratic dependency.

Findings

Existing techniques have polynomial time complexity with high degree.

The new approach reduces exponential dependency to quadratic.

Open question remains on further reducing the polynomial degree.

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.