Authors: Qipeng Kuang, Ondřej Kuželka, Yuanhong Wang, Yuyi Wang
Abstract: 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 also 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, being a spanning subgraph, 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, which allows us to show that these important graph polynomials can
be computed in time polynomial in the number of vertices for any graph that can
be encoded by a fixed $C^2$ sentence and a conjunction of an arbitrary number
of ground unary literals.
Source: http://arxiv.org/abs/2407.11877v1
