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$ 中的语句，它们可在域大小的多项式时间内计算；其次，我们可以利用它们求解 WFOMC，涵盖所有已知可处理的现有公理以及新公理，如二分性、强连通性、具有 $k$ 个连通分量等；第三，著名的 Tutte 多项式可作为弱连通多项式的特例恢复，而严格与非严格有向着色多项式可从强连通多项式中恢复。