The Weighted First-Order Model Counting Problem (WFOMC) asks to compute the weighted sum of models of a given first-order logic sentence over a given domain. It can be solved in time polynomial in the domain size for sentences from the two-variable fragment with counting quantifiers, known as $C^2$. This polynomial-time complexity is known to be retained when extending $C^2$ by one of the following axioms: linear order axiom, tree axiom, forest axiom, directed acyclic graph axiom or connectedness axiom. An interesting question remains as to which other axioms can be added to the first-order sentences in this way. We provide a new perspective on this problem by associating WFOMC with graph polynomials. Using WFOMC, we define Weak Connectedness Polynomial and Strong Connectedness Polynomials for first-order logic sentences. It turns out that these polynomials have the following interesting properties. First, they can be computed in polynomial time in the domain size for sentences from $C^2$. Second, we can use them to solve WFOMC with all of the existing axioms known to be tractable as well as with new ones such as bipartiteness, strong connectedness, having $k$ connected components, etc. Third, the well-known Tutte polynomial can be recovered as a special case of the Weak Connectedness Polynomial, and the Strict and Non-Strict Directed Chromatic Polynomials can be recovered from the Strong Connectedness Polynomials.

翻译：加权一阶模型计数问题（WFOMC）要求计算给定一阶逻辑语句在给定论域上的模型的加权和。对于带计数量词的双变量片段（称为$C^2$）中的语句，该问题可在论域大小的多项式时间内求解。已知当$C^2$扩展以下任一公理时，此多项式时间复杂度仍可保持：线性序公理、树公理、森林公理、有向无环图公理或连通性公理。一个有趣的问题是，是否还能以类似方式向一阶语句添加其他公理。本文通过将WFOMC与图多项式相关联，为该问题提供了新的视角。利用WFOMC，我们为一阶逻辑语句定义了弱连通多项式和强连通多项式。结果表明，这些多项式具有以下重要性质：首先，对于$C^2$中的语句，它们可在论域大小的多项式时间内计算；其次，可利用它们求解包含所有已知易处理公理（如二分性、强连通性、具有$k$个连通分量等新公理）的WFOMC问题；第三，著名的Tutte多项式可作为弱连通多项式的特例恢复，而严格与非严格有向着色多项式可从强连通多项式中恢复。