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.

翻译：我们研究了在具有两个变量和计数量词的逻辑语言上，加权一阶模型计数（WFOMC）的时间复杂性。已知该问题可在域大小的时间多项式内求解。然而，该多项式的次数——在实际应用中往往相对较高——此前从未被恰当探讨过。首先，我们为使用计数量词求解WFOMC的现有技术，建立了一个时间复杂性上界。已知该上界是一个多项式，其次数取决于输入公式的单元格数量。我们观察到，单元格数量又指数级地依赖于公式中出现的计数量词参数。其次，我们提出了一种处理计数量词的新方法，将指数依赖关系降至二次依赖关系，从而获得了更紧的上界。多项式次数对计数量词的依赖能否进一步降低，目前仍是一个未解决问题，这使得我们的新界成为一个有待超越的界。