# Weighted First Order Model Counting with Directed Acyclic Graph Axioms

Sagar Malhotra Fondazione Bruno Kessler, Italy  University of Trento
Italy  Luciano Serafini  Fondazione Bruno Kessler, Italy

###### Abstract

Weighted First Order Model Counting (WFOMC) is the task of computing the
weighted sum of the models of a first-order logic sentence. Probabilistic
inference problems in many statistical relational learning frameworks can be
cast as a WFOMC problem. However, in general, WFOMC is known to be intractable
($\mathrm{\\#P_{1}-}$ complete). Hence, logical fragments that admit
polynomial time WFOMC are of significant interest. Such fragments are called
_domain liftable_. Recent line of works have identified the two-variable
fragment of first-order logic, extended with counting quantifiers, to be
domain liftable. In this paper, we extend this fragment with a _Directed
Acyclic Graph_ axiom, i.e. a relation in the language is acyclic.

##  1 Introduction

_Weighted First Order Model Counting_ (WFOMC) is the task of computing the
weighted sum of the models of a given First Order Logic (FOL) sentence $\Phi$
over a given finite domain of size $n$. Formally,

$\mbox{\sc wfomc}(\Phi,\mbox{\sc w},n)=\sum_{\omega\models\Phi}\mbox{\sc
w}(\omega)$ (1)

where w is a _weight function_ that associates a real number to each
interpretation $\omega$. Applications to Statistical Relational Learning (SRL)
Getoor and Taskar [2007], Raedt et al. [2016] are the key drivers of research
in WFOMC, as probabilsitic inference in popular SRL models like Markov logic
networks Richardson and Domingos [2006] and Probabilsitic Logic Programs
firens et al. [2015] can be reduced to WFOMC. However, WFOMC is
$\\#P_{1}$-complete in general Beame et al. [2015], making tractable fragments
of FOL a significant area of theoretical and practical interest.

Besides its application to SRL, WFOMC is also a convinient language for
investigating enumerative combinatorics, as any FOL definable concept can be
enumerated using WFOMC. Works like Kuusisto and Lutz [2018], Malhotra and
Serafini [2022] have expanded WFOMC formalism for different logical fragments
to admit analytical combinatorial formulae. Furthermore, WFOMC has also been
used for automatic conjecturing of combinatorial formulae Barvínek et al.
[2022]. Hence, domain-liftable fragments of FOL are of significant practical
and theoretical interest.

Fragments of FOL that admit polynomial time WFOMC with respect to domain
cardinality are called _domain-liftable_ or are said to admit _lifted
inference_ Van den Broeck et al. [2011]. A series of results have demonstrated
domain-liftability of the two-variable fragment of FOL Beame et al. [2015],
Van den Broeck et al. [2014] and its extensions with _functionality
constraint_ Kuusisto and Lutz [2018], _cardinality constraints_ , _counting
quantifiers_ Kuželka [2021] and _linear order axiom_ Tóth and Kuželka [2022].
Furthermore, recent results Van Bremen and Kuželka [2021] have expanded
domain-liftability to a constraints that is not definable in an FOL language,
namely a _tree axiom_.

Our paper extends previous research by exploring the domain-liftability of the
two-variable fragment with an additional constraint that cannot be expressed
in FOL, namely a _Directed Acyclic Graph_ (DAG) axiom. A DAG axiom enforces a
selected relation in an FOL sentence to be acyclic. We show that WFOMC in C2
expanded with a DAG axiom is domain liftable, allowing us to efficiently
answer questions like:

How many DAGs with exactly (or atleast or atmost) $k$ sources and exactly $m$
(or atleast or atmost) sinks exist ?

Given the vastness of DAG applications, these results can allow modelling of
many real-world scenarios in models like Markov Logic Networks e.g. citation
networks Clough et al. [2014]. Furthermore, since counting DAGs have become an
important tool for learning Bayesian Networks and causal inference Steinsky
[2003], Ganian et al. [2022], our results could potentially be exploited in
these domains as well.

##  2 Background

This section overviews basic notation and aspects of FOL and WFOMC. We also
revisit existing works — with emphasis on relevance to our results — on WFOMC
in FO2 and C2, and some combinatorial background on the principle of
inclusion-exclusion and counting DAGs.

###  2.1 Basic Definitions.

We use $[n]$ to denote the set of integers $\\{1,\dots,n\\}$. Whenever the set
of integers $[n]$ is obvious from the context we will use $[\overline{m}]$ to
represent the set $[n]\backslash[m]$, i.e. the set $\\{m+1,\dots,n\\}$. We use
bold font letters (e.g. ${\bm{k}}$) to denote vectors, and corresponding
regular font letters (with an aditional index) for the components of the
vectors (e.g. $k_{i}$). Hence, we use $\bm{k}=\langle k_{1},...,k_{u}\rangle$
to denote a vector of $u$ non-negative integers and $|{\bm{k}}|$ to denote
$\sum_{i\in[u]}k_{i}$, i.e., the sum of its components. We will also use the
multinomial coefficients denoted by

$\binom{|{\bm{k}}|}{k_{1},...,k_{u}}=\binom{|{\bm{k}}|}{{\bm{k}}}=\frac{|{\bm{k}}|!}{\prod_{i\in[u]}k_{i}!}$

A summation of the form $\sum_{\bm{k}}f(\bm{k})$, where $f(\bm{k})$ is an
arbitrary function on $\bm{k}$, runs over all possible $\bm{k}$ such that
$\sum_{i\in[u]}k_{i}=|{\bm{k}}|$. When summing (or subtracting) two vectors
${\bm{k}}^{\prime}=\langle k^{\prime}_{1},...,k^{\prime}_{u}\rangle$ and
${\bm{k}}^{\prime\prime}=\langle
k^{\prime\prime}_{1},...,k^{\prime\prime}_{u}\rangle$, we always intend
element wise sum (or subtraction) i.e.
${\bm{k}}^{\prime}+{\bm{k}}^{\prime\prime}=\langle
k^{\prime}_{1}+k^{\prime\prime}_{1},...,k^{\prime}_{u}+k^{\prime\prime}_{u}\rangle$.

###  2.2 First Order Logic

We assume a function-free FOL language $\mathcal{L}$ defined by a set of
variables $\mathcal{V}$ and a set of relational symbols $\mathcal{R}$. We
write $R/k$ to denote that the relational symbol $R$ has arity $k$. For
$(x_{1},...,x_{k})\in\mathcal{V}^{k}$ and $R/k\in\mathcal{R}$, we call
$R(x_{1},...,x_{k})$ an _atom_. A _literal_ is an atom or the negation of an
atom. A _formula_ is formed by connecting atoms with boolean operators
($\neg,\lor$ and $\land$) and quantifiers of the form $\exists x_{i}.$
(existential quantification) and $\forall x_{i}.$ (universal quantification).
The _free_ variables of a formula are those that are not bound by a
quantifier. We write $\Phi(x_{1},\dots x_{k})$ to denote a formula whose free
variables are $\\{x_{1},\dots,x_{k}\\}$. An FOL formula with no free-variables
is called a _sentence_. Hence, a sentence is denoted by a capital greek letter
(e.g. $\Psi$). Given a finite set of constants $\Delta$ called the _domain_.
The set of ground atoms (resp. ground literals) is obtained by replacing all
the variables in the atoms (resp. literals) of $\mathcal{L}$. Hence, given a
predicate $R/k$, and a domain $\Delta$ of size $n$, we have $n^{k}$ ground
atoms of the form $R(a_{1},\dots,a_{k})$, where $(a_{1}\dots
a_{k})\in\Delta^{k}$. An _interpretation_ $\omega$, on a finite _domain_
$\Delta$, is a truth assignment to all the ground atoms. We say $\omega$ is an
interpretation or a model of $\Psi$ if $\omega\models\Psi$, i.e. $\omega$
satisfies the formula $\Psi$. Given a literal (resp. ground literal) $l$, we
use the $pred(l)$ to denote the relational symbol in $l$. We use $\omega_{R}$
to represent the partial interpretation of $\omega$ restricted to the relation
$R$. For a subset $\mathrm{\Delta^{\prime}}\subset\Delta$, we use
$\omega\downarrow\mathrm{\Delta^{\prime}}$ to denote the partial
interpretation induced by $\mathrm{\Delta^{\prime}}$. Hence,
$\omega\downarrow\mathrm{\Delta^{\prime}}$ is an interpretation over the
ground atoms containing only the domain elements in
$\mathrm{\Delta^{\prime}}$.

######  Example 1.

Let us have a language with only one relational symbol $R$ of arity $2$ and a
domain $\Delta=[4]$. We represent an interpretation $\omega$ as a directed
graph, where a pair of domain elements $c$ and $d$ have a directed edge from
$c$ to $d$ if $R(c,d)$ is true in $\omega$ and have no edge otherwise. Let us
take for example the following interpretation:

$1$$2$$3$$4$

then $\omega\downarrow[3]$ is given as:

$1$$2$$3$

We use $\Delta=\Delta^{\prime}\uplus\Delta^{\prime\prime}$ to denote that
$\Delta$ is a union of two disjoint sets $\Delta^{\prime}$ and
$\Delta^{\prime\prime}$. If $\omega^{\prime}$ is an interpretation on
$\Delta^{\prime}$ and $\omega^{\prime\prime}$ is an interpretation on
$\Delta^{\prime\prime}$, then we use
$\omega^{\prime}\uplus\omega^{\prime\prime}$ to denote the parital
interpretation on $\Delta^{\prime}\uplus\Delta^{\prime\prime}$, obtained by
interpreting ground atoms over $\Delta^{\prime}$ as interpreted in
$\omega^{\prime}$ and ground atoms over $\Delta^{\prime\prime}$ as interpreted
in $\omega^{\prime\prime}$. However, notice that ground atoms involving domain
constants from both $\Delta^{\prime}$ and $\Delta^{\prime\prime}$ are left un-
interpreted in $\omega^{\prime}\uplus\omega^{\prime\prime}$.

####  2.2.1 Counting Quantifiers, Cardinality Constraints, Types and, Tables

FO2 is the fragment of FOL with only two variables. An extension of FO2 is
obtained by introducing _counting quantifires_ of the form $\exists^{=k}$
(there exist exactly $k$), $\exists^{\geq k}$ (there exist at least $k$) and
$\exists^{\leq k}$ (there exist at most $k$), this extended fragment is
denoted by C2 Gradel et al. [1997]. Cardinality constraints are constraints on
the cardinality of predicates in an interpretation Kuželka [2021]. For
example, given a formula $\Phi\land(|R|+|P|\geq 5)$, then an interpretation
$\omega\models\Phi\land(|R|+|P|\geq 5)$ if and only if $\omega\models\Phi$ and
the sum of the ground atoms in $\omega$, with predicate $R$ or predicate $P$,
that are interpated to be true, is atleast $5$.

We will use the notion of $1$-types, $2$-type, and $2$-tables as presented in
Kuusisto and Lutz [2018]. A $1$-type is a conjunction of maximally consistent
literals containing only one variable. For example, in an FO2 language with
only a unary predicate $U$ and a binary predicate $R$, ${U(x)\land R(x,x)}$
and ${U(x)\land\neg R(x,x)}$ are examples of 1-types in variable $x$. A
2-table is a conjunction of maximally consistent literals containing exactly
two distinct variables. Extending the previous example, ${R(x,y)\land\neg
R(y,x)\land(x\neq y)}$ and ${R(x,y)\land R(y,x)\land(x\neq y)}$ are instances
of 2-tables. We assume an arbitrary order on the 1-types and 2-tables, hence,
we use ${i(x)}$ to denote the $i^{th}$ 1-type and ${l(x,y)}$ to denote the
$l^{th}$ 2-table. A $2$-type is a quantifier-free formula of the form
${i(x)\land j(y)\land l(x,y)\land(x\neq y)}$ and we use ${ijl(x,y)}$ to
represent it. In a given interpretation $\omega$, we say a domain constant $c$
realizes the $i^{th}$ 1-type if ${\omega\models i(c)}$, we say a pair of
domain constants $(c,d)$ realizes the $l^{th}$ 2-table if ${\omega\models
l(c,d)}$ and, we say $(c,d)$ realizes the 2-type ${ijl(x,y)}$ if
${\omega\models ijl(c,d)}$. We will use $u$ to denote the number of 1-types
and $b$ to denote the number of 2-tables in a given FO2 (or a C2) language.

######  Definition 1 (1-type Cardinality Vector).

An interpretation $\omega$ is said to have the 1-type cardinality vector
${\bm{k}}=\langle k_{1},\dots,k_{u}\rangle$ if and only if, for all $i\in[u]$,
it has $k_{i}$ domain elements $c$ such that $\omega\models i(c)$, where
$i(x)$ is the $i^{th}$ 1-type. If $\omega$ has 1-type cardinality vector
${\bm{k}}$, then we say that $\omega\models{\bm{k}}$.

Notice that in a given interpretation $\omega$ each domain element realizes
exactly one 1-type. Hence, given a 1-type cardinality vector ${\bm{k}}$,
$|{\bm{k}}|$ is equal to the domain cardinality. Furthermore, for a given
${\bm{k}}$ and a fixed pair of 1-types $i$ and $j$, such that $i\neq j$, there
are $k_{i}k_{j}$ pairs domain constants $(c,d)$ such that $\omega\models
i(c)\land j(d)$. For a given ${\bm{k}}$ and a 1-type $i$ there are
$\binom{k_{i}}{2}$ pair of domain constants $(c,d)$, such that $\omega\models
i(c)\land i(d)$.

###  2.3 WFOMC

In WFOMC as defined in equation 1, we assume that the weight function $w$ does
not depend on individual domain constants, which implies that $w$ assigns same
weight to two interpretations which are isomorphic under the permutation of
domain elements. Hence, for a domain $\Delta$ of size $n$, we can equivalently
use $[n]$ as our domain. Furthermore, in this paper we will focus on a special
class of weight functions namely _symmetric weight functions_ defined as
follows:

######  Definition 2.

(Symmetric Weight Function) Given a function-free first order logic language
$\mathcal{L}$ over a domain $\Delta$, where $\mathcal{G}$ are the set of
ground atoms. A symmetric weight function associates two real-valued weights
$w:\mathcal{R}\rightarrow\mathbb{R}$ and
$\bar{w}:\mathcal{R}\rightarrow\mathbb{R}$ to each relational symbol in
$\mathcal{L}$. The weight of an interpretation $\omega$ is then defined as:

$\mbox{\sc w}(\omega)=\prod_{\begin{subarray}{c}\omega\models g\\\
g\in\mathcal{G}\\\
\end{subarray}}w(pred(g))\prod_{\begin{subarray}{c}\omega\models\neg g\\\
g\in\mathcal{G}\end{subarray}}\bar{w}(pred(g)).$ (2)

We use $(w,\bar{w})$ to denote a symmeteric weight function.

We will also need to invoke modularity of WFOMC-preserving reductions.

######  Definition 3 (Van den Broeck et al. [2014]).

A reduction $(\Phi,w,\bar{w})$ to
$(\Phi^{\prime},w^{\prime},\bar{w}^{\prime})$ is modular iff for any sentence
$\Lambda$:

$\mbox{\sc wfomc}(\Phi\land\Lambda,(w,\bar{w}),n)=\mbox{\sc
wfomc}(\Phi^{\prime}\land\Lambda,(w^{\prime},\bar{w}^{\prime}),n)$

Intuitively, modularity implies that the reduction procedure is sound under
presence of other sentences $\Lambda$. And that any new sentence $\Lambda$
does not invalidate the reduction.

For the rest of the paper, whenever referring to weights, we intend symmetric
weights. Hence, we will use $\mbox{\sc wfomc}(\Phi,n)$ without explicitly
mentioning the weights $w$ and $\bar{w}$. We also define $\mbox{\sc
wfomc}(\Phi,{\bm{k}})$ as follows:

$\displaystyle\mbox{\sc
wfomc}(\Phi,{\bm{k}}):=\sum_{\omega\models\Phi\land{\bm{k}}}\mbox{\sc
w}(\omega)$

where $\mbox{\sc w}(\omega)$ is the symmetric weight function.

####  2.3.1 WFOMC in FO2.

Universally quantified FO2 formulas are formulas of the form $\forall
xy.\Phi(x,y)$, where $\Phi(x,y)$ is quantifier-free. We define
$\Phi(\\{x,y\\})$ as
$\Phi(x,x)\land\Phi(x,y)\land\Phi(y,x)\land\Phi(y,y)\land(x\neq y)$. Given a
quantifier-free formula of the form $\Phi(x,y)$, we say the 2-type $ijl(x,y)$
is consistent with $\forall xy.\Phi(x,y)$ if $ijl(x,y)\models\Phi(\\{x,y\\})$,
where we consider atoms in $ijl(x,y)$ and $\Phi(\\{x,y\\})$ as propositional
variables and check entailment using proposition semantics.

One of the key ideas in analysing domain-liftability of universally quantified
FO2 formula is that a pair of domain constants $(c,d)$ in an interpretation
$\omega\models\forall xy.\Phi(x,y)$ can realize a 2-type $ijl(c,d)$ only if
the 2-type is consistent with the formula $\forall xy.\Phi(x,y)$ i.e. only if
$ijl(x,y)\models\Phi(\\{x,y\\})$. We formalize this intuition in the following
proposition.

######  Proposition 1.

Given a universally quantified FO2 formula, $\forall xy.\Phi(x,y)$ interpreted
over a domain $\Delta$. Then $\omega\models\forall xy.\Phi(x,y)$ iff for any
pair of distinct domain constants $(c,d)$ such that $\omega\models ijl(c,d)$,
we have that $ijl(x,y)$ is consistent with $\Phi(\\{x,y\\})$, i.e.
$ijl(x,y)\models\Phi(\\{x,y\\})$.

###### Proof.

If $\omega\models\forall xy.\Phi(x,y)$ and $\omega\models ijl(c,d)$, then
$\omega\models\forall xy.\Phi(x,y)\land ijl(c,d)$. Now, $ijl(c,d)$ is a
complete truth assignment to the ground atoms containing only the domain
constants $c$ or $d$ or both. Hence, $\omega\models\forall xy.\Phi(x,y)\land
ijl(c,d)$ only if $ijl(c,d)\models\Phi(\\{c,d\\})$ i.e. only if
${ijl(x,y)\models\Phi(\\{x,y\\})}$.

If in $\omega$ all pair of domain constants realize only the 2-types
$ijl(x,y)$ consistent with $\forall xy.\Phi(x,y)$. Then
$\omega\models\Phi(\\{c,d\\})$, for all pair of domain constants $(c,d)$.
Hence, $\omega\models\forall xy.\Phi(x,y)$.

∎

We will now define some weight parameters associated with an FOL language.
These parameters will be useful for treating WFOMC. Given an FO2 language
$\mathcal{L}$ and symmetric weight functions $(w,\bar{w})$, let $\mathcal{I}$
denotes the set of atoms in $\mathcal{L}$ containing only variables, i.e. not
grounded. We then define the following two parameters for each 1-type $i(x)$
and 2-table $l(x,y)$:

$w_{i}=\prod_{\begin{subarray}{c}i(x)\models g\\\
g\in\mathcal{I}\end{subarray}}w(pred(g))\prod_{\begin{subarray}{c}i(x)\models\neg
g\\\ g\in\mathcal{I}\end{subarray}}\bar{w}(pred(g))$

and

$v_{l}=\prod_{\begin{subarray}{c}l(x,y)\models g\\\
g\in\mathcal{I}\end{subarray}}w(pred(g))\prod_{\begin{subarray}{c}l(x,y)\models\neg
g\\\ g\in\mathcal{I}\end{subarray}}\bar{w}(pred(g))$

We will now present a slightly reformulated version of WFOMC for univerally
quantified FO2 formulas, as presented in Beame et al. [2015].

######  Theorem 1 (Beame et al. [2015]).

Given a universally quantified FO2 formula $\forall xy.\Phi(x,y)$, interpreted
over a domain $[n]$, then the weighted model count of the models $\omega$ such
that $\omega\models\forall xy.\Phi(x,y)$ and $\omega$ has the 1-type
cardinality ${\bm{k}}$ is given as:

$\displaystyle\mbox{\sc wfomc}(\forall
xy.\Phi(x,y),{\bm{k}})=\binom{n}{\bm{k}}\prod_{i\in[u]}w_{i}^{k_{i}}\prod_{\begin{subarray}{c}{i\leq
j\in[u]}\end{subarray}}\\!\\!\\!r_{ij}^{{\bm{k}}(i,j)}$ (3)

where ${\bm{k}}(i,j)$ is defined as follows:

$\displaystyle{\bm{k}}(i,j)=\begin{cases}\frac{k_{i}(k_{i}-1)}{2}&\text{if
$i=j$}\\\ k_{i}k_{j}&\text{otherwise}\\\ \end{cases}$

where we define $r_{ij}=\sum_{l\in[b]}n_{ijl}v_{l}$, where $n_{ijl}$ is $1$ if
$ijl(x,y)\models\Phi(\\{x,y\\})$ and $0$ otherwise.

###### Proof.

In a given 1-type cardinality vector ${\bm{k}}$, $k_{i}$ represents the number
of constants $c$ of 1-type $i$. Also a given constant realizes exactly one
1-type. Hence, for a given ${\bm{k}}$, we have $\binom{n}{{\bm{k}}}$ possible
ways of realizing 1-types. A domain constant $c$ realizing the $i^{th}$ 1-type
contributes a weight of $w_{i}$ multiplicatively to weight of $\omega$. Hence,
for a given ${\bm{k}}$, the contribution due to 1-type realizations is
$\prod_{i\in[u]}w_{i}^{k_{i}}$. Furthermore, in an interpretation
$\omega\models\forall xy.\Phi(x,y)$, given a pair of constants $c$ and $d$
such that $c$ is of 1-type $i$ and $d$ is of 1-type $j$, using Proposition 1,
we have that $(c,d)$ can realize the 2-table $l(c,d)$, only if
$ijl(x,y)\models\Phi({x,y})$. Hence, in an arbitrary interpretation, the
multiplicative weight contribution due to $l(x,y)$ realization is given by
$n_{ijl}v_{l}$. Also, each ordered pair of constants can realize exactly one
and only one 2-table. Hence, the possible 2-table realization contributes a
weight $r_{ij}=\sum_{l}n_{ijl}v_{l}$. Furthermore, given 1-type assignments to
$i(c)$ and $j(d)$, the ordered pair $(c,d)$ can realize 2-table independently
of all other domain constants. Finally, There are ${\bm{k}}(i,j)$ possible
such pairs, contributing a weight

$\prod_{\begin{subarray}{c}{i\leq
j\in[u]}\end{subarray}}\\!\\!\\!r_{ij}^{{\bm{k}}(i,j)}$

∎

Clearly, equation (3) can be computed in polynomial time w.r.t domain
cardinality. Furthermore, there are only polynomially many ${\bm{k}}$, in the
size of the domain. Hence, $\mbox{\sc wfomc}(\forall xy.\Phi(x,y),n)$ given
as:

$\sum_{|{\bm{k}}|=n}\mbox{\sc wfomc}(\forall xy.\Phi(x,y),{\bm{k}})$

can be computed in polynomial time w.r.t domain size $n$.

Van den Broeck et al. [2014] show that any FOL formula with existential
quantification can be modularly reduced to a WFOMC preserving universally
quantified FO2 formula, with additional new predicates and negative weights.
Hence, showing that FO2 is domain-liftable.

####  2.3.2 WFOMC in C2

Kuželka [2021] show that WFOMC in C2 can be reduced to WFOMC in FO2 with
cardinality constraints. Furthermore, these reductions are independent of the
domain cardinality. In order to prove domain liftability, the proof in Kuželka
[2021], relies on Lagrange interpolation. In the following we provide an
easier presentation of the proof.

######  Theorem 2 (Kuželka [2021], slightly reformulated).

Let $\Phi$ be a first-order logic sentence. Let $\Gamma$ be a arbitrary
cardinality constraint. Then $\mbox{\sc wfomc}(\Phi\land\Gamma,{\bm{k}})$ can
be computed in polynomial time with respect to the domain cardinality,
relative to the $\mbox{\sc wfomc}(\Phi,{\bm{k}})$ oracle.

###### Proof.

We assume an FOL language $\mathcal{L}$, with $r$ relational symbols
$\\{R_{i}/a_{i}\\}_{i\in[r]}$. Given an interpretation $\omega$, let
$\bm{\mu}=\langle|R_{1}|\dots|R_{r}|\rangle$ be the vector containing
cardinality of each predicate $R_{i}$ in $\omega$. Now, $\mbox{\sc w}(\omega)$
can be easily evaluated using the definition of symmetric weight functions
(Definition 2). Furthermore, any two interpretations with same predicate
cardinalities $\bm{\mu}$ as $\omega$, have the same weight $\mbox{\sc
w}(\omega)$. Hence, we use $\mbox{\sc w}_{\bm{\mu}}$ to denote the weight
$\mbox{\sc w}(\omega)$.

Given an FOL formula $\Phi$, let $A_{\bm{\mu}}$ be the number of models
$\omega\models\Phi\land\bm{\mu}$. Clearly, the following holds:

$\mbox{\sc wfomc}(\Phi,{\bm{k}})=\sum_{\bm{\mu}}A_{\mu}\mbox{\sc
w}_{\bm{\mu}}$ (4)

Each predicate $R_{i}/a_{i}$ can be grounded to $n^{a_{i}}$ ground atoms.
Hence, there are $n^{\sum_{i\in[r]}a_{i}}$ possible values of $\bm{\mu}$,
which are polynomial in $n$. Hence, if we evaluate $\mbox{\sc
wfomc}(\Phi,{\bm{k}})$ for $n^{\sum_{i\in[r]}a_{i}}$ different values of
weight functions $(w,\bar{w})$, then we have a linear system of
$n^{\sum_{i\in[r]}a_{i}}$ equations with $n^{\sum_{i\in[r]}a_{i}}$ variables
(variables being $A_{\mu}$), which can be solved in
$O(n^{3\sum_{i\in[r]}a_{i}})$ time, using Gauss-elimination. Once we have all
the $A_{\bm{\mu}}$, we can evaluate any cardinality constraint as follows:

$\mbox{\sc
wfomc}(\Phi\land\Gamma,{\bm{k}})=\sum_{\bm{\mu\models\Gamma}}A_{\mu}\mbox{\sc
w}_{\bm{\mu}}$ (5)

where $\bm{\mu\models\Gamma}$ represents the fact that the predicate
cardinalities $\bm{\mu}$, satisfy the cardinality constraint $\Gamma$. Since,
there area only polynomially many $\bm{\mu}$, equation (5) can be computed in
polynomial time. ∎

######  Remark 1.

In equation (5), we assume that $\bm{\mu}\models\Gamma$ can be checked in
polynomial time wrt $n$. Which is a reasonable assumption for all our
purposes.

######  Remark 2.

In the proof presented above (and in Kuželka [2021]), the first-order
definability of $\Phi$ is never invoked. This property has also been exploited
for imposing cardinality constraints with tree axiom in Van Bremen and Kuželka
[2021].

Theorem 2 extends domain-liftability of any sentence $\Phi$ to its domain
liftability with cardinality constraints. We now move onto the results on
domain-liftability of C2.

######  Theorem 3 (Kuželka [2021]).

The fragment of first-order logic with two variables and counting quantifiers
is domain-liftable.

The key idea behind Theorem 3 is that WFOMC of a C2 sentence $\Phi$ can be
converted to a problem of WFOMC of an FO2 sentence $\Phi^{\prime}$ with
cardinality constraints $\Gamma$ on an extended vocabulary with additional
weights for the new predicates (the new predicates are weighted 1 or -1). We
refer the reader to Kuželka [2021] and Malhotra and Serafini [2022] for the
detailed treatment of Theorem 3. However, for our purposes it is important to
note that this transformation is modular. The modularity of the WFOMC
procedure as presented in Kuželka [2021], has also been exploited to
demonstrate domain-liftability of C2 extended with Tree axiom Van Bremen and
Kuželka [2021] and Linear Order axiom Tóth and Kuželka [2022].

###  2.4 Principle of Inclusion-Exclusion

Given a set of finite sets $\\{A_{i}\\}_{i\in[n]}$, let $A_{J}:=\bigcap_{j\in
J}A_{j}$ for an arbitrary subset $J$ of $[n]$. Then the principle of
inclusion-exclusion (PIE) states that:

$\Big{|}\bigcup_{i}A_{i}\Big{|}=\sum_{\emptyset\neq
J\subseteq[n]}(-1)^{|J|+1}\big{|}A_{J}\big{|}$ (6)

For all subsets $J,J^{\prime}\subseteq[n]$, such that $|J|=|J^{\prime}|=m$ for
some $m\geq 1$, if $A_{J}$ and $A_{J^{\prime}}$ have the same cardinality,
then there are $\binom{n}{m}$ terms in equation (6), with value $A_{[m]}$.
Hence, equation (6) reduces to:

$\Big{|}\bigcup_{i}A_{i}\Big{|}=\sum_{m=1}^{n}(-1)^{m+1}\binom{n}{m}A_{[m]}$
(7)

######  Remark 3.

PIE can be easily extended to the case when $A_{i}$ are sets of weighted FOL
interpretations, where each interpretation $\omega$ has a weight $\mbox{\sc
w}(\omega)$, where w is the symmetric weight function as given in Definition
2. In this case PIE allows us to computed the weighted sum of all the
interpretations in $\bigcup_{i}A_{i}$.

Let $\mbox{\sc w}(A_{i})$ denote the weighted sum of all the interpretations
in $A_{i}$, Then the PIE reduces to:

$\mbox{\sc w}\Big{(}\bigcup_{i}A_{i}\Big{)}=\sum_{\emptyset\neq
J\subseteq[n]}(-1)^{|J|+1}\mbox{\sc w}(A_{J})$ (8)

Similarly, when $\mbox{\sc w}(A_{J})$ and $\mbox{\sc w}(A_{J^{\prime}})$ are
the same for each $m=|J|=|J^{\prime}|$, we have that:

$\mbox{\sc
w}\Big{(}\bigcup_{i}A_{i}\Big{)}=\sum_{m=1}^{n}(-1)^{m+1}\binom{n}{m}\mbox{\sc
w}(A_{[m]})$ (9)

###  2.5 Counting Directed Acyclic Graphs

A _Directed Acyclic Graph (DAG)_ is a directed graph such that starting from
an arbitrary node $i$ and traversing an arbitrary path along directed edges,
we would never arrive at node $i$. We now present the derivation of a
recursive formula for counting the number of DAGs.

Let the nodes be the set $[n]$ and let $A_{i}$ be the set of DAGs on $[n]$
where node $i$ has indegree zero. Since every DAG has at least one node with
in-degree zero, we have that the total number of DAGs i.e. $a_{n}$ is given as
$|\bigcup_{i\in[n]}A_{i}|$. The number of DAGs such that all nodes in
$J\subseteq[n]$ have in-degree zero is then given as $A_{J}:=\bigcap_{j\in
J}A_{j}$. Let us assume that $J=[m]$ for some $1\leq m\leq n$. We now derive a
method for computing $A_{[m]}$. We make the following three observations for
deriving the formula for counting the DAGs in $A_{[m]}$.

  * •

Observation 1. If $\omega\in A_{[m]}$, then there are no edges between the
nodes in $[m]$, as otherwise a node in $[m]$ will have a non-zero in-degree.
In other words, only directed edges from $[m]$ to $[\bar{m}]$ are allowed.

  * •

Observation 2. If $\omega\in A_{[m]}$, then subgraph of $\omega$ restricted to
$[\bar{m}]$ i.e. $\omega\downarrow[\bar{m}]$ is a DAG. And the subgraph of
$\omega$ restricted to $[m]$ is just an empty graph, i.e., the set of isolated
nodes $[m]$ with no edges between them.

  * •

Observation 3. Given a DAG on $[\bar{m}]$, then it can be extended to
$2^{m(n-m)}$ DAGs in $A_{[m]}$. This is because DAGs in $A_{[m]}$ have no
edges between the nodes in $[m]$. They only have outgoing edges from $[m]$ to
$[\bar{m}]$. For extending a given DAG on $[\bar{m}]$ to a DAG in $A_{[m]}$,
we can either draw an out-going edge from $[m]$ to $[\bar{m}]$ or not. Giving
us two choices for each pair of nodes in $[m]\times[\bar{m}]$. Hence, there
are $2^{|[m]\times[\bar{m}]|}=2^{m(n-m)}$ ways to extend a given DAG on
$[\bar{m}]$ to a DAG in $A_{[m]}$.

The number of possible DAGs on $[\bar{m}]$ is $a_{n-m}$. Due to Observation 3,
we have that $A_{[m]}$ has $2^{m(n-m)}a_{n-m}$ DAGs obtained by extending the
DAGs on $[m]$. Furthermore, due to Observation 1 and Observation 2, these are
all the possible DAGs in $A_{[m]}$. Hence, $|A_{[m]}|=2^{m(n-m)}a_{n-m}$. Now,
we can repeat this argument for any $m$ sized subset of $[n]$. Hence, if
$|J|=|J^{\prime}|=m$ then $A_{J}=A_{J^{\prime}}=2^{m(n-m)}a_{n-m}$. Hence,
using the principle of inclusion-exclusion as given in equation (7), we have
that:

$a_{n}=\sum_{m=1}^{n}(-1)^{m+1}\binom{n}{m}2^{m(n-m)}a_{n-m}$ (10)

Notice that replacing $n-m$ with $l$ in equation (10), it can be equivalently
written as:

$a_{n}=\sum_{l=0}^{n-1}(-1)^{n-l+1}\binom{n}{l}2^{l(n-l)}a_{l}$ (11)

This change of variable allows us to write a bottom-up algorithm for counting
DAGs, as given in Algorithm 1. Based on this algorithm we now show that
counting DAGs can be performed in polynomial time with respect to the number
of nodes $n$.

######  Proposition 2.

The number of labelled DAGs over $n$ nodes can be computed in polynomial time.

###### Proof.

We define $a_{0}=1$ by convention and then by using equation (11) in Algorithm
1, we incrementally compute $a_{1},a_{2}...$, saving each result in a list
given by $A$. The for loop runs in time $O(n)$, and in each run in line 5, we
perform other $O(n)$ operations. Hence, the algorithm runs in $O(n^{2})$. ∎

Algorithm 1 Number of DAG on $n$ nodes

1:Input: $n$

2:Output: $a_{n}$

3:$A[0]\leftarrow 1$

4:for $i=1$ to $n$ do

5: $A[i]\leftarrow\sum_{l=0}^{i-1}(-1)^{i-l+1}\binom{i}{l}2^{l(i-l)}A[l]$

6:end for

7:return $A[n]$

##  3 WFOMC with DAG Axiom

In this section we extend the approach used for counting DAGs in equation (10)
to WFOMC of FO2 and C2 formulas with a DAG Axiom. First, we formally define
the DAG axiom. We then present Proposition 3, Proposition 4 and Proposition 5,
analogous to Observation 1, 2 and 3 respectively, as presented in the
subsection 2.5. We then use principle of inclusion-exclusion to compute the
WFOMC of universally quantified FO2 formulas extended with a DAG axiom. And
show our method to be domain-liftable. The proposed apporach is then extended
to admit full FO2, Cardinality constraints and C2. We finally extend the DAG
axiom, with additional unary predicates that represent sources and sinks of
the DAG.

######  Definition 4.

Let $\Phi$ be a first-order logic sentence, possibly containing the binary
relation $R$. An interpretation $\omega$ is a model of $\Psi:=\Phi\land
Acyclic(R)$ if and only if:

  * •

$\omega$ is a model of $\Phi$, and

  * •

$\omega_{R}$ forms a Directed Acyclic Graph

######  Definition 5.

Let $\Psi:=\forall xy.\Phi(x,y)\land Acyclic(R)$, interpreted over the domain
$[n]$. Let $1\leq m\leq n$. Then $\omega$ is a model of $\Psi_{[m]}$ if and
only if $\omega$ is a model of $\Psi$ on $[n]$, such that the domain elements
in $[m]$ have zero $R$-indegree.

Notice that due to Definition 5, for the domain $[n]$, $\Psi_{[n]}$ is
equivalent to $\Psi^{\prime}:=\forall xy.\Phi(x,y)\land\neg R(x,y)$.

######  Proposition 3.

Let $\Psi:=\forall xy.\Phi(x,y)\land Acyclic(R)$ and $\Psi^{\prime}:=\forall
xy.\Phi(x,y)\land\neg R(x,y)$ interpreted over $[n]$. Let $1\leq m\leq n$. If
$\omega$ is a model of $\Psi_{[m]}$, then
$\omega\downarrow[m]\models\Psi^{\prime}$ and
$\omega\downarrow[\bar{m}]\models\Psi$.

###### Proof Sketch.

The proposition is a consequence of following three facts: (1) Since, $\forall
xy.\Phi(x,y)$ is an FO2 formula, then if $\omega\models\forall xy.\Phi(x,y)$,
then $\omega\downarrow[m]\models\forall xy.\Phi(x,y)$ and
$\omega\downarrow[\bar{m}]\models\forall xy.\Phi(x,y)$; (2) In
$\omega\models\Psi_{[m]}$, $\omega_{R}$ cannot have an edge in $[m]$. Hence,
$\omega\downarrow[m]\models\Psi^{\prime}$; and (3) Subgraph of a DAG is a DAG,
hence if $\omega\models\Psi_{[m]}$, then
$\omega\downarrow[\bar{m}]\models\Psi_{[m]}$. We provide the detailed proof in
Appendix. ∎

######  Proposition 4.

Let $\Psi:=\forall xy.\Phi(x,y)\land Acyclic(R)$ and $\Psi^{\prime}:=\forall
xy.\Phi(x,y)\land\neg R(x,y)$ interpreted over the domain $[n]$. Let
$\omega^{\prime}$ be a model of $\Psi^{\prime}$ on the domain $[m]$ and let
$\omega^{\prime\prime}$ be a model of $\Psi$ on the domain $[\bar{m}]$. Then
the number of extensions $\omega$, of
$\omega^{\prime}\uplus\omega^{\prime\prime}$, such that
$\omega\models\Psi_{[m]}\land{\bm{k}}$ is given as:

$\prod_{i,j\in[u]}n_{ij}^{k^{\prime}_{i}\cdot k^{\prime\prime}_{j}}$ (12)

where $k^{\prime}_{i}$ and $k^{\prime\prime}_{i}$ are the number of domain
constants realizing the $i^{th}$ 1-type in $\omega^{\prime}$ and
$\omega^{\prime\prime}$ respectively. We define $n_{ijl}$ to be $1$ if
$ijl(x,y)\models\Phi(\\{x,y\\})\land\neg R(y,x)$ and $0$ otherwise and
$n_{ij}=\sum_{l\in[b]}n_{ijl}$.

###### Proof.

In order to obtain an interpretation $\omega\models\Psi_{[m]}\land{\bm{k}}$ on
the domain $[n]$ from $\omega^{\prime}\uplus\omega^{\prime\prime}$, we only
need to extend $\omega^{\prime}\uplus\omega^{\prime\prime}$ with
interpretations of the ground-atoms containig $(c,d)\in[m]\times[\bar{m}]$.
For a given pair $(c,d)\in[m]\times[\bar{m}]$, let $\omega^{\prime}\models
i(c)$ and $\omega^{\prime\prime}\models j(d)$. Since $\omega$ is a model of
$\forall xy.\Phi(x,y)$, we must have that $ijl(c,d)\models\Phi(\\{c,d\\})$.
Furthermore, since we want that every domain element in $[m]$ has indegree
zero, we cannot have $R(d,c)$. Hence, we must have that
$ijl(c,d)\models\Phi(\\{c,d\\})\land\neg R(d,c)$. Hence, the number of
2-tables that can be realized by $(c,d)$ is given by $n_{ij}$. Since there are
$k^{\prime}_{i}$ domain elements $c$ realizing the $i^{th}$ 1-type in
$\omega^{\prime}$ and $k^{{}^{\prime\prime}}_{j}$ domain elements $d$
realizing the $j^{th}$ 1-type in $\omega^{\prime\prime}$, the number of
extensions $\omega$, of $\omega^{\prime}\uplus\omega^{\prime\prime}$, such
that $\omega\models\Psi_{[m]}\land{\bm{k}}$ is given by expression (12). ∎

######  Proposition 5.

Let $\Psi:=\forall xy.\Phi(x,y)\land Acyclic(R)$ and $\Psi^{\prime}:=\forall
xy.\Phi(x,y)\land\neg R(x,y)$. Then:

$\begin{split}&\mbox{\sc fomc}(\Psi_{[m]},{\bm{k}})=\\\
&\sum_{\begin{subarray}{c}{\bm{k}}={\bm{k}}^{\prime}+{\bm{k}}^{\prime\prime}\\\
|{\bm{k}}^{\prime}|=m\end{subarray}}\prod_{i,j\in[u]}n_{ij}^{k^{\prime}_{i}k^{\prime\prime}_{j}}\cdot\mbox{\sc
fomc}(\Psi^{\prime},{\bm{k}}^{\prime})\cdot\mbox{\sc
fomc}(\Psi,{\bm{k}}^{\prime\prime})\end{split}$ (13)

where ${\bm{k}}^{\prime}+{\bm{k}}^{\prime\prime}$ represents the element-wise
sum of integer-vectors ${\bm{k}}^{\prime}$ and ${\bm{k}}^{\prime\prime}$, such
that $|{\bm{k}}^{\prime}|=m$ and $|{\bm{k}}^{\prime\prime}|=|{\bm{k}}|-m$.
Also, $n_{ij}=\sum_{l}n_{ijl}$ and $n_{ijl}$ is $1$ if
${ijl(x,y)\models\Phi(\\{x,y\\})\land\neg R(y,x)}$ and $0$ otherwise.

###### Proof.

The number of models of $\Psi^{\prime}$ on $[m]$, with 1-type cardinality
vector ${\bm{k}}^{\prime}$ is given as $\mbox{\sc
fomc}(\Psi^{\prime},{\bm{k}}^{\prime})$. Similarly, the number models of
$\Psi$ on $[\bar{m}]$, with 1-type cardinality vector
${\bm{k}}^{\prime\prime}$ is given as $\mbox{\sc
fomc}(\Psi,{\bm{k}}^{\prime\prime})$. Due to proposition 4, each such model
can be extended in
$\prod_{i,j\in[u]}n_{ij}^{k^{\prime}_{i}k^{\prime\prime}_{j}}$ ways. The
summation in (LABEL:eq:_k_k'_m) runs over all possible realizable 1-type
cardinalities over $[m]$ and $[\bar{m}]$, represented by ${\bm{k}}^{\prime}$
and ${\bm{k}}^{\prime\prime}$ respectively, such that they are consistent with
${\bm{k}}$, i.e. when ${\bm{k}}={\bm{k}}^{\prime}+{\bm{k}}^{\prime\prime}$.
Hence, formula (LABEL:eq:_k_k'_m) gives us the total number of models
$\omega$, such that $\omega\downarrow[m]\models\Psi^{\prime}$,
$\omega\downarrow[\bar{m}]\models\Psi$ and $\omega\models\Psi\land{\bm{k}}$
where the domain constant in $[m]$ have zero $R$ indegree. Due to proposition
3, we have that these are all the models such that
$\omega\models\Psi\land{\bm{k}}$ and the domain constants in $[m]$ have zero
$R$ indegree. ∎

Proposition 5 can be easily extended to WFOMC as follows:

######  Proposition 6.

Let $\Psi:=\forall xy.\Phi(x,y)\land Acyclic(R)$ and $\Psi^{\prime}:=\forall
xy.\Phi(x,y)\land\neg R(x,y)$. Then:

$\begin{split}&\mbox{\sc wfomc}(\Psi_{[m]},{\bm{k}})=\\\
&\sum_{\begin{subarray}{c}{\bm{k}}={\bm{k}}^{\prime}+{\bm{k}}^{\prime\prime}\\\
|{\bm{k}}^{\prime}|=m\end{subarray}}\prod_{i,j\in[u]}r_{ij}^{k^{\prime}_{i}k^{\prime\prime}_{j}}\cdot\mbox{\sc
wfomc}(\Psi^{\prime},{\bm{k}}^{\prime})\cdot\mbox{\sc
wfomc}(\Psi,{\bm{k}}^{\prime\prime})\end{split}$ (14)

where ${\bm{k}}^{\prime}+{\bm{k}}^{\prime\prime}$ represents the element-wise
sum of integer-vectors ${\bm{k}}^{\prime}$ and ${\bm{k}}^{\prime\prime}$, such
that $|{\bm{k}}^{\prime}|=m$ and $|{\bm{k}}^{\prime\prime}|=|{\bm{k}}|-m$.
Also, $n_{ij}=\sum_{l}n_{ijl}v_{l}$ and $n_{ijl}$ is $1$ if
${ijl(x,y)\models\Phi(\\{x,y\\})\land\neg R(y,x)}$ and $0$ otherwise.

The proof is almost identical to the one of Propostion 5, with verbose and
cosmetic changes for dealing with weights. In comparision to equation
(LABEL:eq:_k_k'_m) in equation (LABEL:eq:_atleast_weighted), the $r_{ij}$ is
the multiplicative weight contribution due to the $n_{ij}$ – exactly as done
in proof of Theorem 1 – and FOMC on ${\bm{k}}^{\prime}$ and
${\bm{k}}^{\prime\prime}$ can be replaced with WFOMC, because they are
independent counting problems.

######  Proposition 7.

The first order model count of the formula $\Psi:=\forall xy.\Phi(x,y)\land
Acyclic(R)$ is given as:

$\mbox{\sc
wfomc}(\Psi,{\bm{k}}):=\sum_{m=1}^{|{\bm{k}}|}(-1)^{m+1}\binom{|{\bm{k}}|}{m}\mbox{\sc
wfomc}(\Psi_{[m]},{\bm{k}})$ (15)

###### Proof.

The proof idea is very similar to the case for counting DAGs as given in (10).
Let the domain be $[n]$, hence $|{\bm{k}}|=n$. Let $A_{i}$ be the set of
models $\omega\models\Psi$, such that $\omega$ has 1-type cardinality
${\bm{k}}$ and the domain element $i$ has zero $R$-indegree. Since, each DAG
has atleast one node with zero $R$-indegree, our goal is to compute $\mbox{\sc
w}(\cup_{i\in[n]}A_{i})$. Let $J\subseteq[n]$ be an arbitrary set of domain
constants. Let $A_{J}:=\bigcap_{j\in J}A_{j}$ for an arbitrary subset $J$ of
$[n]$. Then using principle of inclusion-exclusion as given in equation (9),
we have that:

$\mbox{\sc wfomc}(\Psi,{\bm{k}})=\sum_{\emptyset\neq
J\subseteq[n]}(-1)^{|J|+1}\mbox{\sc w}(A_{[m]})$ (16)

Now, $A_{[m]}$ is the set of models such that domain elements in $[m]$ have
zero $R$-indegree. Hence, $A_{[m]}$ are exactly the models of $\Psi_{[m]}$.
Furthermore, notice that in Proposition 3, Proposition 4 and Proposition 6,
$[m]$ can be replaced with any $m$-sized subset $J$ of $[n]$. Hence, for all
$J\subseteq[n]$, such that $|J|=m$, we have that $\mbox{\sc
w}(A_{J})=\mbox{\sc wfomc}(\Psi_{[m]},{\bm{k}})$. Hence, equation (16) reduces
to equation (15). ∎

We make a change of variable in equation (15) (similar to equation (11)), by
replacing $m$ with $|{\bm{k}}|-l$, to obtain the following equation:

$\displaystyle\begin{split}&\mbox{\sc wfomc}(\Psi,{\bm{k}})=\\\
&\sum_{l=0}^{|{\bm{k}}|-1}(-1)^{|{\bm{k}}|-l+1}\binom{|{\bm{k}}|}{l}\mbox{\sc
wfomc}(\Psi_{[|{\bm{k}}|-l]},{\bm{k}})\end{split}$ (17)

We provide pseudocode for evaluating equation (17) in Algorithm 2, namely
WFOMC-DAG. We now analyse how WFOMC-DAG works and show that it runs in
polynomial time with respect to domain cardinality $|{\bm{k}}|=n$.

WFOMC-DAG takes as input $\Psi:=\forall xy.\Phi(x,y)\land Acyclic(R)$ and
${\bm{k}}$ – where $\Phi(x,y)$ is a quantifier-free formula and ${\bm{k}}$ is
a 1-type cardinality vector, such that $|{\bm{k}}|=n$ – and returns $\mbox{\sc
wfomc}(\Psi,{\bm{k}})$. In line $3$, an array $A$ with $u$ indices is
initiated and $A[\mathbf{0}]$ is assigned the value $1$, where $\mathbf{0}$
corresponds to the $u$ dimensional zero vector. The for loop in line $5-7$
incrimentally computes $\mbox{\sc wfomc}(\Psi,{\bm{p}})$, where the loop runs
over all $u$-dimensional integer vectors ${\bm{p}}$, such that $p_{i}\leq
k_{i}$, in lexicographical order. The number of possible ${\bm{p}}$ vectors is
atmost $n^{u}$. Hence, the for loop in line 5 runs at most $n^{u}$ iterations.
In line 6, we compute $\mbox{\sc wfomc}(\Psi,{\bm{p}})$ as given in equation
(17). Also in line 6, the function $\overline{\mbox{\sc
wfomc}}(\Psi_{[m]},{\bm{p}})$ — that computes $\mbox{\sc
wfomc}(\Psi_{[m]},{\bm{p}})$ —is called at most $|{\bm{p}}|-1$ times, which is
bounded above by $n$. $A[{\bm{p}}]$ stores the value $\mbox{\sc
wfomc}(\Psi,{\bm{p}})$. Hence, as ${\bm{p}}$ increments in lexicographical
order, $A[{\bm{p}}]$, stores the value of $\mbox{\sc
wfomc}(\Psi_{[m]},{\bm{p}})$. In the function $\overline{\mbox{\sc
wfomc}}(\Psi_{[m]},{\bm{s}})$, the number of iterations in the for loop is
bounded above by $n^{2u}$. And $\mbox{\sc
wfomc}(\Psi^{\prime},{\bm{s}}^{\prime})$ is an FO2 WFOMC problem, again
computable in polynomial time. Hence, the algorithm WFOMC-DAG runs in
polynomial time w.r.t domain cardinality. Notice that since loop 5-7 runs in
lexicographical order, the $A[{\bm{s}}^{\prime\prime}]$ required in the
function $\overline{\mbox{\sc wfomc}}(\Psi_{[m]},{\bm{s}})$ are always already
stored in $A$. Now, there are only polynomially many ${\bm{k}}$ w.r.t domain
cardinality. Hence, computing $\mbox{\sc wfomc}(\Psi,{\bm{k}})$ over all
possible ${\bm{k}}$ values, we can compute $\mbox{\sc wfomc}(\Psi,n)$ in
polynomial time w.r.t domain cardinality. Furthermore, using the modular WFOMC
preserving skolemization process as provided in Van den Broeck et al. [2014],
we can easily extend this result to the entire FO2 fragment. Hence, leading to
the following theorem:

Algorithm 2 WFOMC-DAG

1:Input: $\Psi,{\bm{k}}$

2:Output: $\mbox{\sc fomc}(\Psi,{\bm{k}})$

3:$A[\mathbf{0}]\leftarrow 1$ $\triangleright$ $A$ has $u$ indices

4:$\triangleright$ $\mathbf{0}=\langle 0,...,0\rangle$

5:for $\mathbf{0}<{\bm{p}}\leq{\bm{k}}$ where ${\bm{p}}\in\mathbb{N}_{0}^{u}$
do $\triangleright$ Lexical order

6:
${\\!A[{\bm{p}}]\leftarrow\\!\sum_{l=0}^{|{\bm{p}}|-1}(-1)^{|{\bm{p}}|-l+1}\binom{|{\bm{p}}|}{l}{\overline{\mbox{\sc
wfomc}}}(\\!\Psi_{[|{\bm{p}}|-l]},{\bm{p}})}$

7:end for

8:return $A[{\bm{k}}]$

9:function $\overline{\mbox{\sc wfomc}}$($\Psi_{[m]}$, ${\bm{s}}$)
$\triangleright$ Equation (LABEL:eq:_atleast_weighted)

10: $S=0$

11: for ${\bm{s}}^{\prime}+{\bm{s}}^{\prime\prime}={\bm{s}}$ and
$|{\bm{s}}^{\prime}|=m$ do

12: $S\leftarrow
S+\prod_{i,j\in[u]}r_{ij}^{s^{\prime}_{i}s^{\prime\prime}_{j}}\cdot\mbox{\sc
wfomc}(\Psi^{\prime},{\bm{s}}^{\prime})\cdot A[{\bm{s}}^{\prime\prime}]$

13: end for

14: return $S$

15:end function

######  Theorem 4.

Let $\Psi:=\Phi\land Acyclic(R)$, where $\Phi$ is an FO2 formula. Then
$\mbox{\sc wfomc}(\Psi,n)$ can be computed in polynomial time with respect to
the domain cardinality.

Using Theorem 2 and Remark 2, we can also extend domain-liftability of FO2,
with DAG axiom and cardinality constraints.

######  Theorem 5.

Let $\Psi:=\Phi\land Acyclic(R)$, where $\Phi$ is an FO2 formula, potentially
also containing cardinality constraints. Then $\mbox{\sc wfomc}(\Psi,n)$ can
be computed in polynomial time with respect to the domain cardinality.

Furthermore, since WFOMC of any C2 formula can be modularly reduced to WFOMC
of an FO2 formula with cardinality constraints Kuželka [2021]. We also have
the following theorem:

######  Theorem 6.

Let $\Psi:=\Phi\land Acyclic(R)$, where $\Phi$ is an C2 formula. Then
$\mbox{\sc wfomc}(\Psi,n)$ can be computed in polynomial time with respect to
the domain cardinality.

###  3.1 Source and Sink

######  Definition 6.

Let $\Phi$ be a first order sentence, possibly containing some binary relation
$R$, a unary relation $Source$ and a unary relation $Sink$. Then a structure
$\omega$ is a model of $\Psi=\Phi\land Acyclic(R,Source,Sink)$ if and only if:

  * •

$\omega$ is a model of $\Phi\land Acyclic(R)$, and

  * •

In the DAG represented by $\omega_{R}$, the sources of the DAG are interpreted
to be true in $\omega_{Source}$.

  * •

In the DAG represented by $\omega_{R}$, the sinks of the DAG are interpreted
to be true in $\omega_{Sink}$.

The $Source$ and the $Sink$ predicate can allow encodicng constraints like
$\exists^{=k}x.Source(x)$ or $\exists^{=k}x.Sink(x)$.

######  Theorem 7.

Let $\Psi:=\Phi\land Acyclic(R,Source,Sink)$, where $\Phi$ is a C2 formula.
Then $\mbox{\sc wfomc}(\Psi,n)$ can be computed in polynomial time with
respect to the domain cardinality.

###### Proof.

The sentence $\Psi$ can be equivalently written as:

$\displaystyle\begin{split}&\Phi\land Acyclic(R)\\\ &\land\forall
x.Source(x)\leftrightarrow\neg\exists y.R(y,x)\\\ &\land\forall
x.Sink(x)\leftrightarrow\neg\exists y.R(x,y)\\\ \end{split}$ (18)

which is a FO2 sentence extended with DAG constraint. ∎

## Conclusion

In this paper we demonstrate the domain liftability of FO2 and C2 extended
with a Directed Acyclic Graph Axiom. We then extend our results with Source
and Sink predicates, which can allow additional constraints on the number of
sources and sinks in a DAG. These results can potentially allow better
modelling of datasets that naturally appear with a DAG structure Rossi and
Ahmed [2015]. In future, we aim at investigating successor, predecessor and
ancestory constraints in FOL extended with DAG axioms.

###### Acknowledgements.

We would like to thank Andrea Micheli for the fruitful and interesting
discussion time.

## Appendix

See 3

###### Proof.

We have that $\omega\models\Psi$. Hence, we have that:

$\displaystyle\omega$
$\displaystyle\models\bigwedge_{(c,d)\in[n]^{2}}\Phi(c,d)$
$\displaystyle\Rightarrow\omega$
$\displaystyle\models\bigwedge_{(c,d)\in[m]^{2}}\Phi(c,d)\bigwedge_{(c,d)\in[\bar{m}]^{2}}\Phi(c,d)$
$\displaystyle\bigwedge_{(c,d)\in[\bar{m}]\times[m]}\Phi(c,d)\bigwedge_{(c,d)\in[m]\times[\bar{m}]}\Phi(c,d)$

Since, $\omega\models\bigwedge_{(c,d)\in[m]^{2}}\Phi(c,d)$ and
$\omega\models\bigwedge_{(c,d)\in[\bar{m}]^{2}}\Phi(c,d)$, we have that
$\omega\downarrow[m]\models\forall xy.\Phi(x,y)$ and
$\omega\downarrow[\bar{m}]\models\forall xy.\Phi(x,y)$. Now, since $[m]$ has
zero $R$-indegree, it can only have outgoing $R$-edges to $[\bar{m}]$. Hence,
we can infer that $\omega\downarrow[m]\models\forall xy.\neg R(x,y)$. Now,
$\omega_{R}$ is a DAG, then so is $\omega_{R}\downarrow[\bar{m}]$. Hence,
$\omega\downarrow[\bar{m}]\models Acyclic(R)$. Hence,
$\omega\downarrow[m]\models\Psi^{\prime}$ and
$\omega\downarrow[\bar{m}]\models\Psi$. ∎

## References

  * Barvínek et al. [2022] Jáchym Barvínek, Timothy Van Bremen, Yuyi Wang, Filip Železný, and Ondřej Kuželka.  Automatic conjecturing of p-recursions using lifted inference.  In Nikos Katzouris and Alexander Artikis, editors, _Inductive Logic Programming_ , pages 17–25, Cham, 2022. Springer International Publishing.  ISBN 978-3-030-97454-1.
  * Beame et al. [2015] Paul Beame, Guy Van den Broeck, Eric Gribkoff, and Dan Suciu.  Symmetric weighted first-order model counting.  In _Proceedings of the 34th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems_ , pages 313–328, 2015.
  * Clough et al. [2014] James R. Clough, Jamie Gollings, Tamar V. Loach, and Tim S. Evans.  Transitive reduction of citation networks.  _Journal of Complex Networks_ , 3(2):189–203, 09 2014.  ISSN 2051-1310.  10.1093/comnet/cnu039.  URL https://doi.org/10.1093/comnet/cnu039.
  * firens et al. [2015] Daan firens, Guy Van Den Broeck, Joris Renkens, Dimitar Shterionov, Bernd Gutmann, Ingo Thon, Gerda Janssens, and Luc De Raedt.  Inference and learning in probabilistic logic programs using weighted boolean formulas.  _Theory and Practice of Logic Programming_ , 15(3):358–401, 2015.  10.1017/S1471068414000076.
  * Ganian et al. [2022] Robert Ganian, Thekla Hamm, and Topi Talvitie.  An efficient algorithm for counting markov equivalent dags.  _Artificial Intelligence_ , 304:103648, 2022.  ISSN 0004-3702.  https://doi.org/10.1016/j.artint.2021.103648.  URL https://www.sciencedirect.com/science/article/pii/S0004370221001995.
  * Getoor and Taskar [2007] Lise Getoor and Ben Taskar.  _Statistical relational learning_.  MIT press Cambridge, 2007.
  * Gradel et al. [1997] Erich Gradel, Martin Otto, and Eric Rosen.  Two-variable logic with counting is decidable.  In _Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science_ , pages 306–317. IEEE, 1997.
  * Kuusisto and Lutz [2018] Antti Kuusisto and Carsten Lutz.  Weighted model counting beyond two-variable logic.  In _Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science_ , pages 619–628, 2018.
  * Kuželka [2021] Ondřej Kuželka.  Weighted first-order model counting in the two-variable fragment with counting quantifiers, 2021.  URL https://doi.org/10.1613/jair.1.12320.
  * Malhotra and Serafini [2022] Sagar Malhotra and Luciano Serafini.  Weighted model counting in fo2 with cardinality constraints and counting quantifiers: A closed form formula.  _Proceedings of the AAAI Conference on Artificial Intelligence_ , 36(5):5817–5824, Jun. 2022.  10.1609/aaai.v36i5.20525.  URL https://ojs.aaai.org/index.php/AAAI/article/view/20525.
  * Raedt et al. [2016] Luc De Raedt, Kristian Kersting, Sriraam Natarajan, and David Poole.  _Statistical relational artificial intelligence: Logic, probability, and computation_.  Morgan & Claypool Publishers, 2016.
  * Richardson and Domingos [2006] Matthew Richardson and Pedro Domingos.  Markov logic networks.  _Machine learning_ , 62(1-2):107–136, 2006.
  * Rossi and Ahmed [2015] Ryan A. Rossi and Nesreen K. Ahmed.  The network data repository with interactive graph analytics and visualization.  In _AAAI_ , 2015.  URL https://networkrepository.com.
  * Steinsky [2003] Bertran Steinsky.  Enumeration of labelled chain graphs and labelled essential directed acyclic graphs.  _Discrete Mathematics_ , 270(1):267–278, 2003\.  ISSN 0012-365X.  https://doi.org/10.1016/S0012-365X(02)00838-5.  URL https://www.sciencedirect.com/science/article/pii/S0012365X02008385.
  * Tóth and Kuželka [2022] Jan Tóth and Ondřej Kuželka.  Lifted inference with linear order axiom, 2022.  URL https://arxiv.org/abs/2211.01164.
  * Van Bremen and Kuželka [2021] Timothy Van Bremen and Ondřej Kuželka.  Lifted Inference with Tree Axioms.  In _Proceedings of the 18th International Conference on Principles of Knowledge Representation and Reasoning_ , pages 599–608, 11 2021\.  10.24963/kr.2021/57.  URL https://doi.org/10.24963/kr.2021/57.
  * Van den Broeck et al. [2011] Guy Van den Broeck, Nima Taghipour, Wannes Meert, Jesse Davis, and Luc De Raedt.  Lifted probabilistic inference by first-order knowledge compilation.  In _Proceedings of the Twenty-Second international joint conference on Artificial Intelligence_ , pages 2178–2185. AAAI Press/International Joint Conferences on Artificial Intelligence, 2011.
  * Van den Broeck et al. [2014] Guy Van den Broeck, Wannes Meert, and Adnan Darwiche.  Skolemization for weighted first-order model counting.  In _Fourteenth International Conference on the Principles of Knowledge Representation and Reasoning_ , 2014.