Bridging Weighted First Order Model Counting and Graph Polynomials

Kuang, Qipeng; Kuželka, Ondřej; Wang, Yuanhong; Wang, Yuyi

doi:10.4230/LIPIcs.CSL.2026.7

Bridging Weighted First Order Model Counting and Graph Polynomials

Qipeng Kuang

The University of Hong Kong, China Ondřej Kuželka

Czech Technical University in Prague, Czech Republic Yuanhong Wang

Jilin University, Changchun City, China Yuyi Wang

CRRC Zhuzhou Institute, China

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 $\text{C}^{2}$ . This polynomial-time complexity is known to be retained when extending $\text{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 $\text{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.

Keywords and phrases:

Weighted First-Order Model Counting, Axiom, Enumerative Combinatorics, Tutte Polynomial

Funding:

Ondřej Kuželka: Czech Science Foundation project 24-11820S (“Automatic Combinatorialist”).

Yuanhong Wang: National Natural Science Foundation of China (No. 62506141).

Yuyi Wang: partially supported by the Natural Science Foundation of Hunan Province, China (Grant No. 2024JJ5128).

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Finite Model Theory

Related Version:

Full Version: https://arxiv.org/abs/2407.11877

Supplementary Material:

Software (Source Code): https://github.com/l2l7l9p/Polynomials-for-WFOMC [12]
archived at

swh:1:dir:e82fa8e26998cfb9e25e723b2c1182f17a82276e

DOI:

10.4230/LIPIcs.CSL.2026.7

Event:

34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Editors:

Stefano Guerrini and Barbara König

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

Given a function-free first-order logic sentence $\Psi$ and $n\in\mathbb{N}$ , the first-order model counting (FOMC) problem asks to compute the number of models of $\Psi$ over the domain $\{1,\dots,n\}$ . FOMC can be used, among others, to solve various combinatorics problems on labeled structures. For instance, the FOMC of the sentence $\Psi=\forall x\exists y(E(x,y)\lor E(y,x))\land\forall x\lnot E(x,x)$ corresponds to the number of $n$ -vertex directed graphs with no isolated vertices and no loops. Similarly, the FOMC of $\Phi=\forall x\lnot E(x,x)\land\forall x\forall y\left(E(x,y)\to E(y,x)\right)% \land\forall x\exists_{=k}yE(x,y)$ equals the number of $k$ -regular graphs on $n$ vertices where $\exists_{=k}y$ is a counting quantifier restricting the number of $y$ satisfying $E(x,y)=\top$ to be exactly $k$ for each $x$ .

The weighted variant of the FOMC problem, known as the weighted first-order model counting (WFOMC) problem, additionally expects a specification of positive and negative weights for predicates in the language, which are then used to assign weights to models. In WFOMC, the task is to compute the sum of the weights of the given sentence’s models.¹¹1Surprisingly, WFOMC is also essential for the unweighted FOMC problem since, for example, Skolemization for FOMC [31], which is used to eliminate existential quantifiers, relies on the usage of (negative) weights. WFOMC has applications in Statistical Relational Learning (SRL) [5]. For instance, Markov Logic Networks (MLNs) [21], one of the most popular SRL formalisms, model relational data by a distribution over possible worlds, where the computation of the partition function (used in probabilistic inference in MLN) is reducible to WFOMC [29].

A key issue regarding WFOMC is its computational complexity. Generally, there is no hope of devising algorithms for WFOMC that would scale polynomially with the size of the first-order logic sentences under reasonable assumptions [2]. This is true even for very simple fragments such as the one-variable fragment $\text{FO}^{1}$ , which contains sentences with at most one logical variable. Therefore, most of the focus in this area has been on identifying fragments of first-order logic for which WFOMC can be computed in time polynomial in the size of the domain (but not necessarily in the size of the sentence). The term coined for this kind of tractability by [29] is domain liftability – it is an analog to data complexity [32] from database theory.

The first positive results regarding the tractability of WFOMC came from the two seminal papers [29, 31], which together established domain liftability of the two-variable fragment of first-order logic $\text{FO}^{2}$ . This was quickly complemented by a hardness result [2], showing that WFOMC for the three-variable fragment $\text{FO}^{3}$ is not domain-liftable (under plausible complexity-theoretic assumptions). However, this does not mean that the frontiers of tractability cannot be pushed beyond $\text{FO}^{2}$ . For instance, the two-variable fragment with counting quantifiers $\text{C}^{2}$ [8] (e.g., the above sentence of a $k$ -regular graph) with cardinality constraints (i.e., the restrictions to the number of true ground atoms for relations), which is strictly more expressive than $\text{FO}^{2}$ , was shown to be domain-liftable in [14]. Other works [30, 33, 34] proved domain-liftability when attaching ground unary literals (as part of the input along with the domain size) to sentences from these fragments.

One strategy for discovering new tractable fragments is to add extra axioms to a fragment known to be tractable, which may or may not be finitely expressible in first-order logic. This approach was first explored in [13] where it was shown that adding a single functionality axiom to $\text{FO}^{2}$ results in a domain-liftable fragment.²²2This fragment is contained in $\text{C}^{2}$ , which can encode an arbitrary number of functionality constraints. Subsequent works extended domain liftability to the fragments $\text{C}^{2}$ + Tree [28] and $\text{C}^{2}$ + LinearOrder [24], which are obtained by adding to $\text{C}^{2}$ an axiom specifying that a distinguished relation $R$ should correspond to an undirected tree or to a linear order, respectively. Recently, the work [17] added several new tractable classes: $\text{C}^{2}$ + DAG, $\text{C}^{2}$ + Connected, and $\text{C}^{2}$ + Forest, which allow restricting a distinguished binary relation to be a directed acyclic graph or to be a connected undirected graph or to be a forest. Except for the linear-order and the functionality axiom, these axioms are not finitely expressible in first-order logic.

To add the axioms discussed above to $\text{C}^{2}$ while preserving domain-liftability, existing works usually rely on directly translating specialized techniques from enumerative combinatorics. For instance, Kirchhoff’s matrix-tree theorem was used for the tree axiom in [28]. Similarly, ideas used in existing combinatorial proofs for counting connected graphs and acyclic graphs on $n$ -vertices were adapted to the WFOMC setting in [17] to implement the connectedness and acyclicity axioms. This raises a natural question:

Can we define a general framework for adding axioms to $\text{C}^{2}$ that allows us to prove domain-liftability of new axioms and to efficiently compute the WFOMC of sentences with these axioms?

1.1 Our Contribution

In this paper, we take a route inspired by graph polynomials such as the Tutte polynomial [25] and directed chromatic polynomials [22]. Graph polynomials are algebraic expressions that encode various combinatorial properties of graphs, allowing us to capture information such as connectivity, colorability, and spanning substructures. In this work, we consider $\text{C}^{2}$ possibly extended by cardinality constraints and ground unary literals (which we will call $\text{C}^{2}$ with cardinality constraints for simplicity). We introduce similar polynomials for first-order logic sentences, capturing certain combinatorial properties of their models, and show that they can be computed efficiently for $\text{C}^{2}$ with cardinality constraints, which requires the introduction of new algorithmic techniques for computation of WFOMC. Using the new polynomials for WFOMC, we can tackle the problem of efficiently computing WFOMC of $\text{C}^{2}$ sentences with cardinality constraints and one of a number of non-trivial axioms, special constraints on the graph interpreting a distinguished binary relation $R$ (denoted by $G(R)$ ). The main axioms for which we prove domain-liftability are listed in Table 1, involving several new axioms as well as all of the old ones.

Table 1: Axioms that we proved the domain-liftability of. Note that the first 4 axioms require the distinguished relations to be symmetric and irreflexive.

Axiom	Description	Lifted by	First lifted by
$connected_{k}(R)$	$G(R)$ has $k$ connected components	Theorem 15	new ( $connected_{1}(R)$ by [17])
$bipartite(R)$	$G(R)$ is a bipartite graph	Theorem 16	new
$tree(R)$	$G(R)$ is a tree	Theorem 19	[28]
$\mathit{forest}(R)$	$G(R)$ is a forest	Theorem 20	[17]
$SC(R)$	$G(R)$ is strongly connected	Theorem 31	new
$AC(R)$	$G(R)$ is acyclic	Theorem 33	[17]
$DT(R,Root)$	$G(R)$ is a directed tree such that the root interprets the unary predicate $R o o t$ as true	Theorem 34	[28]
$DF(R)$	$G(R)$ is a directed graph such that each weakly connected component is a directed tree	Theorem 34	[17]
$LO(R)$	$G(R)$ represents a linear order	Theorem 35	[24]

Theorem 1.

The fragment of $\text{C}^{2}$ with cardinality constraints and any single axiom in Table 1 is domain-liftable.

Moreover, we can show domain-liftability of combinations of axioms. Table 2 offers a comprehensive list of axioms obtained by combining the existing axioms, all of which are new axioms that have not been shown to be domain-liftable before.³³3This would be difficult to achieve using existing techniques based on individual treatment of each axiom, as done in the literature.

Table 2: New axioms by combining existing axioms. Note that the first 2 axioms require the distinguished relations to be symmetric and irreflexive.

Axiom	Description	Combined axioms
$bipartite_{k}(R)$	$G(R)$ is a bipartite graph with $k$ connected components	$connected_{k}\land bipartite$
$forest_{k}(R)$	$G(R)$ is a forest with $k$ trees	$connected_{k}\land forest$
$AC_{k}(R)$	$G(R)$ is a DAG with $k$ weakly connected components	$connected_{k}\land AC$
$BiAC(R)$	$G(R)$ is a DAG such that the underlying undirected graph is bipartite	$bipartite\land AC$
$polytree(R)$	$G(R)$ is a polytree, i.e., a DAG whose underlying undirected graph is a tree	$tree\land AC$
$polyforest(R)$	$G(R)$ is a polyforest, i.e., a DAG whose underlying undirected graph is a forest	$forest\land AC$

Theorem 2.

The fragment of $\text{C}^{2}$ with cardinality constraints and any single axiom in Table 2 is domain-liftable.

Besides using the idea of graph polynomials to solve several counting tasks efficiently, conversely, the polynomials for WFOMC bring new results on graph polynomials. We show that the Tutte polynomial [25], the strict and non-strict directed chromatic polynomials [22] can be recovered from our polynomials for WFOMC. This allows us to show that these graph polynomials can be computed in time polynomial in the number of vertices for any graph that can be encoded by a set of ground unary literals, cardinality constraints and a fixed $\text{C}^{2}$ sentence (the parameters of cardinality constraints and the number of ground unary literals are allowed to depend on the number of vertices). This result answers in the positive way the question in [28] whether calculating the Tutte polynomial of a block-structured graph (see its definition in Example 8) can be done in time polynomial in the number of vertices.

1.2 Related Work

We build on several lines of research. First, we build on the stream of results from lifted inference literature which established domain-liftability of several natural fragments of first-order logic [18, 3, 29, 6, 31, 2, 10, 14]. These works started with the seminal results showing domain-liftability of $\text{FO}^{2}$ [29, 31] and continued by showing domain-liftability of larger fragments such as S²FO² and S²RU [10], U₁ [13] or $\text{C}^{2}$ [14]. Second, we build on extensions of these works that added axioms not expressible in these fragments or even in first-order logic such as the tree axiom [28], forest axiom [17], linear order axiom [24], acyclicity axiom [17] and connectedness axiom [17]. In this work, we generalize all of these results and add new axioms to this list, showing their domain-liftability. Finally, our work builds on tools from enumerative combinatorics [23] and on graph polynomials [26]. The most well-known among graph polynomials is the Tutte polynomial [25] but there exist also extensions of it [1], with which we do not work directly in this paper. Computing the Tutte polynomial is known to be intractable in general [9], however, in this work we show that it can be computed in polynomial time for graphs that can be encoded by a fixed sentence from the first-order fragment $\text{C}^{2}$ , possibly with cardinality constraints and ground unary literals, both of which may depend on the number of vertices of the graph (unlike the $\text{C}^{2}$ sentence which needs to stay fixed).

2 Preliminaries

We introduce our notations and main technical concepts, and provide a brief overview of existing algorithms in this section. A brief introduction to graph polynomials is in Appendix B.

Throughout this paper, we denote the set of natural numbers from 1 to $n$ as $[n]$ . For a polynomial $f(x)$ , the notation $[x^{i}]f$ represents the coefficient of the monomial $x^{i}$ .

All vectors used in this paper are non-negative integer vectors. For a vector $\bm{c}$ of length $L$ , $|\bm{c}|$ denotes the sum of its elements, i.e., $\sum_{i=1}^{L}c_{i}$ . When considering two vectors $\bm{a}$ and $\bm{b}$ of the same length $L$ , the operation $\bm{a}+\bm{b}$ denotes the vector $(a_{1}+b_{1},a_{2}+b_{2},\cdots,a_{L}+b_{L})$ , and the subtraction is defined similarly. For a vector $\bm{a}$ and a non-negative integer $n$ , $\binom{n}{\bm{a}}$ refers to $\binom{n}{a_{1}}\binom{n-a_{1}}{a_{2}}\cdots\binom{n-a_{1}-\cdots-a_{L-1}}{a_{% L}}=\frac{n!}{a_{1}!a_{2}!\cdots a_{L}!}$ .

2.1 First-Order Logic

We consider the function-free (we allow constants but not any functions with arity greater than zero), finite domain fragment of first-order logic. An atom of arity $k$ takes the form $P(x_{1},\cdots,x_{k})$ where $P/k$ is from a vocabulary of predicates (also called relations), and $x_{1},\cdots,x_{k}$ are logical variables from a vocabulary of variables or constants from a vocabulary of constants.⁴⁴4We restrict $k\geq 1$ for simplicity but $k\geq 0$ is tractable for this work as well. A literal is an atom or its negation. A formula is a literal or formed by connecting one or more formulas together using negation, conjunction, or disjunction. A formula may be optionally surrounded by one or more quantifiers of the form $\forall x$ or $\exists x$ , where $x$ is a logical variable. A logical variable in a formula is said to be free if it is not bound by any quantifier. A formula with no free variables is called a sentence.

A first-order logic formula in which all variables are substituted by constants in the domain is called ground. A possible world $\omega$ interprets each predicate in a sentence over a finite domain, represented by a set of ground literals. Sometimes we only care about the interpretation of a single predicate $R$ in a possible world $\omega$ , which is denoted by $\omega_{R}$ . The satisfaction relation $\models$ is defined in the usual way: $\omega\models\alpha$ means that the formula $\alpha$ is true in $\omega$ . The possible world $\omega$ is a model of a sentence $\Psi$ if $\omega\models\Psi$ . We denote the set of all models of a sentence $\Psi$ over the domain $\{1,2,\dots,n\}$ by $\mathcal{M}_{\Psi,n}$ .

2.2 Weighted First Order Model Counting

The weighted first-order model counting problem (WFOMC) takes the input consisting of a first-order sentence $\Psi$ , a domain size $n\in\mathbb{N}$ , and a pair of weighting functions $(w,\overline{w})$ that both map all predicates in $\Psi$ to real weights. Given a set $\mathcal{L}$ of ground literals whose predicates are in $\Psi$ , the weight of $\mathcal{L}$ is defined as $W(\mathcal{L},w,\overline{w}):=\prod_{l\in\mathcal{L}_{T}}w(\mathsf{pred}\left% (l\right))\cdot\prod_{l\in\mathcal{L}_{F}}\overline{w}(\mathsf{pred}\left(l% \right)),$ where $\mathcal{L}_{T}$ (resp. $\mathcal{L}_{F}$ ) denotes the set of positive (resp. negative) ground literals in $\mathcal{L}$ , and $\mathsf{pred}\left(l\right)$ maps a literal $l$ to its corresponding predicate name.

Definition 3 (Weighted First Order Model Counting).

The WFOMC of a first-order sentence $\Psi$ over a finite domain of size $n$ under weighting functions $(w,\overline{w})$ is

\mathsf{WFOMC}(\Psi,n,w,\overline{w}):=\sum_{\mu\in\mathcal{M}_{\Psi,n}}W(\mu,% w,\overline{w}).

Since these weightings are defined on the predicate level, all positive ground literals of the same predicate get the same weights, and so do all negative ground literals of the same predicate. For this reason, the notion of WFOMC defined here is also referred to as symmetric WFOMC [2].

Example 4.

Consider $\Psi=\forall x\exists y\ R(x,y)$ , and let $w(R)=1,\overline{w}(R)=1$ . Then $\mathsf{WFOMC}(\Psi,n,\linebreak w,\overline{w})=(2^{n}-1)^{n}$ because for each domain element $i\in[n]$ , there are $2^{n}-1$ ways to choose the truth assignment of $R(i,1),R(i,2),\dots,R(i,n)$ that make $\exists y\ R(i,y)$ satisfied, and there are $n$ domain elements.

2.3 Data Complexity of WFOMC

We consider the data complexity of WFOMC: the complexity of computing $\mathsf{WFOMC}(\Psi,n,w,\overline{w})$ when fixing the input sentence $\Psi$ and weighting $(w,\overline{w})$ , and treating the domain size $n$ as an input encoded in unary.

Definition 5 (Domain-liftability [29]).

A sentence, or class of sentences, that enjoys polynomial-time data complexity, i.e., the complexity is polynomial in the domain size, is said to be domain-liftable.

Building on [29, 31], in [2, Appendix C], it was shown that any sentence with at most two logical variables ( $\text{FO}^{2}$ ) is domain-liftable by devising a polynomial-time algorithm for computing $\mathsf{WFOMC}(\Psi,n,w,\overline{w})$ for any $\text{FO}^{2}$ sentence $\Psi$ and any weighting $(w,\overline{w})$ . The description of this algorithm is in Appendix A. This result also serves as the basis of a WFOMC algorithm for $\text{C}^{2}$ (the $\text{FO}^{2}$ sentence with counting quantifiers) together with cardinality constraints and ground unary literals.

Definition 6 (Counting quantifiers).

The counting quantifier $\exists_{=k}$ restricts that the number of assignments of the quantified variable satisfying the subsequent formula is exactly $k$ . Counting quantifiers $\exists_{\leq k}$ and $\exists_{\geq k}$ are defined similarly.

Counting quantifiers allow us to express concepts such as “each vertex in the undirected graph has exactly $k$ edges”, i.e., $k$ -regular graphs, by the sentence $\forall x\lnot E(x,x)\land\forall x\forall y\left(E(x,y)\to E(y,x)\right)\land% \forall x\exists_{=k}yE(x,y)$ .

Definition 7 (Cardinality constraints).

The cardinality constraint is an expression of the form of $|P|\bowtie k$ , where $P$ is a predicate and $\bowtie$ is a comparison operator $\{<,\leq,=,\geq,>\}$ . These constraints are imposed on the number of distinct positive ground literals of $P$ in a model.

For example, $|Eq|=n$ means that there are exactly $n$ positive ground literals of $E q$ in a model, and the sentence $(\forall x\ Eq(x,x))\land|Eq|=n$ along with a domain of size $n$ encodes an identity relation $E q$ . Note that we allow $k$ in Definition 7 to depend on the domain size (such as in the definition of $E q$ here where we used $|Eq|=n$ ).

Finally, we show the usage of ground unary literals defined in Section 2.1. For example, the sentence $\forall x\exists y(R(x,y)\to S(y))\land S(1)\land\lnot S(2)$ contains ground unary literals $S(1)\land\lnot S(2)$ indicating that any interpretation of this sentence should satisfy that $S(1)$ is true and $S(2)$ is false. Another example is encoding a block-structured graph.

Example 8.

A block-structured graph is an undirected graph $G=(V,E)$ where vertices are partitioned into a constant number of blocks, and for every two blocks $V_{i},V_{j}$ , either $\forall x\in V_{i}\forall y\in V_{j},(x,y)\in E$ or $\forall x\in V_{i}\forall y\in V_{j},(x,y)\not\in E$ . We can encode a block-structured graph in the following way: we introduce a fresh unary predicate $Block_{i}$ for each block $V_{i}$ , and let

$\displaystyle\Psi_{B}=$	$\displaystyle\bigwedge_{V_{i},V_{j}\text{ are connected}}\forall x\forall y(% Block_{i}(x)\land Block_{j}(y)\to E(x,y))$	(1)
	$\displaystyle\land\bigwedge_{V_{i},V_{j}\text{ are not connected}}\forall x% \forall y(Block_{i}(x)\land Block_{j}(y)\to\lnot E(x,y))$
	$\displaystyle\land\bigwedge_{e\in V}\left(Block_{v(e)}(e)\land\bigwedge_{j\neq v% (e)}\lnot Block_{j}(e)\right),$

where $v(e)$ indicates the block that vertex $e$ belongs to, and $Block_{*}(e)$ and $\lnot Block_{*}(e)$ are ground unary literals for vertex $e$ indicating whether $e$ is in the specified block or not.

$\blacktriangleright$ Remark 9.

We need to define the data complexity more carefully when the input sentence of WFOMC involves cardinality constraints and ground unary literals. In such instances, the $\text{C}^{2}$ sentence (including the parameters in counting quantifiers) in the input remains fixed, while cardinality constraints and ground unary literals are considered variable inputs encoded in binary.

The presence of counting quantifiers, cardinality constraints, and ground unary literals does not affect the domain-liftability of $\text{FO}^{2}$ . Using the techniques in [14] and [34, Appendix A], WFOMC of $\text{C}^{2}$ with cardinality constraints and ground unary literals can be reduced to WFOMC of $\text{FO}^{2}$ with symbolic weights⁵⁵5The weighting functions $w,\overline{w}$ map predicates to symbolic variables. For more details, see [14, Section $3.1$ ]., and then solved by the algorithm for $\text{FO}^{2}$ in a straightforward manner.

$\blacktriangleright$ Remark 10.

The techniques mentioned above apply to the methods in this paper. Therefore, in the rest of this paper we only present the algorithms for $\text{FO}^{2}$ and state the results in terms of $\text{C}^{2}$ with cardinality constraints for simplicity.

2.4 Axioms

While $\text{C}^{2}$ captures numerous graph structures, it falls short in expressing certain important graph properties, such as being a tree, a forest, and strongly connected. In fact, these structures cannot be finitely axiomatized by first-order logic [16].

Given a binary predicate $R$ , an interpretation for $R$ can be regarded as a directed graph where the domain is the vertex set and $R$ is the edge set, which we call $G(R)$ . If a possible world $\omega$ is specified, the interpretation of $R$ in $\omega$ is a specific graph, denoted by $G(\omega_{R})$ .

An axiom is a special constraint on the interpretation of a binary predicate $R$ that $G(R)$ should be a certain combinatorial structure. We often write an axiom as $axiom(R)$ where $a x i o m$ is an identifier of the axiom. For example, in what follows, we will discuss the tree axiom $tree(R)$ , which requires $G(R)$ to be a tree, and the forest axiom $forest(R)$ , which requires $G(R)$ to be a forest. For better illustration, we treat axioms as atomic formulas in a sentence, and use $\Psi\land axiom(R)$ to denote the sentence $\Psi$ with the axiom $axiom(R)$ conjoined. For instance, $tree(E)\land\forall x\left(Leaf(x)\leftrightarrow\exists_{=1}y\ E(x,y)\right)$ is a sentence that expresses the concept of trees with a leaf predicate $Leaf/1$ .

3 Weak Connectedness Polynomial

In this section, we introduce our first polynomial, called Weak Connectedness Polynomial (WCP). The WCP is a univariate polynomial defined on a first-order logic sentence and a distinguished binary relation. Similarly to graph polynomials, the WCP can also capture various combinatorial properties of the models of the sentence w.r.t. the binary relation. We show that WCP can be computed in polynomial time in the domain size for sentences from the fragment $\text{C}^{2}$ with cardinality constraints. This property allows us to attach axioms of non-trivial combinatorial structures to the first-order logic sentence as well as to derive the Tutte polynomial for certain graphs. All the omitted proofs can be found in Appendix C.

3.1 Definition

We define WCP as a univariate polynomial whose point evaluation at every positive integer $u$ is equal to a weighted first-order model count of a suitable first-order logic sentence parameterized by $u$ .

Definition 11 (Weak Connectedness Polynomial).

Let $\Psi$ be a first-order logic sentence possibly with cardinality constraints and ground unary literals, $w,\overline{w}$ be two weighting functions, and $R$ be a distinguished binary relation. The $n$ -th WCP $f_{n}(u)$ of $\Psi$ for the relation $R$ is the univariate polynomial which satisfies:

f_{n}(u;\Psi,w,\overline{w},R)=\mathsf{WFOMC}(\Psi_{R,u},n,w,\overline{w})

for all positive integers $u$ . Here, the sentence $\Psi_{R,u}$ is defined as:

	$\displaystyle\Psi_{R,u}=\Psi\wedge$	$\displaystyle\bigwedge_{i=1}^{u}\forall x\forall y\left(A_{i}(x)\wedge(R(x,y)% \vee R(y,x))\to A_{i}(y)\right)$		(2)
	$\displaystyle\wedge$	$\displaystyle\bigwedge_{i=2}^{u}\forall x\left(A_{i}(x)\to A_{i-1}(x)\right),$		(2)

where $A_{1},\cdots,A_{u}$ are fresh unary predicates and $w(A_{i})=\overline{w}(A_{i})=1$ .

Intuitively, by introducing $u$ new predicates $A_{1},\cdots,A_{u}$ , we make each weakly connected component in $G(R)$ contribute a factor of $u+1$ to $\mathsf{WFOMC}$ . In the rest of the paper, we use $cc(\mu_{R})$ to denote the number of weakly connected components in $G(\mu_{R})$ . The most important property of WCP is that it captures $cc(\mu_{R})$ , which is stated formally in the following proposition.

Proposition 12.

For the sentence $\Psi$ , the weighting functions $w$ and $\overline{w}$ and the binary relation $R$ , it holds that

f_{n}(u;\Psi,w,\overline{w},R)=\sum_{\mu\in\mathcal{M}_{\Psi,n}}W(\mu,w,% \overline{w})\cdot(u+1)^{cc(\mu_{R})}.

Proof.

By $\bigwedge_{i=2}^{u}\forall x\left(A_{i}(x)\to A_{i-1}(x)\right)$ , for each element $e$ in the domain there must be an $i^{\prime}\in[0,u]$ such that $A_{1}(e)=\cdots=A_{i^{\prime}}(e)=\top$ and $A_{i^{\prime}+1}(e)=\cdots=A_{u}(e)=\bot$ . Meanwhile, elements whose corresponding vertices form a weakly connected component in $G(\mu_{R})$ must have the same $i^{\prime}$ due to the first row of Equation (2).

Therefore, for any model $\mu$ of $\Psi$ , each weakly connected component in $G(\mu_{R})$ has $u+1$ choices of $i^{\prime}$ regardless of the interpretations of other predicates. That is, $\mu$ replicates $u+1$ times in $\Psi_{R,u}$ , and the weight of each of these replicas is $W(\mu,w,\overline{w})$ due to $w(A_{i})=\overline{w}(A_{i})=1$ . Therefore, the WFOMC of $\Psi_{R,u}$ is $\sum_{\mu\in\mathcal{M}_{\Psi,\mu}}W(\mu,w,\overline{w})\cdot(u+1)^{cc(\mu_{R})}$ , which completes the proof. $\hfill\blacktriangleleft$

Proposition 13.

The $n$ -th WCP $f_{n}(u;\Psi,w,\overline{w},R)$ always exists, and it is a unique univariate polynomial of degree at most $n$ .

Proof.

The existence and the upper bound of the degree follow immediately from Proposition 12 since $cc(\mu_{R})\leq n$ . $\hfill\blacktriangleleft$

3.2 Fast Calculation

Before applying the polynomials in any context, we need to be able to compute them (or at least evaluate them at some points) efficiently. By Proposition 13, $n+1$ evaluations are sufficient to interpolate the $n$ -th WCP (e.g., by Lagrange Interpolation). Therefore, our task is to evaluate the WCP at $u=0,1,\cdots,n$ .

Note that by definition, evaluating the polynomial at a specific positive integer is a WFOMC query. However, such WFOMC is not readily solvable by existing algorithms (e.g., [2, 27]) even for the $\text{FO}^{2}$ fragment. In general, the runtime of these algorithms is exponential in the length of the sentence, while the length of the sentence $\Psi_{R,u}$ in the WFOMC query can be as large as the domain size $n$ , hence these algorithms would not lead to polynomial runtime in the domain size. Luckily, by exploiting the structure of $\Psi_{R,u}$ carefully, the algorithm computing WFOMC for $\text{FO}^{2}$ can be adapted into a dynamic programming (DP) style algorithm that achieves an efficient calculation of the polynomials for $\text{C}^{2}$ sentences with cardinality constraints, which is elaborated in detail in Appendix C.

Proposition 14.

Computing WCP for a given $\text{C}^{2}$ sentence with cardinality constraints, a domain of size $n$ , a distinguished binary relation, and weighting functions can be completed in polynomial time in $n$ .

3.3 Applications

In this section, we show how WCP can be used for computing WFOMC of $\text{C}^{2}$ sentences with cardinality constraints and several combinatorial axioms in polynomial time, i.e. we show that the fragments together with each of these axioms are domain-liftable. We also show that WCP allows us to efficiently compute the Tutte polynomial of any graph that can be encoded by a set of ground unary literals, cardinality constraints and a fixed $\text{C}^{2}$ sentence, e.g., block-structured graphs.

Most of the axioms in this section require some binary relation $R$ to be symmetric and irreflexive. In this case, we append $\forall x\forall y\left(R(x,y)\to R(y,x)\right)\land\forall x\lnot R(x,x)$ to the input sentence $\Psi$ , and interpret the graph $G(R)$ as a simple undirected graph. We denote the new sentence by $\Psi_{R}$ .

3.3.1 Axioms: Existing, Generalized, and New

We first show how WFOMC with several existing and new combinatorial axioms can be computed using WCP.

$𝒌$ -connected-component axiom.

As in Proposition 12, WCP associates the weight of each model with a term indicating the number of connected components in $G(R)$ , therefore we can restrict the number of connected components of $G(R)$ .

Theorem 15.

The fragment of $\text{C}^{2}$ with cardinality constraints and a single $k$ -connected-component axiom is domain-liftable. More concretely, for any $\text{C}^{2}$ sentence $\Psi$ with cardinality constraints, a domain of size $n$ , weighting functions $w,\overline{w}$ and a distinguished binary predicate $R$ , it holds

\mathsf{WFOMC}(\Psi\land connected_{k}(R),n,w,\overline{w})=[u^{k}]f_{n}(u-1;% \Psi_{R},w,\overline{w},R).

Proof.

Consider a $\text{C}^{2}$ sentence $\Psi$ with cardinality constraints, a domain of size $n$ , the weighting functions $w,\overline{w}$ , and a distinguished binary predicate $R$ . By Proposition 12, we have that $\mathsf{WFOMC}(\Psi\land connected_{k}(R),n,w,\overline{w})$ is equal to $[u^{k}]f_{n}(u-1;\Psi_{R},w,\overline{w},R)$ . $\hfill\blacktriangleleft$

Bipartite axiom.

The bipartite axiom to the binary predicate $R$ , denoted by $bipartite(R)$ , requires $R$ to be symmetric and $G(R)$ to be a bipartite graph⁶⁶6Note that bipartite graphs are not finitely axiomatizable in first-order logic by the compactness theorem..

Theorem 16.

The fragment of $\text{C}^{2}$ with cardinality constraints and a single bipartite axiom is domain-liftable.

Tree and forest axioms.

The tree axiom [28] to the binary predicate $R$ (denoted by $tree(R)$ ) requires $R$ to be symmetric and $G(R)$ to be a tree. The forest axiom [17] to the binary predicate $R$ (denoted by $forest(R)$ ) requires $R$ to be symmetric and $G(R)$ to be a forest. To handle these two axioms, we extend the ability of WCP to classify the models of a sentence by both the number of connected components in $G(R)$ and the number of edges in $G(R)$ by introducing a new variable to the weight of $R$ .

Definition 17.

With the notations in Definition 11, the extended WCP of $\Psi$ is defined as a bivariate polynomial such that for all positive integers $u$ and all real numbers $v$ ,

\hat{f}_{n}(u,v;\Psi,w,\overline{w},R)=\mathsf{WFOMC}(\Psi_{R,u},n,w_{R,v},% \overline{w}),

where $w_{R,v}(R)=w(R)\cdot v$ , and $w_{R,v}(P)=w(P)$ for any other predicate $P$ .

Corollary 18 (Corollary from Propositions 12 and 14).

For the sentence $\Psi$ containing the symmetric binary relation $R$ , a domain of size $n$ , and the weighting functions $w,\overline{w}$ , we have

\hat{f}_{n}(u,v;\Psi,w,\overline{w},R)=\sum_{\mu\in\mathcal{M}_{\Psi,n}}W(\mu,% w,\overline{w})\cdot(u+1)^{cc(\mu_{R})}v^{2e(\mu_{R})},

where $cc(\mu_{R})$ is the number of connected components of $G(\mu_{R})$ and $e(\mu_{R})$ is the number of undirected edges⁷⁷7Here, as $R$ is symmetric, $G(\mu_{R})$ is interpreted as an undirected graph, and the number of undirected edges is equal to half the cardinality of $R$ in $\mu$ . It is where the number $2$ in the exponent comes from.of $G(\mu_{R})$ . Furthermore, the extended WCP of $\Psi$ always exists, and can be computed in time polynomial in $n$ using the same techniques as in Proposition 14.

With the above corollary, we can show that the tree and forest axioms are domain-liftable.

Theorem 19.

The fragment of $\text{C}^{2}$ with cardinality constraints and a single tree axiom is domain-liftable. Specifically,

\displaystyle\mathsf{WFOMC}(\Psi\land

\displaystyle tree(R),n,w,\overline{w})=[uv^{2(n-1)}]\hat{f}_{n}(u-1,v;\Psi_{R% },w,\overline{w},R).

Theorem 20.

The fragment of $\text{C}^{2}$ with cardinality constraints and a single forest axiom is domain-liftable. Specifically,

\displaystyle\mathsf{WFOMC}(

\displaystyle\Psi\land forest(R),n,w,\overline{w})=\sum_{i\in[n]}[u^{i}v^{2(n-% i)}]\hat{f}_{n}(u-1,v;\Psi_{R},w,\overline{w},R).

$\blacktriangleright$ Remark 21.

The tree axiom and the forest axiom have already been shown to be domain-liftable in [28] and [17] respectively. Nevertheless, our method provides a more flexible command of the graph structures. For example, it is easy to add further constraints on the number of trees in the forest by our method (we will discuss this in Section 5).

The strong expressive power of $\text{C}^{2}$ fragment with cardinality constraints and the axioms above allows us to represent many interesting combinatorial problems as well as Statistical Relational Learning (SRL) problems.

Example 22.

In a social network, one may want to model the compactness in terms of a symmetric relation $f r i e n d s$ by the number of connected components in $G(friends)$ . In this case, a real number $d$ might be used to represent the degree of compactness: the larger $d$ means that the network is more compact, i.e., the number of connected components in $G(friends)$ is smaller. This can be achieved by defining the weight of a possible world $\omega$ as $W(\omega,w,\overline{w})\cdot\exp(-d\cdot cc(\omega_{friends}))$ . Then the reduced WFOMC of the inference problem is equal to $f_{n}(\exp(-d)-1;\Psi,w,\overline{w},friends)$ , where $\Psi$ and $(w,\overline{w})$ are the sentence and weighting functions modeling other aspects of the social network.

3.3.2 From WCP to Tutte Polynomial

We can further use the extended WCP in Definition 17 to obtain the well-known Tutte polynomial ([25], also see Appendix B for the formal definition) of undirected graphs that can be encoded by a set of ground unary literals, cardinality constraints and a fixed $\text{C}^{2}$ sentence. Note that the size of the $\text{C}^{2}$ sentence should be fixed to a constant independent of the graph size (i.e., the number of vertices) while the parameters for cardinality constraints and the size of ground unary literals are unbounded. The weighting functions are all set to $\mathds{1}$ (i.e., a function always returns $1$ ) in the rest of this section.

Theorem 23.

Let $S$ be an infinite set of undirected graphs. Suppose that there is a fixed $\text{C}^{2}$ sentence $\Psi$ with a distinguished symmetric binary relation $E$ such that for each graph $G\in S$ of size $n$ , there is a $\text{C}^{2}$ sentence $\Psi_{G}$ obtained by conjuncting $\Psi$ with cardinality constraints and ground unary literals, and $G$ is isomorphic to $G(\mu_{E})$ for each model $\mu\in\mathcal{M}_{\Psi_{G},n}$ .⁸⁸8For instance, [11] gave the characterization of such graphs when the sentence is restricted to be in $\text{C}^{2}$ . Note that in their work the counting parameters and the size of the sentence are unbounded while in our case they should be constant to apply the fast calculation of WCP. Then the Tutte polynomial of any $G\in S$ of size $n$ can be computed as follows in time polynomial in $n$ :

T(x,y)=\frac{\hat{f}_{n}\left((x-1)(y-1)-1,\sqrt{y-1};\Psi_{T}(G),\mathds{1},% \mathds{1},R\right)}{(x-1)^{cc(\mu_{E})}(y-1)^{n}\mathsf{WFOMC}(\Psi_{G},n,% \mathds{1},\mathds{1})},

where $\Psi_{T}(G)=\Psi_{G}\land\forall x\forall y\ \left((R(x,y)\to E(x,y))\land(R(x% ,y)\to R(y,x))\right)$ .

Proof.

Denote the edges of $G(\mu_{E})$ by $\mathcal{E}$ . By Corollary 18, we have

		$\displaystyle\hat{f}_{n}\left((x-1)(y-1)-1,\sqrt{y-1};\Psi_{T}(G),\mathds{1},% \mathds{1},R\right)$
	$\displaystyle=$	$\displaystyle\sum_{\mu^{\prime}\in\mathcal{M}_{\Psi_{T}(G),n}}(x-1)^{cc(\mu^{% \prime}_{R})}(y-1)^{cc(\mu^{\prime}_{R})+e(\mu^{\prime}_{R})}$
	$\displaystyle=$	$\displaystyle\mathsf{WFOMC}(\Psi_{G},n,\mathds{1},\mathds{1})\cdot\sum_{A% \subseteq\mathcal{E}}(x-1)^{cc(A)}(y-1)^{cc(A)+\|A\|}$
	$\displaystyle=$	$\displaystyle\mathsf{WFOMC}(\Psi_{G},n,\mathds{1},\mathds{1})\cdot(x-1)^{cc(% \mu_{E})}(y-1)^{n}\cdot T_{G}(x,y),$

where $T_{G}(x,y)$ is the Tutte polynomial of $G$ defined in Appendix B.

By Corollary 18, computing $f_{n}\left((x-1)(y-1)-1,\sqrt{y-1};\Psi_{T}(G),\mathds{1},\mathds{1},R\right)$ is in polynomial time in $n$ . Since the cardinality of $S$ is infinite, the size of $\Psi$ is independent of the size of $G$ , thus $\mathsf{WFOMC}(\Psi_{G},n,\mathds{1},\mathds{1})$ can be computed in time polynomial in $n$ by the algorithm described in Appendix A as well. Therefore, we can obtain $T(x,y)$ in time polynomial in $n$ . $\hfill\blacktriangleleft$

Example 24.

We can get the Tutte polynomial for a simple undirected complete graph of any size $n$ . Let $S$ be the set of all simple undirected complete graphs and define

\displaystyle\Psi=\forall x\lnot E(x,x),\qquad\Psi_{G}=\Psi\land(|E|=n(n-1))

for each $G\in S$ of size $n$ .

Then $\Psi_{G}$ has a unique model $\mu$ over the domain of size $n$ such that $G(\mu_{E})$ is identical to $G$ . Therefore,

\frac{\hat{f}_{n}\left((x-1)(y-1)-1,\sqrt{y-1};\Psi_{T}(G),\mathds{1},\mathds{% 1},R\right)}{(x-1)(y-1)^{n}}

is the Tutte polynomial of the complete graph of size $n$ , which can be computed in polynomial time in $n$ by Theorem 23.

Example 25.

Consider the Tutte polynomial of a block-structured graph defined in Example 8. We first fix the number $k$ of blocks and the connection among blocks. Let $S$ be the set of block-structured graphs of $n$ vertices such that each graph has $k$ blocks and the fixed connection. Define similarly to Equation (1) the following sentences:

	$\displaystyle\Psi=$	$\displaystyle\bigwedge_{V_{i},V_{j}\text{ are connected}}(Block_{i}(x)\land Block% _{j}(y)\to E(x,y))$
		$\displaystyle\land\bigwedge_{V_{i},V_{j}\text{ are not connected}}(Block_{i}(x% )\land Block_{j}(y)\to\lnot E(x,y)),$
	$\displaystyle\Psi_{G}=$	$\displaystyle\Psi\land\bigwedge_{e\in V}\left(Block_{v(e)}(e)\land\bigwedge_{j% \neq v(e)}\lnot Block_{j}(e)\right)$

for each $G\in S$ of size $n$ . Then, the Tutte polynomial of $G$ is

\frac{\hat{f}_{n}\left((x-1)(y-1)-1,\sqrt{y-1};\Psi_{T}(G),\mathds{1},\mathds{% 1},R\right)}{(x-1)^{cc(G)}(y-1)^{n}}.

By Theorem 23, the Tutte polynomial of $G$ can be computed in polynomial time in $n$ . Applying the same proof to any constant $k$ and any possible connection among blocks, we conclude that the Tutte polynomial of any block-structured graph can be computed in polynomial time in the size of the graph.

The above result answers positively the question in [28] whether calculating the Tutte polynomial of a block-structured graph is hard. However, we remark that this result cannot be extended to computing the Tutte polynomial or evaluating any point for general graphs since representing a general graph by a first-order sentence involves a list of ground binary literals, making the WFOMC task $\mathsf{\#P}$ -hard [30]. Therefore we are consistent with the hardness of computing the Tutte polynomial of general graphs [9], while showing tractability for block-structured ones (with a constant number of blocks).

4 Strong Connectedness Polynomials

The polynomial WCP is insensitive to the orientation of the edges of $G(R)$ , where $R$ is the distinguished relation. Hence, with WCP we can only define axioms that do not depend on the orientation of the edges of the graph $G(R)$ . In this section, we define two new polynomials, Strict Strong Connectedness Polynomial (SSCP) and Non-strict Strong Connectedness Polynomial (NSCP), that use the orientation of the edges as well. Both polynomials are collectively referred to as Strong Connectedness Polynomials (SCPs). We show that these new polynomials can be used to enforce several axioms, some of which have not been known to be domain-liftable before. All the omitted proofs can be found in the full version.

4.1 Definition

The definitions of SCPs are similar to WCP except that we need another sequence of unary predicates to characterize the strong connectedness in $G(R)$ .

Definition 26 (Strong Connectedness Polynomials).

Let $\Psi$ be a first-order logic sentence possibly with cardinality constraints and ground unary literals, $w$ and $\overline{w}$ be two weighting functions and $R$ be a distinguished binary relation. The $n$ -th Strict Strong Connectedness Polynomial (SSCP) $g_{n}(u,v)$ of $\Psi$ for the relation $R$ is the bivariate polynomial which satisfies:

g_{n}(u,v;\Psi,w,\overline{w},R)=\mathsf{WFOMC}(\Psi_{R,u,v},n,w,\overline{w})

for all positive integers $u, v$ , where $\Psi_{R,u,v}$ is defined as:

	$\displaystyle\Psi_{R,u,v}=\Psi\land$	$\displaystyle\bigwedge_{i=1}^{u}\forall x\forall y\left(A_{i}(x)\wedge(R(x,y)% \vee R(y,x))\to A_{i}(y)\right)\wedge\bigwedge_{i=2}^{u}\forall x\left(A_{i}(x% )\to A_{i-1}(x)\right)$
	$\displaystyle\wedge$	$\displaystyle\bigwedge_{i=1}^{v-1}\forall x\forall y\left(B_{i}(x)\wedge R(x,y% )\to B_{i+1}(y)\right)\wedge\forall x\forall y\left(R(x,y)\to\lnot B_{v}(x)% \land B_{1}(y)\right)$
	$\displaystyle\wedge$	$\displaystyle\bigwedge_{i=2}^{v}\forall x\left(B_{i}(x)\to B_{i-1}(x)\right)$

where $A_{i}$ ’s and $B_{i}$ ’s are fresh unary predicates and $w(A_{i})=\overline{w}(A_{i})=w(B_{i})=\overline{w}(B_{i})=1$ .

The $n$ -th Non-strict Strong Connectedness Polynomial (NSCP) $\bar{g}_{n}(u,v)$ of $\Psi$ for the relation $R$ is the bivariate polynomial which satisfies:

\bar{g}_{n}(u,v;\Psi,w,\overline{w},R)=\mathsf{WFOMC}(\bar{\Psi}_{R,u,v},n,w,% \overline{w})

for all positive integers $u, v$ , where $\bar{\Psi}_{R,u,v}$ is defined as:

	$\displaystyle\bar{\Psi}_{R,u,v}=\Psi\land$	$\displaystyle\bigwedge_{i=1}^{u}\forall x\forall y\left(A_{i}(x)\wedge(R(x,y)% \vee R(y,x))\to A_{i}(y)\right)\wedge\bigwedge_{i=2}^{u}\forall x\left(A_{i}(x% )\to A_{i-1}(x)\right)$
	$\displaystyle\wedge$	$\displaystyle\bigwedge_{i=1}^{v}\forall x\forall y\left(B_{i}(x)\wedge R(x,y)% \to B_{i}(y)\right)\wedge\bigwedge_{i=2}^{v}\forall x\left(B_{i}(x)\to B_{i-1}% (x)\right)$

where $A_{i}$ ’s and $B_{i}$ ’s are fresh unary predicates and $w(A_{i})=\overline{w}(A_{i})=w(B_{i})=\overline{w}(B_{i})=1$ .

The predicates $A_{1},\cdots,A_{u}$ treat $R$ symmetrically and are defined similarly as those in WCP. As discussed in Proposition 12, we can imagine them as capturing the information about weakly connected components of $G(R)$ . The predicates $B_{1},\cdots,B_{v}$ capture the directionality of edges in $G(R)$ , enabling further directed axioms on $R$ . We give an interpretation of both SSCP and NSCP by the following proposition and present more properties and applications in Section 4.3.

Proposition 27.

For the sentence $\Psi$ , the weighting functions $w$ and $\overline{w}$ and the binary relation $R$ , it holds that

	$\displaystyle g_{n}(u,v;\Psi,w,\overline{w},R)$	$\displaystyle=\sum_{\mu\in\mathcal{M}_{\Psi,n}}W(\mu,w,\overline{w})\cdot(u+1)% ^{cc(\mu_{R})}\cdot\chi_{G(\mu_{R})}(v+1),$
	$\displaystyle\bar{g}_{n}(u,v;\Psi,w,\overline{w},R)$	$\displaystyle=\sum_{\mu\in\mathcal{M}_{\Psi,n}}W(\mu,w,\overline{w})\cdot(u+1)% ^{cc(\mu_{R})}\cdot\bar{\chi}_{G(\mu_{R})}(v+1),$

where $cc(\mu_{R})$ is the number of weekly connected components of $G(\mu_{R})$ , and $\chi_{G(\mu_{R})}$ and $\bar{\chi}_{G(\mu_{R})}$ are the strict and non-strict directed chromatic polynomials ([22], also see Appendix B for the formal definitions) of $G(\mu_{R})$ respectively.

Proposition 28.

$g_{n}(u,v;\Psi,w,\overline{w},R)$ and $\bar{g}_{n}(u,v;\Psi,w,\overline{w},R)$ always exist, and they are unique bivariate polynomials in which both variables have a degree at most $n$ .

4.2 Fast Calculation

Similarly to WCP, we can efficiently compute both SCPs for $\text{C}^{2}$ sentences with cardinality constraints.

Proposition 29.

Computing NSCP for a given $\text{C}^{2}$ sentence with cardinality constraints, a domain of size $n$ , a distinguished binary relation, and weighting functions can be completed in polynomial time in $n$ .

Proposition 30.

Computing SSCP for a given $\text{C}^{2}$ sentence with cardinality constraints, a domain of size $n$ , a distinguished binary relation, and weighting functions can be completed in polynomial time in $n$ .

4.3 Applications

Now, we show how SCP can be used for axioms that are associated with the orientation of the edges in $G(R)$ , and for computing the directed chromatic polynomial of certain graphs.

Strong connectedness axiom.

The strong connectedness axiom to the binary predicate $R$ , denoted by $SC(R)$ , requires $G(R)$ to be a strongly connected directed graph.

Theorem 31.

The fragment of $\text{C}^{2}$ with cardinality constraints and a single strong connectedness axiom is domain-liftable. More concretely, for any $\text{C}^{2}$ sentence $\Psi$ with cardinality constraints, a domain of size $n$ , weighting functions $w,\overline{w}$ and a distinguished binary predicate $R$ , it holds

\displaystyle\mathsf{WFOMC}(\Psi

\displaystyle\land SC(R),n,w,\overline{w})=-[u]\bar{g}_{n}(u-1,-2;\Psi,w,% \overline{w},R).

Example 32.

A tournament is an orientation of an undirected complete graph. We can further require $G(R)$ to be strongly connected by adding the strongly connected tournament axiom to the binary predicate $R$ , denoted by $SCT(R)$ . For any $\text{C}^{2}$ sentence $\Psi$ with cardinality constraints, a domain of size $n$ , weighting functions $w,\overline{w}$ and a distinguished binary predicate $R$ , the sentence

	$\displaystyle\Psi_{TN}$	$\displaystyle=\Psi\land\forall x\left(\lnot R(x,x)\land Eq(x,x)\right)\land(\|% Eq\|=n)$		(3)
		$\displaystyle\land\forall x\forall y\big(\lnot Eq(x,y)\to(R(x,y)\lor R(y,x))% \land(\lnot R(x,y)\lor\lnot R(y,x))\big)$		(3)

restricts $G(R)$ to be a tournament. Then by Theorem 31, it holds that

\displaystyle\mathsf{WFOMC}(\Psi

\displaystyle\land SCT(R),n,w,\overline{w})=-[u]\bar{g}_{n}(u-1,-2;\Psi_{TN},w% ,\overline{w},R).

Therefore, the fragment of $\text{C}^{2}$ with cardinality constraints and a single strongly connected tournament axiom is domain-liftable.

Acyclicity axiom.

The acyclicity axiom to the binary predicate $R$ , denoted by $AC(R)$ , requires that $G(R)$ does not have any directed cycle, or equivalently, $G(R)$ is a directed acyclic graph (DAG).

Theorem 33.

The fragment of $\text{C}^{2}$ with cardinality constraints and a single acyclicity axiom is domain-liftable. Specifically,

\displaystyle\mathsf{WFOMC}(\Psi

\displaystyle\land AC(R),n,w,\overline{w})=(-1)^{n}\cdot g_{n}(0,-2;\Psi,w,% \overline{w},R).

Directed tree and forest axioms.

The directed tree axiom to the binary predicate $R$ and the unary predicate $R o o t$ , denoted by $DT(R,Root)$ , requires that $G(R)$ is a DAG with a single source, and the single source interprets $R o o t$ as true. The directed forest axiom to the binary predicate $R$ , denoted by $DF(R)$ , requires that $G(R)$ is a DAG such that every weakly connected component is a directed tree. In other words, $G(R)$ is a DAG such that every vertex has at most one incoming edge.

Theorem 34.

The fragment of $\text{C}^{2}$ with cardinality constraints and a single directed tree axiom or a single directed forest axiom is domain-liftable.

Linear order axiom.

The linear order axiom to the binary predicate $R$ , denoted by $LO(R)$ , requires that $R$ represents a linear order. That is to say, $G(R)$ is an acyclic tournament with a self-loop for each vertex.

Theorem 35.

The fragment of $\text{C}^{2}$ with cardinality constraints and a single linear order axiom is domain-liftable.

$\blacktriangleright$ Remark 36.

Though some of the axioms have been proven to be domain-liftable such as the acyclicity axiom in [17] and the linear order axiom in [24], by our approach we can further generalize these axioms to obtain more features such as restricting the number of weakly connected components of $G(R)$ of an acyclic graph. For example, if we require $G(R)$ to be the union of $k$ disjoint directed acyclic graphs, we can obtain the WFOMC by $(-1)^{n}\cdot[u^{k}]g_{n}(u-1,-2;\Psi,w,\overline{w},R)$ .

From SSCP and NSCP to Directed Chromatic Polynomials.

With the same idea of obtaining the Tutte polynomial for graphs encoded by a set of ground unary literals, cardinality constraints and a fixed $\text{C}^{2}$ sentence, we can recover the strict and non-strict directed chromatic polynomials ([22], also see Appendix B for the formal definitions) from SSCP and NSCP respectively of such sentences encoding directed graphs.

Corollary 37 (Corollary from Theorem 23).

Let $S$ be an infinite set of directed graphs. Suppose that there is a fixed $\text{C}^{2}$ sentence $\Psi$ with a distinguished binary relation $E$ such that for each $D\in S$ of size $n$ , there is a $\text{C}^{2}$ sentence $\Psi_{D}$ obtained by conjuncting $\Psi$ with cardinality constraints and ground unary literals, and $D$ is isomorphic to $G(\mu_{E})$ for each model $\mu\in\mathcal{M}_{\Psi_{D},n}$ . Then the strict and non-strict directed chromatic polynomials of any $D\in S$ of size $n$ can be computed as follows in time polynomial in $n$ :

\displaystyle\chi_{D}(x)=\frac{g_{n}\left(0,x;\Psi_{D},\mathds{1},\mathds{1},E% \right)}{\mathsf{WFOMC}(\Psi_{D},n,\mathds{1},\mathds{1})},\qquad\bar{\chi}_{D% }(x)=\frac{\bar{g}_{n}\left(0,x;\Psi_{D},\mathds{1},\mathds{1},E\right)}{% \mathsf{WFOMC}(\Psi_{D},n,\mathds{1},\mathds{1})},

where $\mathds{1}$ is the weighting function that always returns 1.

5 Combinations of Axioms

An important advantage of the proposed approach over the prior works is that it can easily extend to new axioms by combining existing axioms. Adopting the methodology of existing research [28, 24, 17], one would typically delve into the literature on polytree enumeration [20] and attempt to adapt the techniques (if they exist) to the WFOMC problem. However, even if such techniques are available, integrating them into current WFOMC algorithms is not a trivial task. In contrast, our approach leverages a single polynomial to encapsulate the structural characteristics of the models.

Theorem 38.

The fragment of $\text{C}^{2}$ with cardinality constraints and a single axiom in the following list is domain-liftable.

$\blacksquare$

$bipartite_{k}(R)=connected_{k}(R)\land bipartite(R)$ , requiring $G(R)$ to be a bipartite graph with $k$ connected components;
$\blacksquare$

$forest_{k}(R)=connected_{k}(R)\land forest(R)$ , requiring $G(R)$ to be a forest with $k$ trees;
$\blacksquare$

$AC_{k}(R)=connected_{k}(R)\land AC(R)$ , requiring $G(R)$ to be a DAG with $k$ weakly connected components;
$\blacksquare$

$BiAC(R)=bipartite(R)\land AC(R)$ , requiring $G(R)$ to be a DAG whose underlying undirected graph is bipartite;
$\blacksquare$

$polytree(R)=tree(R)\land AC(R)$ , requiring $G(R)$ to be a polytree, i.e., a DAG whose underlying undirected graph is a tree;
$\blacksquare$

$polyforest(R)=forest(R)\land AC(R)$ , requiring $G(R)$ to be a polyforest, i.e., a DAG whose underlying undirected graph is a forest.

Note that in the combination of axioms involving $AC(R)$ , we do not require $R$ to be symmetric.

References

[1] Jordan Awan and Olivier Bernardi. Tutte polynomials for directed graphs. Journal of Combinatorial Theory, Series B, 140:192–247, 2020. doi:10.1016/j.jctb.2019.05.006.
[2] Paul Beame, Guy Van den Broeck, Eric Gribkoff, and Dan Suciu. Symmetric weighted first-order model counting. In PODS, pages 313–328. ACM, 2015. doi:10.1145/2745754.2745760.
[3] Rodrigo de Salvo Braz, Eyal Amir, and Dan Roth. Lifted first-order probabilistic inference. In IJCAI, pages 1319–1325. Professional Book Center, 2005. URL: http://ijcai.org/Proceedings/05/Papers/1548.pdf.
[4] Reinhard Diestel, Alexander Schrijver, and Paul Seymour. Graph theory. Oberwolfach Reports, 4(2):887–944, 2008.
[5] Lise Getoor and Ben Taskar. Introduction to statistical relational learning, volume 1. MIT press Cambridge, 2007.
[6] Vibhav Gogate and Pedro M. Domingos. Probabilistic theorem proving. In UAI, pages 256–265. AUAI Press, 2011. URL: https://dslpitt.org/uai/displayArticleDetails.jsp?mmnu=1&smnu=2&article_id=2263&proceeding_id=27.
[7] Erich Grädel, Phokion G. Kolaitis, and Moshe Y. Vardi. On the decision problem for two-variable first-order logic. Bull. Symb. Log., 3(1):53–69, 1997. doi:10.2307/421196.
[8] Erich Grädel, Martin Otto, and Eric Rosen. Two-variable logic with counting is decidable. In LICS, pages 306–317. IEEE Computer Society, 1997. doi:10.1109/LICS.1997.614957.
[9] François Jaeger, Dirk L Vertigan, and Dominic JA Welsh. On the computational complexity of the jones and tutte polynomials. Mathematical Proceedings of the Cambridge Philosophical Society, 108(1):35–53, 1990.
[10] Seyed Mehran Kazemi, Angelika Kimmig, Guy Van den Broeck, and David Poole. New liftable classes for first-order probabilistic inference. In Advances in Neural Information Processing Systems 29: Annual Conference on Neural Information Processing Systems, pages 3117–3125, 2016. URL: https://proceedings.neurips.cc/paper/2016/hash/c88d8d0a6097754525e02c2246d8d27f-Abstract.html.
[11] Sandra Kiefer, Pascal Schweitzer, and Erkal Selman. Graphs identified by logics with counting. ACM Trans. Comput. Log., 23(1):1:1–1:31, 2022. doi:10.1145/3417515.
[12] Qipeng Kuang. l2l7l9p/Polynomials-for-WFOMC. Software, swhId: swh:1:dir:e82fa8e26998cfb9e25e723b2c1182f17a82276e (visited on 2026-02-02). URL: https://github.com/l2l7l9p/Polynomials-for-WFOMC, doi:10.4230/artifacts.25483.
[13] Antti Kuusisto and Carsten Lutz. Weighted model counting beyond two-variable logic. In LICS, pages 619–628. ACM, 2018. doi:10.1145/3209108.3209168.
[14] Ondrej Kuzelka. Weighted first-order model counting in the two-variable fragment with counting quantifiers. J. Artif. Intell. Res., 70:1281–1307, 2021. doi:10.1613/jair.1.12320.
[15] Michel Las Vergnas. Convexity in oriented matroids. J. Comb. Theory, Ser. B, 29(2):231–243, 1980. doi:10.1016/0095-8956(80)90082-9.
[16] Leonid Libkin. Elements of finite model theory, volume 41. Springer, 2004. doi:10.1007/978-3-662-07003-1.
[17] Sagar Malhotra, Davide Bizzaro, and Luciano Serafini. Lifted inference beyond first-order logic. Artif. Intell., 342:104310, 2025. doi:10.1016/j.artint.2025.104310.
[18] David Poole. First-order probabilistic inference. In IJCAI, pages 985–991. Morgan Kaufmann, 2003. URL: http://ijcai.org/Proceedings/03/Papers/142.pdf.
[19] Ronald C Read. An introduction to chromatic polynomials. Journal of combinatorial theory, 4(1):52–71, 1968.
[20] George Rebane and Judea Pearl. The recovery of causal poly-trees from statistical data. In UAI, pages 175–182. Elsevier, 1987. URL: https://dslpitt.org/uai/displayArticleDetails.jsp?mmnu=1&smnu=2&article_id=1813&proceeding_id=1003.
[21] Matthew Richardson and Pedro M. Domingos. Markov logic networks. Mach. Learn., 62(1-2):107–136, 2006. doi:10.1007/s10994-006-5833-1.
[22] Richard P Stanley. A chromatic-like polynomial for ordered sets. In Proc. Second Chapel Hill Conf. on Combinatorial Mathematics and its Applications (Univ. North Carolina, Chapel Hill, NC, 1970), Univ. North Carolina, Chapel Hill, NC, pages 421–427, 1970.
[23] Richard P Stanley. What is enumerative combinatorics? Springer, 1986.
[24] Jan Tóth and Ondřej Kuželka. Lifted inference with linear order axiom. In AAAI, pages 12295–12304. AAAI Press, 2023. doi:10.1609/aaai.v37i10.26449.
[25] William Thomas Tutte. A contribution to the theory of chromatic polynomials. Canadian journal of mathematics, 6:80–91, 1954.
[26] WT Tutte. Graph-polynomials. Advances in Applied Mathematics, 32(1-2):5–9, 2004. doi:10.1016/S0196-8858(03)00041-1.
[27] Timothy van Bremen and Ondrej Kuzelka. Faster lifting for two-variable logic using cell graphs. In UAI, volume 161 of Proceedings of Machine Learning Research, pages 1393–1402. AUAI Press, 2021. URL: https://proceedings.mlr.press/v161/bremen21a.html.
[28] Timothy van Bremen and Ondrej Kuzelka. Lifted inference with tree axioms. Artif. Intell., 324:103997, 2023. doi:10.1016/j.artint.2023.103997.
[29] Guy Van den Broeck. On the completeness of first-order knowledge compilation for lifted probabilistic inference. In NIPS, pages 1386–1394, 2011. URL: https://proceedings.neurips.cc/paper/2011/hash/846c260d715e5b854ffad5f70a516c88-Abstract.html.
[30] Guy Van den Broeck and Jesse Davis. Conditioning in first-order knowledge compilation and lifted probabilistic inference. In AAAI, pages 1961–1967. AAAI Press, 2012. doi:10.1609/aaai.v26i1.8404.
[31] Guy Van den Broeck, Wannes Meert, and Adnan Darwiche. Skolemization for weighted first-order model counting. In KR. AAAI Press, 2014. URL: http://www.aaai.org/ocs/index.php/KR/KR14/paper/view/8012.
[32] Moshe Y. Vardi. The complexity of relational query languages (extended abstract). In STOC, pages 137–146. ACM, 1982. doi:10.1145/800070.802186.
[33] Yuanhong Wang, Juhua Pu, Yuyi Wang, and Ondrej Kuzelka. On exact sampling in the two-variable fragment of first-order logic. In LICS, pages 1–13. IEEE, 2023. doi:10.1109/LICS56636.2023.10175742.
[34] Yuanhong Wang, Juhua Pu, Yuyi Wang, and Ondrej Kuzelka. Lifted algorithms for symmetric weighted first-order model sampling. Artif. Intell., 331:104114, 2024. doi:10.1016/j.artint.2024.104114.

Appendix A Domain-Liftability of $\text{FO}^{2}$

We briefly describe the algorithm of computing WFOMC for $\text{FO}^{2}$ , as some of its concepts are important for designing algorithms for computing our polynomials efficiently. We mostly follow the notation from [27]. Any sentence in $\text{FO}^{2}$ can be reduced to the prenex normal form with only universal quantifiers (i.e., $\forall x\forall y\ \psi(x,y)$ , where $\psi(x,y)$ is a quantifier-free formula) by the normalization in [7] and the technique of eliminating existential quantifiers in [31]. The reduction respects the WFOMC value, and hence in what follows, we assume that the input sentence is in the form $\forall x\forall y\ \psi(x,y)$ . Two notions are needed to present the algorithm.

Definition 39 (1-type).

A 1-type of a first-order sentence $\Psi$ is a maximally consistent set⁹⁹9A set of literals is maximally consistent if it is consistent (does not contain both a literal and its negation) and cannot be extended to a larger consistent set. of literals formed from atoms in $\Psi$ using only a single variable $x$ .

For example, $\Psi=\forall x\forall y\left(F(x)\land G(x,y)\right)$ has four 1-types: $F(x)\land G(x,x)$ , $F(x)\land\lnot G(x,x)$ , $\lnot F(x)\land G(x,x)$ and $\lnot F(x)\land\lnot G(x,x)$ . Intuitively, a 1-type interprets unary and reflexive binary predicates for a single domain element.

The weighted model counting problem (WMC) is defined similarly but the input formula is a ground quantifier-free formula.

Definition 40 (Weighted Model Counting).

The WMC of a ground quantifier-free formula $\Phi$ under weighting functions $(w,\overline{w})$ is $\mathsf{WMC}(\Phi,w,\overline{w}):=\sum_{\mu\in\mathcal{M}_{\Phi}}W(\mu,w,% \overline{w})$ , where $\mathcal{M}_{\Phi}$ denotes the set of all models of $\Phi$ .

Example 41.

The WMC of a ground quantifier-free formula $\Phi=R(a,b)\to S(a)$ under $w(R)=2,\overline{w}(R)=w(S)=\overline{w}(S)=1$ is

W(\{R(a,b),S(a)\},w,\overline{w})+W(\{\lnot R(a,b),S(a)\},w,\overline{w})+W(\{% \lnot R(a,b),\lnot S(a)\},w,\overline{w})=4.

Let $C_{1}(x),C_{2}(x),\cdots,C_{p}(x)$ be all the 1-types of $\Psi$ . When we consider domain-liftability, the sentence $\Psi$ is fixed and therefore $p$ is a constant. We partition domain elements into 1-types by enumerating the configuration $\bm{c}=(c_{1},c_{2},\cdots,c_{p})$ , a vector indicating the number of elements partitioned to each 1-type, since in the symmetric WFOMC only the configuration matters. Then we can rewrite $\Psi$ in the form of

\displaystyle\Psi=\bigwedge_{1\leq i<j\leq p}\forall x\in C_{i}\forall y\in C_% {j}(\psi(x,y)\land\psi(y,x))\land\bigwedge_{1\leq i\leq p}\forall x\in C_{i}% \forall y\in C_{i}\ \psi(x,y),

where $\psi(x,y)$ is a quantifier-free formula.

Since we know the truth values of the unary and reflexive binary atoms of each 1-type, we may simplify the body of each conjunct by substituting every unary and reflexive binary literal with true or false as appropriate. Denote by $\psi_{i}(x,y)$ the simplification of $\psi(x,y)$ when both $x$ and $y$ belong to the same 1-type $C_{i}$ , and by $\psi_{ij}(x,y)$ the simplification of $\psi(x,y)\land\psi(y,x)$ when $x$ and $y$ belong to $C_{i}$ and $C_{j}$ respectively. We then have:

\displaystyle\Psi=\bigwedge_{1\leq i<j\leq p}\forall x\in C_{i}\forall y\in C_% {j}\ \psi_{ij}(x,y)\land\bigwedge_{1\leq i\leq p}\forall x\in C_{i}\forall y% \in C_{i}\ \psi_{i}(x,y).

An important property here is that each conjunct is independent of others since no two conjuncts involve the same ground binary literal. Let

	$\displaystyle r_{i,j}$	$\displaystyle=\mathsf{WMC}(\psi_{i,j}(a,b),w,\overline{w}),$
	$\displaystyle s_{i}$	$\displaystyle=\mathsf{WMC}(\psi_{i}(a,b)\land\psi_{i}(b,a),w,\overline{w})$

be the mutual and internal 1-type coefficient of $\Psi$ respectively. Then we have

\mathsf{WFOMC}(\Psi,n,w,\overline{w})=\sum_{|\bm{c}|=n}\binom{n}{\bm{c}}\prod_% {1\leq i\leq p}W(C_{i},w,\overline{w})^{c_{i}}\cdot s_{i}^{\binom{c_{i}}{2}}% \prod_{1\leq i<j\leq p}r_{i,j}^{c_{i}c_{j}},

(4)

which can be calculated in polynomial time in $n$ .

Appendix B Graph Polynomial

We give a brief introduction to graph polynomials which are a class of polynomials defined on graphs that carry combinatorial meaning.

Tutte Polynomial.

The Tutte polynomial [25] is one of the most well-known graph polynomials for undirected graphs. Consider an undirected graph $G=(V,E)$ , where $V$ is the set of vertices and $E$ is the set of edges. The Tutte polynomial for the graph $G$ is a polynomial in two variables $x$ and $y$ defined as

T_{G}(x,y)=\sum_{A\subseteq E}(x-1)^{cc(A)-cc(E)}(y-1)^{cc(A)+|A|-|V|},

where $cc(A)$ is the number of connected components considering only edges in $A$ .

The Tutte polynomial holds significant combinatorial meaning. Evaluating the polynomial at specific points reveals various combinatorial properties. For example, $T_{G}(1,1)$ counts the number of spanning forests of $G$ (specifically, the number of spanning trees if $G$ is connected), and $T_{G}(0,2)$ counts the strongly connected orientations of $G$ [15]. Substituting a concrete value for only one variable yields another graph polynomial of $G$ . For example, $T_{G}(x,0)$ corresponds to the chromatic polynomial [19] of $G$ ; $T_{G}(0,y)$ corresponds to the flow polynomial [4] of $G$ .

The computation of the Tutte polynomial for an arbitrary graph is known to be computationally challenging. Even the evaluation of a specific point of the polynomial is known to be $\mathsf{\#P}$ -hard, with only a limited number of points being computationally tractable [9].

Directed Chromatic Polynomial.

The idea of the chromatic polynomial of a directed graph appeared in [22], although it was originally stated in terms of ordered sets. Given a directed graph $D=(V,E)$ where $n=|V|$ , let $\chi_{D}(x)$ be the number of ways of coloring each vertex in $D$ by one of the colors $\{1,2,\cdots,x\}$ such that if there is an edge from $u$ to $v$ , the color of $u$ is smaller than the color of $v$ . We have the following lemma to state that $\chi_{D}(x)$ is a polynomial of $x$ .

Lemma 42 ([22]).

For a directed graph $D$ of size $n$ , let $\chi^{*}_{D}(i)$ be the number of surjective colorings of vertices using $i$ colors (i.e., each color should be used at least once) such that if there is an edge from $u$ to $v$ , the color of $u$ is smaller than the color of $v$ . It holds that

\chi_{D}(x)=\sum_{i=1}^{n}\binom{x}{i}\chi^{*}_{D}(i)=\sum_{i=1}^{n}\frac{x(x-% 1)\cdots(x-i+1)}{i!}\chi^{*}_{D}(i),

where $\binom{x}{i}=0$ if $i>x$ .

Corollary 43.

$\chi_{D}(x)$ is a polynomial of $x$ of degree $n$ .

We call $\chi_{D}(x)$ the strict directed chromatic polynomial of $D$ . A variant of it is the non-strict directed chromatic polynomial $\bar{\chi}_{D}(x)$ where for each positive integer $x$ , $\bar{\chi}_{D}(x)$ equals the number of colorings of the vertices in $D$ by one of the $x$ colors $\{1,2,\cdots,x\}$ such that if there is an edge from $u$ to $v$ , the color of $u$ is smaller than or equal to the color of $v$ . Similarly to $\chi_{D}(x)$ , $\bar{\chi}_{D}(x)$ is also a polynomial of $x$ .

Corollary 44.

$\bar{\chi}_{D}(x)$ is a polynomial of $x$ of degree $n$ .

The relation between $\chi_{D}(x)$ and $\bar{\chi}_{D}(x)$ is given by the following lemma.

Lemma 45 ([22, 1]).

Let $D$ be a directed graph and $acyc(D)$ be the directed acyclic graph obtained from $D$ by condensing each cycle into a vertex. Denote the number of vertices in $acyc(D)$ by $|V(acyc(D))|$ . We have

	$\displaystyle\chi_{D}(x)$	$\displaystyle=$
	$\displaystyle\bar{\chi}_{D}(x)$	$\displaystyle=(-1)^{\|V(acyc(D))\|}\chi_{acyc(D)}(-x).$

Appendix C Omitted Proofs in Section 3

Proof of Proposition 14.

Let $\Psi$ and $R$ be the input $\text{FO}^{2}$ sentence and the binary relation that WCP is defined on. Consider the point evaluation of the WCP at $u$ . Let $C_{1}(x),C_{2}(x),\cdots,C_{p}(x)$ be the valid 1-types ¹⁰¹⁰10We call a 1-type valid if it is satisfiable in some model of the sentence. of $\Psi$ . Due to the definition of $\Psi_{R,u}$ , the valid 1-types of $\Psi_{R,u}$ must have the form $C_{i}(x)\wedge C^{A}_{i^{\prime}}(x)$ , where $C^{A}_{i^{\prime}}(x)$ is defined as

\displaystyle C^{A}_{i^{\prime}}(x)=A_{1}(x)\wedge A_{2}(x)\wedge\dots A_{i^{% \prime}}(x)\wedge\lnot A_{i^{\prime}+1}(x)\wedge\dots\wedge\lnot A_{u}(x)

for $i^{\prime}\in[u]$ , and

C^{A}_{0}(x)=\lnot A_{1}(x)\wedge\lnot A_{2}(x)\wedge\dots\wedge\lnot A_{u}(x).

We use the tuple $(i,i^{\prime})$ to index the 1-type $C_{i}(x)\wedge C^{A}_{i^{\prime}}(x)$ . Then we have the following observation.

Observation 46.

Let $r_{(i,i^{\prime}),(j,j^{\prime})}$ be the mutual 1-type coefficient (defined in Appendix A) of $\Psi_{R,u}$ . It holds that

r_{(i,i^{\prime}),(j,j^{\prime})}=\begin{cases}r_{i,j}=\mathsf{WMC}(\psi_{i,j}% (a,b),w,\overline{w}),&i^{\prime}=j^{\prime},\\ \begin{aligned} r^{\not-}_{i,j}=\mathsf{WMC}(&\psi_{i,j}(a,b)\wedge\lnot R(a,b% )\wedge\lnot R(b,a),w,\overline{w}),\end{aligned}&i^{\prime}\neq j^{\prime},\\ \end{cases}

where $\psi_{i,j}(x,y)$ is the simplified formula of $\Psi$ defined in Appendix A.

This observation provides an important insight into the structure of the new 1-types (as shown in Figure 1): we can imagine that the new 1-types of $\Psi_{R,u}$ form $u+1$ layers, with each layer containing a replica of the original 1-types of $\Psi$ . If two elements $a, b$ fall in 1-types in the same layer, $R(a,b)$ can be either true or false. But if $a$ and $b$ are located in 1-types in different layers, $R(a,b)$ as well as $R(b,a)$ must be false due to the definition of $\Psi_{R,u}$ in Equation (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

).

Therefore, we can perform a “blocked” DP, where each block consists of the 1-types in the same layer. We can write the new 1-type configuration as

c_{(1,1)},\cdots,c_{(p,1)},\ c_{(1,2)},\cdots,c_{(p,2)},\ \cdots,\ c_{(1,u)},% \cdots,c_{(p,u)}

where $c_{(i,i^{\prime})}$ is the number of elements in the 1-type $(i,i^{\prime})$ . For any $\hat{u}\in[u]$ , we define $h_{\hat{u},(c_{1},c_{2},\dots,c_{p})}$ to be the weights of 1-types $(1,1),\cdots,(p,1),\cdots,(1,\hat{u}),\cdots,(p,\hat{u})$ such that $c_{i}=\sum_{j=1}^{\hat{u}}c_{(i,j)}$ for each $i\in[p]$ , that is,

	$\displaystyle h_{\hat{u},(c_{1},c_{2},\dots,c_{p})}$	$\displaystyle=\sum_{c_{(1,1)}+\cdots+c_{(1,\hat{u})}=c_{1}}\dots\sum_{c_{(p,1)% }+\cdots+c_{(p,\hat{u})}=c_{p}}\frac{(\sum_{i\in[p]}c_{i})!}{\prod_{i\in[p],i^% {\prime}\in[\hat{u}]}c_{(i,i^{\prime})}!}$
		$\displaystyle\prod_{i\in[p],i^{\prime}\in[\hat{u}]}W(C_{i},w,\overline{w})^{c_% {(i,i^{\prime})}}\cdot s_{i}^{\binom{c_{(i,i^{\prime})}}{2}}\prod_{\begin{% subarray}{c}i,j\in[p],i^{\prime},j^{\prime}\in[\hat{u}],\\ (i,i^{\prime})<(j,j^{\prime})\end{subarray}}\left(r_{(i,i^{\prime}),(j,j^{% \prime})}\right)^{c_{(i,i^{\prime})}c_{(j,j^{\prime})}},$

where $(i,i^{\prime})<(j,j^{\prime})$ means $i<j$ or $i=j\land i^{\prime}<j^{\prime}$ .

For simplicity, we use $\bm{c}$ to denote $(c_{1},c_{2},\dots,c_{p})$ . Then the new term $h_{\hat{u},\bm{c}}$ can be also computed by a DP algorithm:

\displaystyle h_{\hat{u},\bm{c}}=\sum_{\bm{\bar{c}}+\bm{c}^{*}=\bm{c}}

\displaystyle\binom{|\bm{c}|}{|\bm{c}^{*}|}\cdot h_{\hat{u}-1,\bm{\bar{c}}}% \cdot w_{in}(\bm{c}^{*})\cdot w_{cross}(\bm{\bar{c}},\bm{c}^{*}),

(5)

where recall that $\bm{\bar{c}}+\bm{c}^{*}=\bm{c}$ means that $\bar{c}_{i}+c^{*}_{i}=c_{i}$ for each $i\in[p]$ ,

w_{in}(\bm{c}^{*})=\binom{|\bm{c}^{*}|}{\bm{c}^{*}}\prod_{i=1}^{p}W(C_{i},w,% \overline{w})^{c_{i}^{*}}\cdot s_{i}^{\binom{c_{i}^{*}}{2}}\prod_{1\leq i<j% \leq p}\left(r_{i,j}\right)^{c_{i}^{*}c_{j}^{*}}

is the weight within layer $\hat{u}$ , and

w_{cross}(\bm{\bar{c}},\bm{c}^{*})=\prod_{i=1}^{p}\prod_{j=1}^{p}\left(r_{i,j}% ^{\not-}\right)^{\bar{c}_{i}c_{j}^{*}}

is the weight between the layer $\hat{u}$ and the layers before $\hat{u}$ . The initial values are $h_{0,\bm{c}}=w_{in}(\bm{c})$ for each $\bm{c}$ . Then the final WFOMC of $\Psi_{R,u}$ can be obtained by:

\mathsf{WFOMC}(\Psi_{R,u},n,w,\overline{w})=\sum_{|\bm{c}|=n}h_{u,\bm{c}}.

The new DP algorithm is summarized in Algorithm 1, where interpolate_1d( $\dots$ ) takes $n+1$ points as input and returns the corresponding polynomial of degree $n$ .

Algorithm 1 Computing the WCP.

Moreover, any WFOMC problem for $\text{C}^{2}$ sentences with cardinality constraints can be reduced to WFOMC of an $\text{FO}^{2}$ sentence, which can be solved in polynomial time in $n$ by the algorithm presented above. The interpolation step from $n+1$ point evaluations to the polynomial can also be done in polynomial time in $n$ , completing the proof. $\hfill\blacktriangleleft$

Proof of Theorem 16.

Consider a $\text{C}^{2}$ sentence $\Psi$ with cardinality constraints, a domain of size $n$ weighting functions $w,\overline{w}$ , and a distinguished binary predicate $R$ . We need another two predicates to represent the bipartite graph. Define

	$\displaystyle\Psi_{b}=$	$\displaystyle\Psi_{R}\land\forall x\ ((P_{1}(x)\lor P_{2}(x))\land(\lnot P_{1}% (x)\lor\lnot P_{2}(x)))$
		$\displaystyle\land\forall x\forall y\ \left(P_{1}(x)\land P_{1}(y)\lor P_{2}(x% )\land P_{2}(y)\to\lnot R(x,y)\right),$

where $w(P_{1})=\overline{w}(P_{1})=w(P_{2})=\overline{w}(P_{2})=1$ . The predicates $P_{1},P_{2}$ divide domain elements into two groups to ensure that $G(R)$ is a bipartite graph. However, overcounting occurs since for every connected component in the bipartite graph, we have two choices of assigning vertices to $P_{1}$ and $P_{2}$ . Hence, for each connected component, we need to multiply the WFOMC by a factor $\frac{1}{2}$ to its weight, which can be done using WCP:

	$\displaystyle\mathsf{WFOMC}(\Psi\land bipartite(R),n,w,\overline{w})$	$\displaystyle=\sum_{\mu\in\mathcal{M}_{\Psi_{b},n}}W(\mu,w,\overline{w})\cdot(% \frac{1}{2})^{cc(\mu_{R})}$
		$\displaystyle=f_{n}(-\frac{1}{2};\Psi_{b},w,\overline{w},R).\$

$\hfill\blacktriangleleft$

Proof of Theorem 19.

Consider a $\text{C}^{2}$ sentence $\Psi$ with cardinality constraints, a domain of size $n$ , weighting functions $w,\overline{w}$ and a distinguished binary predicate $R$ . By definition, the tree axiom requires that $G(R)$ should be connected and the number of edges in $G(R)$ should be $n-1$ . By Corollary 18, we have

\displaystyle\mathsf{WFOMC}(\Psi\land

\displaystyle tree(R),n,w,\overline{w})=[uv^{2(n-1)}]\hat{f}_{n}(u-1,v;\Psi_{R% },w,\overline{w},R).\

$\hfill\blacktriangleleft$

Proof of Theorem 20.

Consider a $\text{C}^{2}$ sentence $\Psi$ with cardinality constraints, a domain of size $n$ , weighting functions $w,\overline{w}$ and a distinguished binary predicate $R$ . By definition, the forest axiom requires the number of edges in $G(R)$ to be equal to the difference between the number of vertices in $G(R)$ and the number of connected components in $G(R)$ . By Corollary 18, we have

\displaystyle\mathsf{WFOMC}(

\displaystyle\Psi\land forest(R),n,w,\overline{w})=\sum_{i\in[n]}[u^{i}v^{2(n-% i)}]\hat{f}_{n}(u-1,v;\Psi_{R},w,\overline{w},R).\

$\hfill\blacktriangleleft$

[bib.bib1] [1] Jordan Awan and Olivier Bernardi. Tutte polynomials for directed graphs. Journal of Combinatorial Theory, Series B, 140:192–247, 2020. doi:10.1016/j.jctb.2019.05.006.

[bib.bib2] [2] Paul Beame, Guy Van den Broeck, Eric Gribkoff, and Dan Suciu. Symmetric weighted first-order model counting. In PODS, pages 313–328. ACM, 2015. doi:10.1145/2745754.2745760.

[bib.bib3] [3] Rodrigo de Salvo Braz, Eyal Amir, and Dan Roth. Lifted first-order probabilistic inference. In IJCAI, pages 1319–1325. Professional Book Center, 2005. URL: http://ijcai.org/Proceedings/05/Papers/1548.pdf.

[bib.bib4] [4] Reinhard Diestel, Alexander Schrijver, and Paul Seymour. Graph theory. Oberwolfach Reports, 4(2):887–944, 2008.

[bib.bib5] [5] Lise Getoor and Ben Taskar. Introduction to statistical relational learning, volume 1. MIT press Cambridge, 2007.

[bib.bib6] [6] Vibhav Gogate and Pedro M. Domingos. Probabilistic theorem proving. In UAI, pages 256–265. AUAI Press, 2011. URL: https://dslpitt.org/uai/displayArticleDetails.jsp?mmnu=1&smnu=2&article_id=2263&proceeding_id=27.

[bib.bib7] [7] Erich Grädel, Phokion G. Kolaitis, and Moshe Y. Vardi. On the decision problem for two-variable first-order logic. Bull. Symb. Log., 3(1):53–69, 1997. doi:10.2307/421196.

[bib.bib8] [8] Erich Grädel, Martin Otto, and Eric Rosen. Two-variable logic with counting is decidable. In LICS, pages 306–317. IEEE Computer Society, 1997. doi:10.1109/LICS.1997.614957.

[bib.bib9] [9] François Jaeger, Dirk L Vertigan, and Dominic JA Welsh. On the computational complexity of the jones and tutte polynomials. Mathematical Proceedings of the Cambridge Philosophical Society, 108(1):35–53, 1990.

[bib.bib10] [10] Seyed Mehran Kazemi, Angelika Kimmig, Guy Van den Broeck, and David Poole. New liftable classes for first-order probabilistic inference. In Advances in Neural Information Processing Systems 29: Annual Conference on Neural Information Processing Systems, pages 3117–3125, 2016. URL: https://proceedings.neurips.cc/paper/2016/hash/c88d8d0a6097754525e02c2246d8d27f-Abstract.html.

[bib.bib11] [11] Sandra Kiefer, Pascal Schweitzer, and Erkal Selman. Graphs identified by logics with counting. ACM Trans. Comput. Log., 23(1):1:1–1:31, 2022. doi:10.1145/3417515.

[bib.bib12] [12] Qipeng Kuang. l2l7l9p/Polynomials-for-WFOMC. Software, swhId: swh:1:dir:e82fa8e26998cfb9e25e723b2c1182f17a82276e (visited on 2026-02-02). URL: https://github.com/l2l7l9p/Polynomials-for-WFOMC, doi:10.4230/artifacts.25483.

[bib.bib13] [13] Antti Kuusisto and Carsten Lutz. Weighted model counting beyond two-variable logic. In LICS, pages 619–628. ACM, 2018. doi:10.1145/3209108.3209168.

[bib.bib14] [14] Ondrej Kuzelka. Weighted first-order model counting in the two-variable fragment with counting quantifiers. J. Artif. Intell. Res., 70:1281–1307, 2021. doi:10.1613/jair.1.12320.

[bib.bib15] [15] Michel Las Vergnas. Convexity in oriented matroids. J. Comb. Theory, Ser. B, 29(2):231–243, 1980. doi:10.1016/0095-8956(80)90082-9.

[bib.bib16] [16] Leonid Libkin. Elements of finite model theory, volume 41. Springer, 2004. doi:10.1007/978-3-662-07003-1.

[bib.bib17] [17] Sagar Malhotra, Davide Bizzaro, and Luciano Serafini. Lifted inference beyond first-order logic. Artif. Intell., 342:104310, 2025. doi:10.1016/j.artint.2025.104310.

[bib.bib18] [18] David Poole. First-order probabilistic inference. In IJCAI, pages 985–991. Morgan Kaufmann, 2003. URL: http://ijcai.org/Proceedings/03/Papers/142.pdf.

[bib.bib19] [19] Ronald C Read. An introduction to chromatic polynomials. Journal of combinatorial theory, 4(1):52–71, 1968.

[bib.bib20] [20] George Rebane and Judea Pearl. The recovery of causal poly-trees from statistical data. In UAI, pages 175–182. Elsevier, 1987. URL: https://dslpitt.org/uai/displayArticleDetails.jsp?mmnu=1&smnu=2&article_id=1813&proceeding_id=1003.

[bib.bib21] [21] Matthew Richardson and Pedro M. Domingos. Markov logic networks. Mach. Learn., 62(1-2):107–136, 2006. doi:10.1007/s10994-006-5833-1.

[bib.bib22] [22] Richard P Stanley. A chromatic-like polynomial for ordered sets. In Proc. Second Chapel Hill Conf. on Combinatorial Mathematics and its Applications (Univ. North Carolina, Chapel Hill, NC, 1970), Univ. North Carolina, Chapel Hill, NC, pages 421–427, 1970.

[bib.bib23] [23] Richard P Stanley. What is enumerative combinatorics? Springer, 1986.

[bib.bib24] [24] Jan Tóth and Ondřej Kuželka. Lifted inference with linear order axiom. In AAAI, pages 12295–12304. AAAI Press, 2023. doi:10.1609/aaai.v37i10.26449.

[bib.bib25] [25] William Thomas Tutte. A contribution to the theory of chromatic polynomials. Canadian journal of mathematics, 6:80–91, 1954.

[bib.bib26] [26] WT Tutte. Graph-polynomials. Advances in Applied Mathematics, 32(1-2):5–9, 2004. doi:10.1016/S0196-8858(03)00041-1.

[bib.bib27] [27] Timothy van Bremen and Ondrej Kuzelka. Faster lifting for two-variable logic using cell graphs. In UAI, volume 161 of Proceedings of Machine Learning Research, pages 1393–1402. AUAI Press, 2021. URL: https://proceedings.mlr.press/v161/bremen21a.html.

[bib.bib28] [28] Timothy van Bremen and Ondrej Kuzelka. Lifted inference with tree axioms. Artif. Intell., 324:103997, 2023. doi:10.1016/j.artint.2023.103997.

[bib.bib29] [29] Guy Van den Broeck. On the completeness of first-order knowledge compilation for lifted probabilistic inference. In NIPS, pages 1386–1394, 2011. URL: https://proceedings.neurips.cc/paper/2011/hash/846c260d715e5b854ffad5f70a516c88-Abstract.html.

[bib.bib30] [30] Guy Van den Broeck and Jesse Davis. Conditioning in first-order knowledge compilation and lifted probabilistic inference. In AAAI, pages 1961–1967. AAAI Press, 2012. doi:10.1609/aaai.v26i1.8404.

[bib.bib31] [31] Guy Van den Broeck, Wannes Meert, and Adnan Darwiche. Skolemization for weighted first-order model counting. In KR. AAAI Press, 2014. URL: http://www.aaai.org/ocs/index.php/KR/KR14/paper/view/8012.

[bib.bib32] [32] Moshe Y. Vardi. The complexity of relational query languages (extended abstract). In STOC, pages 137–146. ACM, 1982. doi:10.1145/800070.802186.

[bib.bib33] [33] Yuanhong Wang, Juhua Pu, Yuyi Wang, and Ondrej Kuzelka. On exact sampling in the two-variable fragment of first-order logic. In LICS, pages 1–13. IEEE, 2023. doi:10.1109/LICS56636.2023.10175742.

[bib.bib34] [34] Yuanhong Wang, Juhua Pu, Yuyi Wang, and Ondrej Kuzelka. Lifted algorithms for symmetric weighted first-order model sampling. Artif. Intell., 331:104114, 2024. doi:10.1016/j.artint.2024.104114.

Bridging Weighted First Order Model Counting and Graph Polynomials

Abstract

Keywords and phrases:

Funding:

Copyright and License:

2012 ACM Subject Classification:

Related Version:

Supplementary Material:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

1.1 Our Contribution

Theorem 1.

Theorem 2.

1.2 Related Work

2 Preliminaries

2.1 First-Order Logic

2.2 Weighted First Order Model Counting

Definition 3 (Weighted First Order Model Counting).

Example 4.

2.3 Data Complexity of WFOMC

Definition 5 (Domain-liftability [29]).

Definition 6 (Counting quantifiers).

Definition 7 (Cardinality constraints).

Example 8.

▶ Remark 9.

▶ Remark 10.

2.4 Axioms

3 Weak Connectedness Polynomial

3.1 Definition

Definition 11 (Weak Connectedness Polynomial).

Proposition 12.

Proof.

Proposition 13.

Proof.

3.2 Fast Calculation

Proposition 14.

3.3 Applications

3.3.1 Axioms: Existing, Generalized, and New

𝒌-connected-component axiom.

Theorem 15.

Proof.

Bipartite axiom.

Theorem 16.

Tree and forest axioms.

Definition 17.

Corollary 18 (Corollary from Propositions 12 and 14).

Theorem 19.

Theorem 20.

▶ Remark 21.

Example 22.

3.3.2 From WCP to Tutte Polynomial

Theorem 23.

Proof.

Example 24.

Example 25.

4 Strong Connectedness Polynomials

4.1 Definition

Definition 26 (Strong Connectedness Polynomials).

Proposition 27.

Proposition 28.

4.2 Fast Calculation

Proposition 29.

Proposition 30.

4.3 Applications

Strong connectedness axiom.

Theorem 31.

Example 32.

Acyclicity axiom.

Theorem 33.

Directed tree and forest axioms.

Theorem 34.

Linear order axiom.

Theorem 35.

▶ Remark 36.

From SSCP and NSCP to Directed Chromatic Polynomials.

Corollary 37 (Corollary from Theorem 23).

5 Combinations of Axioms

$\blacktriangleright$ Remark 9.

$\blacktriangleright$ Remark 10.

$𝒌$ -connected-component axiom.

$\blacktriangleright$ Remark 21.

$\blacktriangleright$ Remark 36.

Appendix A Domain-Liftability of $\text{FO}^{2}$