Bridging Weighted First Order Model Counting and Graph Polynomials

Fuente: arXiv
Saved in:
Bibliographic Details
Main Authors: Kuang, Qipeng, Kuželka, Ondřej, Wang, Yuanhong, Wang, Yuyi
Format: Preprint
Published: 2024
Subjects:
Online Access:
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866914183320174592
author Kuang, Qipeng
Kuželka, Ondřej
Wang, Yuanhong
Wang, Yuyi
author_facet Kuang, Qipeng
Kuželka, Ondřej
Wang, Yuanhong
Wang, Yuyi
contents 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.
format Preprint
id arxiv_https___arxiv_org_abs_2407_11877
institution arXiv
publishDate 2024
record_format arxiv
spellingShingle Bridging Weighted First Order Model Counting and Graph Polynomials
Kuang, Qipeng
Kuželka, Ondřej
Wang, Yuanhong
Wang, Yuyi
Logic in Computer Science
Artificial Intelligence
03C13, 68T27, 05A15 (Primary)
F.4.0
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.
title Bridging Weighted First Order Model Counting and Graph Polynomials
topic Logic in Computer Science
Artificial Intelligence
03C13, 68T27, 05A15 (Primary)
F.4.0
url https://arxiv.org/abs/2407.11877