Bridging Weighted First Order Model Counting and Graph Polynomials

TL;DR

This paper introduces a novel approach linking weighted first-order model counting with graph polynomials, enabling polynomial-time computation and extending tractability to new axioms like bipartiteness and connectivity.

Contribution

It defines new graph polynomials for WFOMC, demonstrating their computational properties and unifying various graph invariants within a logical framework.

Findings

Polynomials can be computed in polynomial time for $C^2$ sentences.

These polynomials generalize known graph invariants like Tutte polynomial.

New tractable axioms such as bipartiteness and connectivity are incorporated.

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.