Bridging Weighted First Order Model Counting and Graph Polynomials

要約

重み付き 1 次モデル計数問題 (WFOMC) は、指定されたドメインにわたる指定された 1 次論理文のモデルの重み付き合計を計算するように求めます。
これは、$C^2$ として知られる、計数量指定子を含む 2 変数フラグメントからの文のドメイン サイズの時間多項式で解くことができます。
この多項式時間の複雑さは、次の公理のいずれかによって $C^2$ を拡張する場合にも保持されます: 線形順序公理、ツリー公理、フォレスト公理、有向非巡回グラフ公理、または接続公理。
この方法で他のどの公理を一次文に追加できるかについては、興味深い疑問が残ります。
WFOMC をグラフ多項式と関連付けることにより、この問題に対する新しい視点を提供します。
WFOMC を使用して、一次論理文の弱連結多項式と強連結多項式を定義します。
これらの多項式には次の興味深い特性があることがわかります。
まず、$C^2$ からの文の領域サイズで多項式時間で計算できます。
第二に、それらを使用して、扱いやすいことが知られている既存の公理をすべて使用するだけでなく、二部性、強い連結性、スパニング部分グラフであること、$k$ の接続成分を持つことなどの新しい公理を使用して WFOMC を解くことができます。
-既知のトゥッテ多項式は弱い連結多項式の特別なケースとして復元でき、厳密および非厳密な有向色多項式は強い連結多項式から復元できます。これにより、これらの重要なグラフ多項式が次のように計算できることを示すことができます。
固定の $C^2$ 文と任意の数の基底単項リテラルの結合によってエンコードできるグラフの頂点数の時間多項式。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google