Bridging Weighted First Order Model Counting and Graph Polynomials

TL;DR

This work reframes WFOMC in the two-variable (C^2) fragment by introducing graph-polynomial tools that encode how models decompose under added axioms. The Weak Connectedness Polynomial and Strong Connectedness Polynomials allow polynomial-time computation for C^2 with cardinality constraints and enable domain-liftability across a broad set of axioms, including new ones like bipartiteness and strong connectivity. The framework also recovers classical graph polynomials, notably the Tutte polynomial and directed chromatic polynomials, by evaluating the polynomials on graph encodings, thereby linking lifted inference with enumerative combinatorics. Overall, the paper offers a unified, constructive method to ascertain the tractability of WFOMC with axioms and to compute important graph polynomials in new, structured settings.

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 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.

Figures (2)

• Figure 1: The 1-type structure of $\Psi_{R,u}$. Each tiny gray box represents an original 1-type of $\Psi$. The bold gray cells (each containing $4 \times 4$ boxes) refer to the replica of the original 1-types in each layer. The DP algorithm proceeds from left (cells $0, \cdots, 3$) to right (cell $4$).
• Figure 2: The 1-type structure of $\Psi_{R,u,v}$ which is a $(v+1) \times (u+1)$ grid. Each tiny gray box represents an original 1-type of $\Psi$. The bold gray cells (each containing $4 \times 4$ boxes) refer to the replicas of the original 1-types. The DP algorithm proceeds first along the vertical direction (from cell $(4,0)$ to cell $(4,4)$) and then along the horizontal direction (from columns $0, \cdots, 3$ to column $4$).

Theorems & Definitions (64)

• Theorem 1.1
• Theorem 1.2
• Example 2.1
• Definition 2.2: Weighted First Order Model Counting
• Example 2.3
• Definition 2.4: Weighted Model Counting
• Example 2.5
• Definition 2.6: Domain-liftability WFOMC-UFO2
• Definition 2.7: 1-type
• Definition 2.8: Counting quantifiers