# Complexity of Weighted First-Order Model Counting in the Two-Variable
Fragment with Counting Quantifiers:
A Bound to Beat

Jan Tóth
Faculty of Electrical Engineering
Czech Technical University in Prague
Prague, Czech Republic
Ondřej Kuželka
Faculty of Electrical Engineering
Czech Technical University in Prague
Prague, Czech Republic

###### Abstract

We study the time complexity of the weighted first-order model counting
(WFOMC) over the logical language with two variables and counting quantifiers.
The problem is known to be solvable in time polynomial in the domain size.
However, the degree of the polynomial, which turns out to be relatively high
for most practical applications, has never been properly addressed. First, we
formulate a time complexity bound for the existing techniques for solving
WFOMC with counting quantifiers. The bound is already known to be a polynomial
with its degree depending on the number of cells of the input formula. We
observe that the number of cells depends, in turn, exponentially on the
parameter of the counting quantifiers appearing in the formula. Second, we
propose a new approach to dealing with counting quantifiers, reducing the
exponential dependency to a quadratic one, therefore obtaining a tighter upper
bound. It remains an open question whether the dependency of the polynomial
degree on the counting quantifiers can be reduced further, thus making our new
bound a _bound to beat_.

##  1 Introduction

The weighted first-order model counting (WFOMC) problem was originally
proposed in the area of lifted inference as a method to perform probabilistic
inference over statistical relational learning models on the lifted level (Van
den Broeck et al., 2011). Its applications have ranged beyond (symbolic)
probabilistic reasoning since then, including conjecturing recursive formulas
in enumerative combinatorics (Barvínek et al., 2021) and discovering
combinatorial integer sequences (Svatoš et al., 2023).

Regardless of the particular application context, WFOMC is also used to define
a class of tractable (referred to as _domain-liftable_) modelling languages,
i.e., languages which permit polynomial-time WFOMC computation in the domain
size. The logical fragment with two variables was the first to be identified
as such (Van den Broeck, 2011; Van den Broeck et al., 2014). Negative result
proving that logic with three variables contains $\verb|#|P_{1}$-complete
counting problems followed (Beame et al., 2015), spawning many attempts to
recover at least some of the expressive power provided by three and more
variables, yet retaining the domain-liftability property.

Kazemi et al. (2016) introduced two new liftable classes, namely
$\textbf{S}^{2}\textbf{FO}^{2}$ and $\textbf{S}^{2}\textbf{RU}$. Kuusisto and
Lutz (2018) extended the two-variable fragment with one function constraint
and showed such language to be domain-liftable, too. That result was later
generalized to the two-variable fragment with counting quantifiers, denoted by
$\textbf{C}^{2}$ (Kuželka, 2021). Moreover, several axioms can be added on top
of the counting quantifiers, still retaining domain-liftability as well (van
Bremen and Kuželka, 2021b; Tóth and Kuželka, 2023; Malhotra and Serafini,
2023; Malhotra et al., 2023).

The work presented here has two major contributions. First, we study the
domain-liftability result for $\textbf{C}^{2}$ in a greater detail, deriving a
more concrete upper bound on the time complexity. Although the bound has
already been proved to be polynomial in the domain size, the polynomial is yet
to be explicitly derived. Moreover, as we will show, the polynomial’s degree
depends exponentially on the particular counting quantifiers appearing in the
input formula. Second, we propose a new approach to dealing with counting
quantifiers, when computing WFOMC over $\textbf{C}^{2}$, which decreases the
identified exponential dependency to a quadratic one. Thus, we further tighten
the upper bound.

First, we review necessary preliminaries in Section 2. In Section 3, we derive
an upper bound on the time complexity of computing WFOMC over $\textbf{C}^{2}$
for existing techniques. In Section 4, we continue by presenting a new
technique for solving the problem, which improves the old upper bound
considerably. To support our theoretical results, Section 5 contains several
experimental scenarios. The runtime measurements therein show our improvement
for several $\textbf{C}^{2}$ sentences and also sentences from one of the
domain-liftable $\textbf{C}^{2}$ extensions. Finally, we review related works
in Section 6 and we conclude in Section 7.

##  2 Background

Notation-wise, we adhere to the standard way of writing both algebraic and
logical formulas. For readability purposes, we sometimes use $\cdot$ to denote
multiplication and other times, as is also common, we drop the operation sign.
We use boldface letters such as x to denote vectors and for any
$n\in\mathds{N}$, $\left[n\right]$ denotes the set $\\{1,2,\ldots,n\\}$.

###  2.1 First-Order Logic

We work with a function-free subset of first-order logic (FOL). A particular
language is defined by a finite set of variables $\mathcal{V}$, a finite set
of constants (also called domain) $\Delta$ and a finite set of predicates
$\mathcal{P}$. Assuming a predicate $P\in\mathcal{P}$ with arity $k$, we also
write $P/k\in\mathcal{P}$. An _atom_ has the form
$P(t_{1},t_{2},\ldots,t_{k})$ where $P/k\in\mathcal{P}$ and $t_{i}\in\Delta$
$\cup$ $\mathcal{V}$ are called _terms_. A literal is an atom or its negation.
A set of _formulas_ can be then defined inductively. Both atoms and literals
are formulas. Given some formulas, more complex formulas may be formed by
combining them using logical connectives, or by surrounding them with a
universal ($\forall x$) or an existential ($\exists x$) quantifier where
$x\in\mathcal{V}$.

A variable $x$ in a formula is called _free_ if the formula contains no
quantification over $x$, otherwise $x$ is called _bound_. A formula is called
a _sentence_ if it contains no free variables. A formula is called _ground_ if
it contains no variables.

We use the definition of truth (i.e., semantics) from _Herbrand Logic_
(Hinrichs and Genesereth, 2006). The _Herbrand Base_ (HB) of a language is the
set of all ground atoms that can be constructed given the sets $\mathcal{P}$
and $\Delta$. A possible world, usually denoted by $\omega$, is any subset of
HB. Atoms contained in a possible world $\omega$ are considered to be true,
the rest, i.e., those contained in $\text{HB}\setminus\omega$, are considered
false. The truth value of a more complex formula in a possible world is
defined in the natural way. A possible world $\omega$ is a _model_ of a
formula $\varphi$ if $\varphi$ is satisfied in $\omega$.

####  2.1.1 FOL Fragments

We often do not work with the entire language of FOL, but rather some of its
fragments. The simplest fragment that we work with is the logic with at most
two variables, denoted as $\textbf{FO}^{2}$. As the name suggests, any formula
from $\textbf{FO}^{2}$ contains at most two logical variables.

The second fragment that we consider is the two-variable fragment with
cardinality constraints. We keep the restriction of at most two variables, but
we recover some of the expressive power of logics with more variables by
introducing an additional syntactic construct, namely a _cardinality
constraint_ (CC). We denote such language as $\textbf{FO}^{2}+\textbf{CC}$.
CCs have the form $(|P|=k)$, where $P\in\mathcal{P}$ and $k\in\mathds{N}$.
Intuitively, such a cardinality constraint is satisfied in $\omega$ if there
are exactly $k$ ground atoms with predicate $P$ therein.

Finally, the fragment that we pay most of our attention to is the two-variable
logic with counting quantifiers, denoted by $\textbf{C}^{2}$. A _counting
quantifier_ is a generalization of the traditional existential quantifier. For
a variable $x\in\mathcal{V}$, a quantifier of the form $(\exists^{=k}x)$,
where $k\in\mathds{N}$, is allowed by our syntax. Satisfaction of formulas
with counting quantifiers is defined naturally, in a similar manner to the
satisfaction of cardinality constraints. For example, $\exists^{=k}x:\psi(x)$
is satisfied in $\omega$ if there are exactly $k$ constants
$\\{A_{1},A_{2},\ldots,A_{k}\\}\subseteq\Delta$ such that $\forall
i\in[k]:\omega\models\psi(A_{i})$.111Both cardinality constraints and counting
quantifiers can be defined to also allow inequality operators apart from
equality. However, in techniques that we study, inequalities are handled by
transforming them to equalities (Kuželka, 2021). Hence, for brevity, we opted
for the simpler case with equality signs only.

Note the distinction between cardinality constraints and counting quantifiers.
While the counting formula $\exists^{=k}x\;R(x)$ can be equivalently written
using a cardinality constraint as $(|R|=k)$, the formula $\forall
x\exists^{=k}y\;R(x,y)$ no longer permits such a simple transformation.

###  2.2 Weighted First-Order Model Counting

Let us start by formally defining the task that we study.

######  Definition 1.

(Weighted First-Order Model Counting) Let $\varphi$ be a formula over a fixed
logical language $\mathcal{L}$. Let $(w,\overline{w})$ be a pair of weight
functions assigning a weight to each predicate in $\mathcal{L}$. Let $n$ be a
natural number. Denote $\mathcal{MOD}(\varphi,n)$ the set of all models of
$\varphi$ on a domain on size $n$. We define

$\displaystyle\textup{WFOMC}(\varphi,n,w,\overline{w})=\sum_{\omega\in\mathcal{MOD}(\varphi,n)}\prod_{l\in\omega}w(\mathsf{pred}(l))\prod_{l\in\textup{HB}\setminus\omega}\overline{w}(\mathsf{pred}(l)),$

where the function $\mathsf{pred}$ maps each literal to its predicate.

In general, WFOMC is a difficult problem. There exists a sentence with three
logical variables, for which the computation is $\verb|#|P_{1}$-complete with
respect to n (Beame et al., 2015). However, for some logical languages, WFOMC
can be computed in time polynomial in the domain size, which is also referred
to as the language being _domain-liftable_.

######  Definition 2.

(Domain-Liftability) Consider a logical language $\mathcal{L}$. The language
is said to be _domain-liftable_ if and only if for any fixed
$\varphi\in\mathcal{L}$ and any $n\in\mathds{N}$, it holds that
WFOMC($\varphi,n,w,\overline{w}$) can be computed in time polynomial in $n$.

Thus, when we study domain-liftable languages, we focus on the time complexity
with respect to the domain size, which is assumed to be the only varying
input. That is also called _data complexity_ of WFOMC in other literature
(Beame et al., 2015).

In the remainder of this text, it is often the case that we reduce one WFOMC
computation (instance) to another over a different (larger) formula, possibly
with fresh (not appearing in the original vocabulary) predicates. Even then,
the assumed input language remains fixed in the context of the new WFOMC
instance. Moreover, if we do not specify some of the weights for the new
predicates, they are assumed to be unitary.

The first language proved to be domain-liftable was the language of
$\textbf{UFO}^{2}$, i.e., universally quantified $\textbf{FO}^{2}$ (Van den
Broeck, 2011), which was later generalized to the entire $\textbf{FO}^{2}$
fragment (Van den Broeck et al., 2014). The original proof, making use of
first-order knowledge compilation (Van den Broeck et al., 2011), was later
reformulated using _1-types_ (which we call _cells_) from logic literature
(Beame et al., 2015).

######  Definition 3.

(Valid Cell) A cell of a first-order formula $\varphi$ is a maximal consistent
conjunction of literals formed from atoms in $\varphi$ using only a single
variable. Moreover, a cell $C(x)$ of a first-order formula $\varphi(x,y)$ is
valid, if $\varphi(t,t)\wedge C(t)$ is satisfiable for any constant
$t\in\Delta$.

######  Example 1.

Consider $\varphi=G(x)\vee H(x,y)$.

Then $\varphi$ has four cells:

$\displaystyle C_{1}(x)$ $\displaystyle=\neg G(x)\wedge\neg H(x,x),$
$\displaystyle C_{2}(x)$ $\displaystyle=\neg G(x)\wedge H(x,x),$
$\displaystyle C_{3}(x)$ $\displaystyle=G(x)\wedge\neg H(x,x),$ $\displaystyle
C_{4}(x)$ $\displaystyle=G(x)\wedge H(x,x).$

However, only cells $C_{2},C_{3}$ and $C_{4}$ are valid.

Another domain-liftable language is $\textbf{FO}^{2}+\textbf{CC}$. WFOMC over
$\textbf{FO}^{2}+\textbf{CC}$ is solved by repeated calls to an oracle solving
WFOMC over $\textbf{FO}^{2}$. The number of required calls depends on the
arities of predicates that appear in cardinality constraints. Consider
$\Upsilon=\bigwedge_{i=1}^{m}\left(|R_{i}|=k_{i}\right)$ and let us denote

$\alpha(\Upsilon)=\prod_{i=1}^{m}{\left(arity(R_{i})+1\right)}.$

For an $\textbf{FO}^{2}+\textbf{CC}$ formula $\Gamma=\Phi\wedge\Upsilon$ such
that $\Phi\in\textbf{FO}^{2}{}$ and $\Upsilon$ same as above, we will require
$n^{\alpha}$ calls to the oracle (Kuželka, 2021).

Having defined WFOMC, valid cells, and function $\alpha$, we can state known
upper bounds for computing WFOMC over $\textbf{FO}^{2}$ and
$\textbf{FO}^{2}+\textbf{CC}$. We concentrate those results into a single
theorem.

######  Theorem 1.

Let $\Gamma$ be an $\textbf{FO}^{2}$ sentence with $p$ valid cells. Let
$\Upsilon=\bigwedge_{i=1}^{m}\left(|R_{i}|=k_{i}\right)$ be $m$ cardinality
constraints, where $R_{1},R_{2},\ldots,R_{m}$ are some predicates from the
language of $\Gamma$ and each $k_{i}\in\mathds{N}$. For any $n\in\mathds{N}$
and any fixed weights $(w,\overline{w})$, WFOMC($\Gamma,n,w,\overline{w}$) can
be computed in time $\mathcal{O}(n^{p+1})$, and
WFOMC($\Gamma\wedge\Upsilon,n,w,\overline{w}$) can be computed in time
$\mathcal{O}(n^{\alpha(\Upsilon)}\cdot n^{p+1})$. Since both the bounds are
polynomials in $n$, both languages are domain-liftable.

The first bound follows from the cell-based domain-liftability proof (Beame et
al., 2015).222The state-of-the-art algorithm for computing WFOMC over
$\textbf{FO}^{2}$, i.e., FastWFOMC, improves the bound considerably in some
cases (van Bremen and Kuželka, 2021a). However, as the improvements are not
guranteed in the general case, we work with this bound as an effective worst
case. Moreover, as we demonstrate in the experimental section, our new
encoding described further in the text improves the FastWFOMC runtime for
$\textbf{C}^{2}$ sentences reduced to $\textbf{FO}^{2}+\textbf{CC}$ as well.
The second bound follows from Propositions $4$ and $5$ in Kuželka (2021).

It is important to note that Theorem 1 assumes all mathematical operations to
take constant time. Hence, the theorem omits factors relating to _bit
complexity_ which Kuželka (2021) also addresses. However, those factors remain
the same in all transformations that we consider. Therefore, for increased
readability, we omit them. For a more detailed discussion on bit complexity,
see the appendix.

###  2.3 Solving WFOMC with Counting Quantifiers

Yet another domain-liftable language is the language of $\textbf{C}^{2}$.
WFOMC over $\textbf{C}^{2}$ is solved by a reduction to WFOMC over
$\textbf{FO}^{2}+\textbf{CC}$ (Kuželka, 2021). The reduction consists of
several steps that we review in the lemmas below. The lemmas concentrate
results from other publications, hence, we make appropriate references to each
of them.

First, we review a specialized _Skolemization_ procedure for WFOMC (Van den
Broeck et al., 2014) which turns an arbitrary $\textbf{FO}^{2}$ sentence into
a $\textbf{UFO}^{2}$ sentence. Since all algorithms for solving WFOMC over
$\textbf{FO}^{2}$ expect a universally quantified sentence as an input, this
is a paramount procedure. Compared to the source publication, we present a
slightly modified Skolemization procedure. The modification is due to Beame et
al. (2015).

######  Lemma 1.

Let $\Gamma=Q_{1}x_{1}Q_{2}x_{2}\ldots Q_{k}x_{k}\Phi(x_{1},\ldots,x_{k})$ be
a first-order sentence in prenex normal form with each quantifier $Q_{i}$
being either $\forall$ or $\exists$ and $\Phi$ being a quantifier-free
formula. Denote $j$ the first position of $\exists$. Let
$\textbf{x}=(x_{1},\ldots,x_{j-1})$ and
$\varphi(\textbf{x},x_{j})=Q_{j+1}x_{j+1}\ldots Q_{k}x_{k}\Phi$. Set

$\Gamma^{\prime}=\forall\textbf{x}\left(\left(\exists
x_{j}\varphi(\textbf{x},x_{j})\right)\Rightarrow A(\textbf{x})\right),$

where $A$ is a fresh predicate. Then, for any $n\in\mathds{N}$ and any weights
$(w,\overline{w})$ with $w(A)=1$ and $\overline{w}(A)=-1$, it holds that

$\textup{WFOMC}(\Gamma,n,w,\overline{w})=\textup{WFOMC}(\Gamma^{\prime},n,w,\overline{w}).$

Lemma 1 suggests how to eliminate one existential quantifier. By transforming
the implication inside $\Gamma^{\prime}$ into a disjunction, we obtain a
universally quantified sentence. Repeating the procedure for each sentence in
the input formula will eventually lead to one universally quantified sentence.

Next, we present a technique to eliminate negation of a subformula without
distributing it inside. The procedure builds on ideas from the Skolemization
procedure and it was presented as Lemma 3.4 in Beame et al. (2015). It was
also described as a _relaxed Tseitin transform_ in Meert et al. (2016).

######  Lemma 2.

Let $\neg\psi(\textbf{x})$ be a subformula of a first-order logic sentence
$\Gamma$ with $k$ free variables $\textbf{x}=(x_{1},\ldots,x_{k})$. Let $C/k$
and $D/k$ be two fresh predicates with $w(C)=\overline{w}(C)=w(D)=1$ and
$\overline{w}(D)=-1$. Denote $\Gamma^{\prime}$ the formula obtained from
$\Gamma$ by replacing the subformula $\neg\psi(\textbf{x})$ with
$C(\textbf{x})$. Let $\Upsilon=\left(\forall\textbf{x}\;C(\textbf{x})\vee
D(\textbf{x})\right)\wedge\left(\forall\textbf{x}\;C(\textbf{x})\vee\psi(\textbf{x})\right)\wedge\left(\forall\textbf{x}\;D(\textbf{x})\vee\psi(\textbf{x})\right)$.
Then, it holds that

$\textup{WFOMC}(\Gamma,n,w,\overline{w})=\textup{WFOMC}(\Gamma^{\prime}\wedge\Upsilon,n,w,\overline{w}).$

Finally, we move to dealing with counting quantifiers. We start with a single
counting quantifier. The approach follows from Lemma 3 in Kuželka (2021).

######  Lemma 3.

Let $\Gamma$ be a first-order logic sentence. Let $\Psi$ be a $\textbf{C}^{2}$
sentence such that $\Psi=\exists^{=k}x\;R(x)$. Let $\Psi^{\prime}=(|R|=k)$ be
a cardinality constraint. Then, it holds that

$\displaystyle\textup{WFOMC}(\Gamma\wedge\Psi,n,w,\overline{w})=\textup{WFOMC}(\Gamma\wedge\Psi^{\prime},n,w,\overline{w}).$

Next, we deal with a specific case of a formula quantified as
$\forall\exists^{=k}$. The following lemma was Lemma 2 in Kuželka (2021)

######  Lemma 4.

Let $\Gamma$ be a first-order logic sentence. Let $\Psi$ be a $\textbf{C}^{2}$
sentence such that $\Psi=\forall x\exists^{=k}y\;R(x,y)$. Let $\Upsilon$ be an
$\textbf{FO}^{2}+\textbf{CC}$ sentence defined as

$\displaystyle\Upsilon$ $\displaystyle=(|R|=k\cdot n)\wedge(\forall x\forall
y\;R(x,y)\Leftrightarrow\bigvee_{i=1}^{k}f_{i}(x,y))$
$\displaystyle\wedge\bigwedge_{1\leq i<j\leq k}(\forall x\forall
y\;f_{i}(x,y)\Rightarrow\neg f_{j}(x,y))$
$\displaystyle\wedge\bigwedge_{i=1}^{k}(\forall x\exists y\;f_{i}(x,y)),$

where $f_{i}/2$ are fresh predicates not appearing anywhere else. Then, it
holds that

$\textup{WFOMC}(\Gamma\wedge\Psi,n,w,\overline{w})=\frac{1}{(k!)^{n}}\textup{WFOMC}(\Gamma\wedge\Upsilon,n,w,\overline{w}).$

Finally, we present a case, which helps dealing with an arbitrary counting
formula. It was originally presented as Lemma 4 in Kuželka (2021).

######  Lemma 5.

Let $\Gamma$ be a first-order logic sentence. Let $\Psi$ be a $\textbf{C}^{2}$
sentence such that $\Psi=\forall x\;A(x)\vee(\exists^{=k}y\;R(x,y))$. Define
$\Upsilon=\Upsilon_{1}\wedge\Upsilon_{2}\wedge\Upsilon_{3}\wedge\Upsilon_{4}$
such that

$\displaystyle\Upsilon_{1}$ $\displaystyle=\forall x\forall y\;\neg
A(x)\Rightarrow(R(x,y)\Leftrightarrow B^{R}(x,y))$ $\displaystyle\Upsilon_{2}$
$\displaystyle=\forall x\forall y\;(A(x)\wedge B^{R}(x,y))\Rightarrow
U^{R}(y))$ $\displaystyle\Upsilon_{3}$ $\displaystyle=(|U^{R}|=k)$
$\displaystyle\Upsilon_{4}$ $\displaystyle=\forall
x\exists^{=k}y\;B^{R}(x,y),$

where $U^{R}/1$ and $B^{R}/2$ are fresh predicates not appearing anywhere
else. Then, it holds that

$\textup{WFOMC}(\Gamma\wedge\Psi,n,w,\overline{w})=\frac{1}{\binom{n}{k}}\textup{WFOMC}(\Gamma\wedge\Upsilon,n,w,\overline{w}).$

Algorithm 1 shows how to combine the lemmas above to reduce WFOMC over
$\textbf{C}^{2}$ to WFOMC over $\textbf{UFO}^{2}+\textbf{CC}$.

Algorithm 1 Converts $\textbf{C}^{2}$ formulas into
$\textbf{UFO}^{2}+\textbf{CC}$

Input: Sentence $\Gamma\in\textbf{C}^{2}{}$
Output: Sentence $\Gamma^{*}\in\textbf{UFO}^{2}+\textbf{CC}{}$

1: for all sentence $\exists^{=k}x\;\psi(x)$ in $\Gamma$ do

2: Apply Lemma 3

3: end for

4: for all sentence $\forall x\exists^{=k}y\;\psi(x,y)$ in $\Gamma$ do

5: Apply Lemma 4

6: end for

7: for all subformula $\varphi(x)=\exists^{=k}y\;\psi(x,y)$ in $\Gamma$ do

8: Create new predicates $R/2$ and $A/1$

9: Let $\mu\leftarrow\forall x\forall y\;R(x,y)\Leftrightarrow\psi(x,y)$

10: Let $\nu\leftarrow\forall x\;A(x)\Leftrightarrow(\exists^{=k}y\;R(x,y))$

11: Apply Lemmas 2, 5 and 4 to $\nu$

12: Replace $\varphi(x)$ by $A(x)$

13: Append $\mu\wedge\nu$ to $\Gamma$

14: end for

15: for all sentence with an existential quantifier in $\Gamma$ do

16: Apply Lemma 1

17: end for

18: return $\Gamma$

##  3 An Upper Bound for Existing Techniques

As we have already mentioned above, WFOMC($\varphi,n,w,\overline{w}$) for
$\varphi\in\textbf{FO}^{2}+\textbf{CC}\;$ can be computed in time
$\mathcal{O}(n^{p+1+\alpha})$, where $p$ is the number of valid cells of
$\varphi$ (Beame et al., 2015; Kuželka, 2021) and
$\alpha=\prod_{i=1}^{m}{\left(arity(R_{i})+1\right)}$ with
$R_{1},R_{2},\ldots,R_{m}$ being all the predicates appearing in cardinality
constraints. Let us see, how the bound increases when we try computing WFOMC
over $\textbf{C}^{2}$.

###  3.1 A Worked Example on Removing Counting Quantifiers

To be able to compute WFOMC of a particular $\textbf{C}^{2}$ sentence, we must
first encode the sentence in $\textbf{UFO}^{2}+\textbf{CC}$. Let us start with
an example of applying Algorithm 1 to do just that.

Consider computing WFOMC($\varphi,n,w,\overline{w}$) for the sentence

$\varphi=\exists^{=k}x\exists^{=l}y\;\psi(x,y),$ (1)

where $\psi$ is a quantifier-free formula from the two-variable fragment and
$k,l\in\mathds{N}$.

First, let us introduce two new fresh predicates, namely $R/2$ and $P/1$. The
predicate $R$ will replace the formula $\psi$ and $P$ will do the same for the
counting subformula $\exists^{=l}y\;\psi(x,y)$. Specifically, we obtain

$\displaystyle\varphi^{(1)}$ $\displaystyle=\left(\exists^{=k}x\;P(x)\right)$
(2) $\displaystyle\wedge\left(\forall
x\;P(x)\Leftrightarrow\left(\exists^{=l}y\;R(x,y)\right)\right).$ (3)
$\displaystyle\wedge\left(\forall x\forall
y\;R(x,y)\Leftrightarrow\psi(x,y)\right)$ (4)

While Sentence 2 is already easily encoded using a single cardinality
constraint as Lemma 3 suggests, Sentence 3 requires more work. Let us split
the sentence into two implications:

$\displaystyle\varphi^{(2)}$
$\displaystyle=\left(|P|=k\right)\wedge\left(\forall x\forall
y\;R(x,y)\Leftrightarrow\psi(x,y)\right)$ (5)
$\displaystyle\wedge\left(\forall
x\;P(x)\Rightarrow\left(\exists^{=l}y\;R(x,y)\right)\right)$ (6)
$\displaystyle\wedge\left(\forall
x\;P(x)\Leftarrow\left(\exists^{=l}y\;R(x,y)\right)\right).$ (7)

Sentence 6 can easily be rewritten into a form processable by Lemma 5, whereas
Sentence 7 will first need to be transformed using Lemma 2, since the sentence
can be rewritten as

$\displaystyle\forall x\;P(x)\vee\neg\left(\exists^{=l}y\;R(x,y)\right).$

After applying Lemma 2, we obtain

$\displaystyle\varphi^{(3)}$
$\displaystyle=\left(|P|=k\right)\wedge\left(\forall x\forall
y\;R(x,y)\Leftrightarrow\psi(x,y)\right)$ (8)
$\displaystyle\wedge\left(\forall
x\;\overline{P}(x)\vee\left(\exists^{=l}y\;R(x,y)\right)\right)$ (9)
$\displaystyle\wedge\left(\forall
x\;C(x)\vee\left(\exists^{=l}y\;R(x,y)\right)\right)$ (10)
$\displaystyle\wedge\left(\forall
x\;D(x)\vee\left(\exists^{=l}y\;R(x,y)\right)\right)$ (11)
$\displaystyle\wedge\left(C(x)\vee D(x)\right)\wedge\left(\forall
x\;\overline{P}(x)\Leftrightarrow\neg P(x)\right),$ (12)

with $\overline{w}(D)=-1$. Apart from applying Lemma 2, we also introduced
another fresh predicate $\overline{P}/1$ which wraps the negation of $P$ for
brevity further down the line.

Next, we need to apply Lemma 5 three times, to Sentences 9 through 11. The
repetitions can, luckily, be avoided. By the distributive property of
conjunctions and disjunctions, we can _factor_ $\overline{P}/1,C/1$ and $D/1$
out from the sentences, thus obtaining

$\displaystyle\varphi^{(4)}$
$\displaystyle=\left(|P|=k\right)\wedge\left(\forall x\forall
y\;R(x,y)\Leftrightarrow\psi(x,y)\right)$ (13)
$\displaystyle\wedge\left(\forall x\;F(x)\Leftrightarrow\left(C(x)\vee
D(x)\vee\overline{P}(x)\right)\right)$ (14) $\displaystyle\wedge\left(\forall
x\;F(x)\vee\left(\exists^{=l}y\;R(x,y)\right)\right)$ (15)
$\displaystyle\wedge\left(C(x)\vee D(x)\right)\wedge\left(\forall
x\;\overline{P}(x)\Leftrightarrow\neg P(x)\right),$ (16)

Let us denote $\mathcal{T}_{l}(K,L)$ the transformation result when applying
Lemma 5 to a sentence

$\displaystyle\left(\forall
x\;K(x)\vee\left(\exists^{=l}y\;L(x,y)\right)\right),$

which is now the form of Sentence 15. After that application, our original
sentence $\varphi$ becomes

$\displaystyle\varphi^{(5)}$
$\displaystyle=\left(|P|=k\right)\wedge\left(\forall x\forall
y\;R(x,y)\Leftrightarrow\psi(x,y)\right)$
$\displaystyle\wedge\mathcal{T}_{l}(F,R)\wedge\left(\forall
x\;F(x)\Leftrightarrow\left(C(x)\vee D(x)\vee\overline{P}(x)\right)\right)$
$\displaystyle\wedge\left(C(x)\vee D(x)\right)\wedge\left(\forall
x\;\overline{P}(x)\Leftrightarrow\neg P(x)\right).$

We are still not done. The result of Lemma 5 still contains another counting
quantifier. Specifically, the sentence $\mathcal{T}_{l}(K,L)$ contains the
subformula

$\displaystyle\forall x\exists^{=l}y\;B^{L}(x,y),$

where $B^{L}/2$ is a fresh predicate. We need Lemma 4 to get rid of this
counting construct. Using said lemma will turn $\mathcal{T}_{l}(K,L)$ into

$\displaystyle\mathcal{T}^{\prime}_{l}(K,L)$ $\displaystyle=\forall x\forall
y\;\neg K(x)\Rightarrow\left(L(x,y)\Leftrightarrow B^{L}(x,y)\right)$ (17)
$\displaystyle\wedge\forall x\forall y\;(K(x)\wedge B^{L}(x,y))\Rightarrow
U^{L}(y))$ (18)
$\displaystyle\wedge\left(|U^{L}|=l\right)\wedge\left(|B^{L}|=n\cdot l\right)$
(19) $\displaystyle\wedge\forall x\forall
y\;B^{L}(x,y)\Leftrightarrow\bigvee_{i=1}^{l}f_{i}(x,y)$ (20)
$\displaystyle\wedge\bigwedge_{1\leq i<j\leq l}\left(\forall x\forall
y\;f_{i}(x,y)\Rightarrow\neg f_{j}(x,y)\right)$ (21)
$\displaystyle\wedge\bigwedge_{i=1}^{l}\left(\forall x\exists
y\;f_{i}(x,y)\right).$ (22)

We have obtained an $\textbf{FO}^{2}+\textbf{CC}$ sentence. Unfortunately, we
are still unable to directly compute WFOMC for such a formula either. The
problem lies in the $l$ sentences making up Formula 22, each containing an
existential quantifier. Following Lemma 1, we can replace each $\forall
x\exists y\;f_{i}(x,y)$ with $\forall x\forall y\;\neg f_{i}(x,y)\vee
A_{i}(x)$, where $A_{i}/1$ is a fresh predicate with $\overline{w}(A_{i})=-1$
for each $i$. Denote $\mathcal{T}^{\prime\prime}_{l}(K,L)$ the result of
applying such change to $\mathcal{T}^{\prime}_{l}(K,L)$. Finally, we obtain a
$\textbf{UFO}^{2}+\textbf{CC}$ sentence

$\displaystyle\varphi^{*}$
$\displaystyle=\left(|P|=k\right)\wedge\left(\forall x\forall
y\;R(x,y)\Leftrightarrow\psi(x,y)\right)$
$\displaystyle\wedge\mathcal{T}^{\prime\prime}_{l}(F,R)\wedge\left(\forall
x\;F(x)\Leftrightarrow\left(C(x)\vee D(x)\vee\overline{P}(x)\right)\right)$
$\displaystyle\wedge\left(C(x)\vee D(x)\right)\wedge\left(\forall
x\;\overline{P}(x)\Leftrightarrow\neg P(x)\right).$

###  3.2 Deriving the Upper Bound

As one can observe, the formula $\varphi^{*}$ in the example above has grown
considerably, compared to its original form. The question is whether the
formula growth can influence the asymptotic bound from Theorem 1. At first
glance, the answer may seem negative. That is due to the fact that the
transformation only extends the vocabulary (which is assumed to be fixed),
adds cardinality constraints (which are concentrated in the function $\alpha$)
and increases length of the input formula (which is also a constant with
respect to $n$). However, there is one caveat to be aware of. When extending
the vocabulary, we may introduce new valid cells. The vocabulary is fixed once
WFOMC computation starts, but if we have formula $\Gamma\wedge\Phi$ such that
$\Gamma\in\textbf{FO}^{2}+\textbf{CC}{}$ and $\Phi\in\textbf{C}^{2}{}$, then
this formula already has $p$ valid cells. Once we construct
$\Gamma\wedge\Phi^{*}$, where $\Phi^{*}\in\textbf{FO}^{2}+\textbf{CC}{}$ is
obtained from $\Phi$ in the similar manner as $\varphi^{*}$ is constructed
from $\varphi$, the new formula will have $p^{*}$ valid cells and, possibly,
$p\leq p^{*}$. If we wish to express a complexity bound for $\textbf{C}^{2}$,
we should inspect the possible increase in $p$ to obtain $p^{*}$ .

To deal with an arbitrary $\textbf{C}^{2}$ formula, we need to be able to deal
with subformulas such as the one in Sentence 3. As one can observe from both
the example above and Algorithm 1, encoding such a sentence in universally
quantified $\textbf{FO}^{2}+\textbf{CC}$ requires, in order of appearance,
Lemmas 2, 5, 4 and 1. Applying Lemmas 2 and 5 introduces only a constant
number of fresh predicates. Hence, the increase in $p$ can be expressed by
multiplication with a constant $\beta$. See the proof of Theorem 2 for
derivation of a value for $\beta$.

Although the constant $\beta$ may increase our polynomial degree considerably,
there is another, much more substantial, influence. An application of Lemma 4,
which additionally requires Lemma 1 to deal with _unskolemized_ formulas such
as in Formula 22 will introduce $2k$ new predicates. Although $k$ is a
parameter of the counting quantifiers, i.e., part of the language, and the
language is assumed to be fixed, the size of the encoding of $\textbf{C}^{2}$
in $\textbf{FO}^{2}+\textbf{CC}$ obviously depends on $k$. Hence, the number
of cells may also increase with respect to $k$, and, as we formally state
below, it in fact does.

######  Lemma 6.

For any $m\in\mathds{N}$, there exists a sentence
$\Gamma=\varphi\wedge\bigwedge_{i=1}^{m}\left(\forall
x\exists^{=k_{i}}y\;\psi_{i}(x,y)\right)$ such that the universally quantified
$\textbf{FO}^{2}+\textbf{CC}$ encoding of $\Gamma$ obtained using Lemma 4 has
$\mathcal{O}(\prod_{i=1}^{m}\gamma(k_{i})\cdot p)$ valid cells, where $p$ is
the number of valid cells of $\varphi$ and $\gamma(k)=(k+2)\cdot 2^{k-1}$.

###### Proof.

Consider the sentence

$\displaystyle\Gamma=$ $\displaystyle\bigwedge_{i=1}^{m}\left(\forall x\forall
y\;E_{i}(x,y)\Rightarrow E_{i}(y,x)\right)\wedge$ (23)
$\displaystyle\bigwedge_{i=1}^{m}\left(\forall
x\exists^{=k_{i}}E_{i}(x,y)\right).$ (24)

In this setting, $\varphi$ is Formula 23 and it has $p=2^{m}$ valid cells. We
need to apply Lemma 4 $m$ times to encode sentences in Formula 24 into
$\textbf{FO}^{2}+\textbf{CC}$. Let us investigate one such application.

First, consider valid cells of $\varphi$, that contain $E_{i}(x,x)$
negatively. Then all $f_{ij}(x,x)$ must also be negative (the index $j$ now
refers to the predicates introduced in a single application of Lemma 4), which
will immediately satisfy all _skolemization clauses_ obtained by application
of Lemma 1. Hence, the atoms $A_{ij}(x)$ will be allowed to be present either
positively or negatively for all $j$. Thus, the number of such cells will
increase $2^{k_{i}}$ times.

Second, consider valid cells of $\varphi$, that contain $E_{i}(x,x)$
positively. Then exactly one of $f_{ij}(x,x)$ can be satisfied in each cell.
That will cause the number of cells to be multiplied by $k_{i}$. Next, for a
particular cell, denote $t$ the index such that $f_{it}(x,x)$ is positive in
that cell. Then all $A_{ij}(x)$ such that $j\neq t$ will again be free to
assume either positive or a negative form. Only $A_{it}(x)$ will be fixed to
being positive. Hence, the number of such cells will further be multiplied by
$2^{k_{i}-1}$.

Overall, for a single application of Lemma 4, the number of cells will be
$\mathcal{O}(2^{k_{i}}\cdot p+k_{i}\cdot 2^{k_{i}-1}\cdot
p)\in\mathcal{O}((k_{i}+2)\cdot 2^{k_{i}-1}\cdot p)$, where we upper bound
both partitions of the valid cells of $\varphi$ by their total number. After
repeated application of Lemmas 4 and 1, the bound above directly leads to the
bound we sought to prove.333In the proof, we opted for as simple formula as
possible. It would be easy to handle computing WFOMC for $\Gamma$ by
decomposing the problem into $m$ identical and independent problems. It is,
however, also easy to envision a case where such decomposition is not as
trivial. Consider adding constraints such that for each $x$ and $y$, there is
only one $i$ such that $E_{i}(x,y)$ is satisfied. ∎

One last consideration for dealing with all of $\textbf{C}^{2}$ is Lemma 3.
The lemma adds one new cardinality constraint to the formula, which does not
increase number of cells in any way. It will, however, require more calls to
an oracle for WFOMC over $\textbf{FO}^{2}$. That influence on the overall
bound can still be concentrated in the function $\alpha$. To distinguish the
values from before encoding $\textbf{C}^{2}$ and after, let us denote the new
value $\alpha^{\prime}$.

Finally, we are ready to state the overall time complexity bound for computing
WFOMC over $\textbf{C}^{2}$.

######  Theorem 2.

Consider an arbitrary $\textbf{C}^{2}{}$ sentence rewritten as

$\varphi=\Gamma\wedge\bigwedge_{i=1}^{m}\left(\forall
x\;P_{i}(x)\Leftrightarrow\left(\exists^{=k_{i}}y\;R_{i}(x,y)\right)\right),$

where $\Gamma\in\textbf{FO}^{2}+\textbf{CC}$. For any $n\in\mathds{N}$ and any
fixed weights $(w,\overline{w})$, $\textup{WFOMC}(\varphi,n,w,\overline{w})$
can be computed in time $\mathcal{O}(n^{\alpha^{\prime}}\cdot
n^{1+\prod_{i=1}^{m}\beta\cdot\gamma(k_{i})\cdot p})$, where $p$ is the number
of valid cells of $\Gamma$, and $\alpha^{\prime}$ and $\beta$ are constants
with respect to both $n$ and each $k_{i}$.

###### Proof.

Suppose that

$\displaystyle\Gamma$
$\displaystyle=\psi\wedge\bigwedge_{i=1}^{m_{1}}(|Q_{i}|=l_{i})$

with $\psi\in\textbf{FO}^{2}{}$ and $Q_{i}$ being predicates from the
vocabulary of $\psi$. Consider encoding a single $\textbf{C}^{2}$ sentence

$\displaystyle\mu_{i}=\left(\forall
x\;P_{i}(x)\Leftrightarrow\left(\exists^{=k_{i}}y\;R_{i}(x,y)\right)\right)$

into $\textbf{UFO}^{2}+\textbf{CC}$ using Algorithm 1.

First, we apply Lemma 2 and leverage distributive law obtaining

$\displaystyle\mu^{(1)}_{i}$ $\displaystyle=\left(\forall x\;C(x)\vee
D(x)\right)\wedge\left(\forall x\;\overline{P_{i}}(x)\Leftrightarrow\neg
P_{i}(x)\right)$ $\displaystyle\wedge\left(\forall
x\;A(x)\Leftrightarrow\left(C(x)\vee
D(x)\vee\overline{P_{i}}\right)\right)\wedge\left(\forall
x\;A(x)\vee\left(\exists^{=k_{i}}y\;R_{i}(x,y)\right)\right),$

with $C/1,D/1$ and $A/1$ being fresh predicates and $\overline{w}(D)=-1$.
Second, using Lemma 5, we construct

$\displaystyle\mu^{(2)}_{i}$ $\displaystyle=\left(\forall x\;C(x)\vee
D(x)\right)\wedge\left(\forall x\;\overline{P_{i}}(x)\Leftrightarrow\neg
P_{i}(x)\right)\wedge\left(\forall x\;A(x)\Leftrightarrow\left(C(x)\vee
D(x)\vee\overline{P_{i}}\right)\right)$ $\displaystyle\wedge\left(\forall
x\forall y\;\neg A(x)\Rightarrow\left(R_{i}(x,y)\Leftrightarrow
B^{R_{i}}(x,y)\right)\right)\wedge\left(\forall x\forall y\;\left(A(x)\wedge
B^{R_{i}}(x,y)\right)\Rightarrow U^{R_{i}}(y)\right)$
$\displaystyle\wedge\left(|U^{R_{i}}|=k_{i}\right)\wedge\left(\forall
x\exists^{=k_{i}}y\;B^{R_{i}}(x,y)\right),$

where $U^{R_{i}}/1$ and $B^{R_{i}}/2$ are also fresh predicates.

Let us now inspect, how the number of cells may have increased so far. If the
original formula had $p$ valid cells, then after application of Lemma 2, there
may be up to $4p$ cells. To show that, consider partitioning valid cells into
those that satisfy the subformula $\psi(\textbf{x})$ considered by Lemma 2 and
those that do not. In the former case, the new cells must satisfy both $C(x)$
and $D(x)$, thus the number of cells remains unchanged. In the latter case,
$C(x)$ or $D(x)$ must be satisfied, leading to a factor of three. Hence, we
have an upper bound of $p+3p=4p$.

Similarly for Lemma 5, in cells that do not satisfy $A(x)$, $B^{R}(x,x)$ is
determined, but $U^{R}(x)$ is unconstrained, leading to a factor of two. In
the other cells, if $B^{R}(x,x)$ is also satisfied, then $U^{R}(x)$ is
determined, but it is unconstrained if $B^{R}(x,x)$ is satisfied, which can be
upper bounded by considering only the second case, leading to another factor
of two. Hence, we have another factor of $2+2=4$. Overall, in the worst case,
the increase in the number of cells by Lemmas 2 and 5 is by a factor of

$\displaystyle\beta=8,$

which will be applied each time we process one sentence $\mu_{i}$.

Next, let us investigate applying Lemmas 4 and 1 to $\mu^{(2)}_{i}$ which
produces

$\displaystyle\mu_{i}^{(3)}$ $\displaystyle=\left(\forall x\;C(x)\vee
D(x)\right)\wedge\left(\forall x\;\overline{P_{i}}(x)\Leftrightarrow\neg
P_{i}(x)\right)\wedge\left(\forall x\;A(x)\Leftrightarrow\left(C(x)\vee
D(x)\vee\overline{P_{i}}\right)\right)$ $\displaystyle\wedge\left(\forall
x\forall y\;\neg A(x)\Rightarrow\left(R_{i}(x,y)\Leftrightarrow
B^{R_{i}}(x,y)\right)\right)\wedge\left(\forall x\forall y\;\left(A(x)\wedge
B^{R_{i}}(x,y)\right)\Rightarrow U^{R_{i}}(y)\right)$
$\displaystyle\wedge\left(|U^{R_{i}}|=k_{i}\right)\wedge\left(|B^{R_{i}}|=n\cdot
k_{i}\right)$ $\displaystyle\wedge\left(\forall x\forall
y\;B^{R_{i}}(x,y)\Leftrightarrow\bigvee_{i=1}^{k_{i}}f_{i}(x,y)\right)\wedge\bigwedge_{1\leq
i<j\leq k_{i}}\left(\forall x\forall y\;f_{i}(x,y)\Rightarrow\neg
f_{j}(x,y)\right)$ $\displaystyle\wedge\bigwedge_{i=1}^{l}\left(\forall
x\forall y\;\neg f_{i}(x,y)\vee A_{i}(x)\right),$

where $f_{i}/2$ and $A_{i}/1$ are fresh predicates with
$\overline{w}(A_{i})=-1$. It follows from Lemma 6 that application of Lemmas 4
and 1 may increase the number of valid cells by a factor of

$\displaystyle\gamma(k_{i})=(k_{i}+2)\cdot 2^{k_{i}-1}.$

The factor is an upper bound due to the fact that the sentence $\Gamma$ shown
in the proof of Lemma 6 affords the atoms with he predicates $f_{i}$ and
$A_{i}$ the highest possible number of degrees of freedom. The truth values of
the atoms are determined only by sentences added through application of Lemmas
4 and 1. Therefore, there cannot be more valid cells.

Finally, assuming that each $\mu_{i}$ is encoded into
$\textbf{FO}^{2}+\textbf{CC}$ independently of others, we can substitute all
values into the bound from Theorem 1 obtaining the bound from our claim.

One thing remaining is to evaluate the factor related to the cardinality
constraints in our final formula and make sure it is a constant with respect
to both $n$ and the counting parameters. Following Kuželka (2021), the factor
is

$\displaystyle\alpha^{\prime}$
$\displaystyle=\left(\sum_{i=1}^{m}arity(U^{R_{i}})+arity(B^{R_{i}})\right)+\left(\sum_{i=1}^{m_{1}}arity(Q_{i})+1\right)=3m+m_{1}+\sum_{i=1}^{m_{1}}arity(Q_{i}).$

∎

##  4 Improving the Upper Bound

Let us now inspect the bound from Theorem 2. Although it is polynomial in $n$,
meaning that $\textbf{C}^{2}{}$ is in fact domain-liftable (Kuželka, 2021), we
can see that the number of valid cells (a part of the polynomial’s degree)
grows exponentially with respect to the counting parameters $k_{i}$. In this
section, we propose an improved encoding to the one from Lemma 4 which reduces
said growth to a quadratic one.

The new encoding does not build on entirely new principles, instead, it takes
the existing transformation and makes it more efficient. Same as in Lemma 4,
we will describe the situation for dealing with one $\forall\exists^{=k}$
subformula. The procedure could easily be generalized to having
$m\in\mathds{N}$ such subformulas by repeating the process for each of them
independently.

The largest issue with the current encoding are the _Skolemization_ predicates
$A_{i}/1$ which increase the number of valid cells exponentially with respect
to $k$. The new encoding will seek to constrain those predicates so that the
increase is reduced. Let us start with a formula

$\displaystyle\Gamma=\varphi\wedge\forall x\exists^{=k}y\;\psi(x,y),$ (25)

where $\varphi\in\textbf{FO}^{2}+\textbf{CC}{}$ and $\psi$ is quantifier-free.
Let us also consider the encoding of $\Gamma$ in a universally quantified
$\textbf{FO}^{2}+\textbf{CC}$, i.e.,

$\displaystyle\Gamma^{*}$ $\displaystyle=\varphi\wedge\left(\forall x\forall
y\;R(x,y)\Leftrightarrow\psi(x,y)\right)\wedge(|R|=k)$
$\displaystyle\wedge\left(\forall x\forall
y\;R(x,y)\Leftrightarrow\bigvee_{i=1}^{k}f_{i}(x,y)\right)$
$\displaystyle\wedge\bigwedge_{1\leq i<j\leq k}\left(\forall x\forall
y\;f_{i}(x,y)\Rightarrow\neg f_{j}(x,y)\right)$
$\displaystyle\wedge\bigwedge_{i=1}^{k}\left(\forall x\forall y\;\neg
f_{i}(x,y)\vee A_{i}(x)\right),$

with fresh predicates $R/2,f_{i}/2$ and $A_{i}/1$ and weights
$\overline{w}(A_{i})=-1$ for all $i\in\left[k\right]$.

###  4.1 Canonical Models

The new encoding will leverage a concept that we call a _canonical model_ ,
which we gradually build in this subsection.

Let $\omega$ be a model of $\Gamma^{*}$ and $t\in\Delta$ be an arbitrary
domain element. Denote $\mathcal{A}^{t}\subseteq\left[k\right]$ the set of
indices such that

$\displaystyle\omega\models\bigwedge_{j\in\mathcal{A}^{t}}A_{j}(t)\wedge\bigwedge_{j\in\left[k\right]\setminus\mathcal{A}^{t}}\neg
A_{j}(t).$

Now, let us transform $\omega$ into $\omega_{t}$ which will be another model
of $\Gamma^{*}$.

First, we separate all atoms in $\omega$ (atoms true in $\omega$) without the
predicates $f_{i}/2$ and $A_{i}/1$ into the set $\mathcal{R}_{0}$, and atoms
from $\omega\setminus\mathcal{R}_{0}$ not containing the constant $t$ into
$\mathcal{R}_{1}$. Second, we define an auxiliary injective function
$g:\mathcal{A}^{t}\mapsto\left[k\right]$ mapping elements of $\mathcal{A}^{t}$
to the first $|\mathcal{A}^{t}|$ positive integers, i.e.,

$\displaystyle g(j)=|\\{j^{\prime}\in\mathcal{A}^{t}\;|\;j^{\prime}\leq
j\\}|.$

Third, we define a set of atoms $\mathcal{A}^{new}$ such that

$\displaystyle\mathcal{A}^{new}=\\{A_{{g(j)}}(t)\;|\;\omega\models
A_{j}(t)\\},$

i.e., we accumulate the Skolemization atoms with the constant $t$ that are
satisfied in $\omega$ and we change their indices to the first
$|\mathcal{A}^{t}|$ positive integers. Next, we do a similar thing for atoms
with $f_{i}$’s. Note, that we use the same function $g$ as for
$\mathcal{A}^{t}$. Hence, we construct a set

$\displaystyle\mathcal{F}^{new}=\\{f_{{g(j)}}(t,t^{\prime})\;|\;\omega\models
f_{j}(t,t^{\prime}),t^{\prime}\in\Delta\\}.$

Finally, we are ready to define the new model of $\Gamma^{*}$ as

$\displaystyle\omega_{t}=\mathcal{R}_{0}\cup\mathcal{R}_{1}\cup\mathcal{A}^{new}\cup\mathcal{F}^{new}.$

######  Lemma 7.

For any $\omega\models\Gamma^{*}$ and any $t\in\Delta$, $\omega_{t}$
constructed as described above is another model of $\Gamma^{*}$.

###### Proof.

To prove the claim, it is sufficient to note that we can permute the indices
$i$ and the sentence $\Gamma^{*}$ will remain the same. The transformation
simply permutes the indices so that the satisfied atoms with predicates
$A_{i}$ and the constant $t$ have the lowest possible indices. ∎

Now, suppose that we take some model of $\Gamma^{*}$ and we repeatedly perform
the transformation described above for all domain elements, i.e., for some
ordering of the domain such as $\Delta=\\{t_{1},t_{2},\ldots,t_{n}\\}$, we
construct $\omega_{t_{1}}$ from $\omega$, then we construct $\omega_{t_{2}}$
from $\omega_{t_{1}}$ etc., until we obtain $\omega_{t_{n}}=\omega^{*}$. Note
that there can be several models $\omega$ that lead to the same $\omega^{*}$,
thus $\omega^{*}$ effectively induces an equivalence class.

######  Definition 4.

A model $\omega^{*}$ constructed in the way described above is a _canonical
model_ of $\Gamma^{*}$. Moreover, all models of $\Gamma^{*}$ that lead to the
same canonical model are called _A-equivalent_.444The letter “A” simply refers
to the Skolemization predicates that we call $A_{i}$, although they could be
called anything else.

A property of A-equivalent models will be useful in what follows. We formalize
it as another lemma.

######  Lemma 8.

Let $\omega^{*}$ be a canonical model of $\Gamma^{*}$. There are

$\displaystyle\prod_{t\in\Delta}\binom{k}{|\mathcal{A}^{t}|}$ (26)

models that are A-equivalent to $\omega^{*}$. Moreover, any two A-equivalent
models have the same weight.

###### Proof.

It follows from the proof of Lemma 7 that the atoms of $A_{i}$’s that are true
in $\omega^{*}$ have the lowest possible indices. Hence, for a fixed
$t\in\Delta$, the number of models that lead to $\omega^{*}$ depends only on
the number of ways that we can split the indices between the satisfied and
unsatisfied atoms. There are $k$ indices to choose from and, for a fixed
assignment, the set $\mathcal{A}^{t}$ holds the indices of satisfied
$A_{j}(t)$’s, which leads directly to Equation 26.

The second claim follows from the fact that the transformation of any $\omega$
into $\omega^{*}$ does not change the number of true atoms of any given
predicate. ∎

###  4.2 The New Encoding

In this subsection, we use the concept of canonical models and observations
from Lemma 8 to devise an encoding that counts only canonical models. By
weighing them accordingly, we then recover the correct weighted model count of
the original problem.

Let us start by introducing new fresh predicates $C_{i}/1$. We will want an
atom $C_{j}(t)$ to be true if and only if $A_{1}(t),A_{2}(t),\ldots A_{j}(t)$
were the only Skolemization atoms satisfied in a model of $\Gamma^{*}$ (the
old encoding). Intuitively, the predicates $C_{i}$ will constrain the models
to only correspond to canonical models. Thus, we define $C_{i}$’s as

$\displaystyle\Gamma_{C}=\bigwedge_{j=0}^{k}$ $\displaystyle\forall
x\;C_{j}(x)\Leftrightarrow\left(\bigwedge_{h\in\left[j\right]}A_{h}(x)\wedge\bigwedge_{h\in\left[k\right]\setminus\left[j\right]}\neg
A_{h}(x)\right).$

The new encoding can then be described as

$\displaystyle\Gamma^{new}=\Gamma^{*}\wedge\Gamma_{C}\wedge\left(\forall
x\;\bigvee_{j=0}^{k}C_{j}(x)\right).$ (27)

The final disjunction was added to make sure that we only count canonical
models (at least one of $C_{i}$’s is satisfied).

One more thing to consider are weights for the predicates $C_{i}$. A
particular atom $C_{j}(t)$ is satisfied in a model $\omega$, if the model is a
canonical model corresponding to $C_{j}(t)$ according to the sentence
$\Gamma_{C}$. Following Lemma 8, such model represents an entire set of
A-equivalent models, each with the same weight. Hence, if $C_{j}(t)$ is
satisfied, we should count the model weight of $\omega$ as many times as how
many A-equivalent models to $\omega$ there are. If $C_{j}(t)$ is, on the other
hand, unsatisfied, we do not want to change the weight in any way. Therefore,
we set $w(C_{i})=\binom{k}{i}$ and $\overline{w}(C_{i})=1$ for all
$i\in\left[k\right]$.

######  Lemma 9.

For any sentence $\Gamma\in\textbf{C}^{2}{}$ such as the one in Equation 25
and $\Gamma^{new}\in\textbf{FO}^{2}+\textbf{CC}{}$ obtained from $\Gamma$ as
in Equation 27, for any $n\in\mathds{N}$ and any weights $(w,\overline{w})$
extended for predicates $C_{i}$ as above, it holds that

$\displaystyle\textup{WFOMC}(\Gamma,n,w,\overline{w})=\frac{1}{(k!)^{n}}\textup{WFOMC}(\Gamma^{new},n,w,\overline{w}).$

###### Proof.

$\Gamma_{C}$ encodes each canonical model of $\Gamma^{*}$ using a single
$C_{j}$ predicate indicating that exactly $A_{1}(t),A_{2}(t),\ldots,A_{j}(t)$
are satisfied for any $t\in\Delta$. For all $i\in\\{0,1,\ldots,k\\}$,
$\Gamma_{C}$ allows at most one $C_{i}(t)$ to be true for any $t$. The
disjuction in $\Gamma^{new}$ requires at least one $C_{i}(t)$ to be true.
Combined, each model of $\Gamma^{new}$ is one of canonical models of
$\Gamma^{*}$. Hence, we are only counting canonical models of $\Gamma^{*}$.

It follows from Lemma 8 that for a canonical model $\omega$ represented by
$C_{i}$, there are $\binom{k}{i}$ models of $\Gamma^{*}$ that are A-equivalent
to $\omega$. Hence, when we have one canonical model, it represents
$\binom{k}{i}$ models that must all be considered to obtain the correct
weighted model count leading to the weight $w(C_{i})=\binom{k}{i}$ for each
$C_{i}$.

So far, we have shown that we are counting models of $\Gamma^{*}$. However, we
must still deal with the over counting introduced by using Lemma 4 to turn
$\Gamma$ into $\Gamma^{*}$. Therefore, we use the same factor as in Lemma 4 to
only count models of $\Gamma$. ∎

###  4.3 The Improved Upper Bound

With the new encoding, we can decrease the number of valid cells of a sentence
obtained after applying Lemma 4 to a $\textbf{C}^{2}$ sentence. Hence, we can
improve the upper bound on time complexity of computing WFOMC over
$\textbf{C}^{2}$. Using the same notation as in Theorem 2, we can formulate
Theorem 3.

######  Theorem 3.

Consider an arbitrary $\textbf{C}^{2}{}$ sentence rewritten as

$\varphi=\Gamma\wedge\bigwedge_{i=1}^{m}\left(\forall
x\;P_{i}(x)\Leftrightarrow\left(\exists^{=k_{i}}y\;R_{i}(x,y)\right)\right),$

where $\Gamma\in\textbf{FO}^{2}+\textbf{CC}$. For any $n\in\mathds{N}$ and any
fixed weights $(w,\overline{w})$, $\textup{WFOMC}(\varphi,n,w,\overline{w})$
can be computed in time $\mathcal{O}(n^{\alpha^{\prime}}\cdot
n^{1+\prod_{i=1}^{m}\beta\cdot\gamma^{\prime}(k_{i})\cdot p})$, where $p$ is
the number of valid cells of $\Gamma$ and
$\gamma^{\prime}(k)=\mathcal{O}(k^{2}+2k+1)$.

###### Proof.

Most of the proof is identical to the proof of Theorem 2. What remains is to
derive $\gamma^{\prime}$.

Let us return to the sentence from the proof of Lemma 6, i.e,

$\Gamma=\bigwedge_{i=1}^{m}\left(\forall x\forall y\;E_{i}(x,y)\Rightarrow
E_{i}(y,x)\right)\wedge\bigwedge_{i=1}^{m}\left(\forall
x\exists^{=k_{i}}E_{i}(x,y)\right).$

As we already know, sentence $\Gamma$ causes the largest increase in the
number of valid cells. With the old encoding, most of truth values of the
Skolemization atoms with predicates $A_{i}$ were unconstrained leading to an
exponential blowup. Due to Equation 27, that is no longer the case. The
sentence $\Gamma_{C}$ forces $C_{j}(t)$ to be true if and only if
$A_{1}(t),A_{2}(t),\ldots,A_{j}(t)$ are true and all other $A_{i}(t)$ with
$j<i\leq k$ are false. Hence, if $C_{j^{\prime}}(t)$ is true, then all other
$C_{j}(t)$ with $j^{\prime}\neq j$ are false. Moreover, at least one
$C_{i}(t)$ must be true due to the final disjunction in Equation 27.

Therefore, we only have $(k+1)$ possibilities, as how to assign truth values
to atoms with $C_{i}$ predicates. The truth values of atoms with $A_{i}$’s are
then directly determined without any more degrees of freedom. Hence, for both
cases considered in the proof of Lemma 6, we receive a factor $(k+1)$ instead
of the exponential. Thus, we obtain
$\gamma^{\prime}=\mathcal{O}((k+1)p+k(k+1)p)\in\mathcal{O}((k^{2}+2k+1)p)$. ∎

##  5 Experiments

In this section, we support our theoretical findings by providing time
measurements for various WFOMC computations using both the old and the new
$\textbf{C}^{2}$ encoding. We also provide tables comparing the number of
valid cells $p$, which determines the polynomial degree, giving a more
concrete idea on the speed-up provided by the new encoding.

For all of our experiments, we used _FastWFOMC.jl_ ,555https://github.com/jan-
toth/FastWFOMC.jl an open source Julia implementation of the FastWFOMC
algorithm (van Bremen and Kuželka, 2021a), which is arguably the state-of-the-
art, reported by its authors to outperform the first approach to computing
WFOMC in a lifted manner, i.e, ForcLIFT,666https://dtaid.cs.kuleuven.be/wfomc
which is based on knowledge compilation (Van den Broeck et al., 2011).

Apart from time measurements for $\textbf{C}^{2}$ sentences, we also inspect
sentences from one of the domain-liftable $\textbf{C}^{2}$ extensions, namely
$\textbf{C}^{2}$ with the linear order axiom (Tóth and Kuželka, 2023). Apart
from time measurements on sentences from that fragment, we also use it to
encode a Markov Logic Network and perform exact lifted inference therein.

Most of our experiments were performed in a single thread on a computer with
an AMD Ryzen 5 7500F CPU running at speeds 3.4GHz and 32 GB RAM. Problems
containing the linear order axiom, which have considerably higher memory
requirements, were solved using a machine with AMD EPYC 7742 CPU running at
speeds 2.25GHz and 512 GB of RAM.

###  5.1 Performace Measurements

####  5.1.1 Sentences with Counting Quantifiers

First, consider a $\textbf{C}^{2}$ sentence encoding $k$-regular undirected
graphs without loops, i.e.,

$\displaystyle\Gamma_{1}$ $\displaystyle=\left(\forall x\;\neg
E(x,x)\right)\wedge\left(\forall x\forall y\;E(x,y)\Rightarrow
E(y,x)\right)\wedge\left(\forall x\exists^{=k}y\;E(x,y)\right).$

In our experiments, we simply count the number of such graphs on $n$ vertices,
i.e., we set $w(E)=\overline{w}(E)=1$ and we compute
$\textup{WFOMC}(\Gamma_{1},n,w,\overline{w})$ for gradually increasing domain
sizes $n$. Since our new encoding is aimed at improving the runtime with
respect to the counting parameter $k$, we do the computation for several
different parameters $k$ as well.

Figure 1 shows the measured runtimes for $k\in\\{3,4,5\\}$. As one can
observe, the new encoding surpasses the old in each case. The difference may
not seem as distinct for $k=3$ compared to $k=4$ or $k=5$ but note that it is
still substantial. For one, runtime for $n=51$ already exceeded runtime of
$1000$ seconds in case of the old encoding, whereas the new encoding did not
reach that value even for $n=70$. Additionally to the figure, Table 1 shows
the number of valid cells $p_{old}$ produced by the old encoding of
$\Gamma_{1}$ into $\textbf{FO}^{2}+\textbf{CC}$ and $p_{new}$ produced by the
new one. As one can observe, e.g., for $k=5$, the new encoding reduces the
runtime from $\mathcal{O}(n^{33})$ to $\mathcal{O}(n^{7})$.

$k$ | 3 | 4 | 5
---|---|---|---
$p_{old}$ | 8 | 16 | 32
$p_{new}$ | 4 | 5 | 6
Table 1: Number of valid cells for $k$-regular graphs

(a) $3$-regular

(b) $4$-regular

(c) $5$-regular

Figure 1: Runtime for counting $k$-regular graphs

Next, we can extend the $k$-regular graph definition to also include a
coloring by $l$ colors, effectively obtaining a logical description of
$k$-regular $l$-colored graphs.777Note that $l$-colored graphs are graphs
along with a coloring using at most $l$ colors. That is different from
$l$-colorable graphs which is a set of graphs that can be colored using $l$
colors. Sentence $\Gamma_{2}$ encodes such graphs and we again count the
number of such graphs on larger and larger domains for various values $k$ and
$l$ using WFOMC.

$\displaystyle\Gamma_{2}$ $\displaystyle=\forall x\;\neg E(x,x)\wedge\forall
x\forall y\;E(x,y)\Rightarrow E(y,x)$ $\displaystyle\wedge\bigwedge_{1\leq
i<j\leq l}\left(\forall x\;C_{i}(x)\Rightarrow\neg C_{j}(x)\right)$
$\displaystyle\wedge\left(\forall x\forall
y\;E(x,y)\Rightarrow\left(\bigwedge_{i=1}^{l}\neg\left(C_{i}(x)\wedge
C_{i}(y)\right)\right)\right)$ $\displaystyle\wedge\forall
x\exists^{=k}y\;E(x,y)\wedge\forall x\;\bigvee_{i=1}^{l}C_{i}(x)$

The runtime measurements are available in Figure 2. Similarly to the previous
case, Table 2 shows number of valid cells for various scenarios, even for some
that are not included in Figure 2 due to their computational demands.

$l$ $k$ | 3 | 4 | 5
---|---|---|---
2 | 16 | 32 | 64
3 | 24 | 48 | 96
4 | 32 | 64 | 128
(a) Old encoding

$l$ $k$ | 3 | 4 | 5
---|---|---|---
2 | 8 | 10 | 12
3 | 12 | 15 | 18
4 | 16 | 20 | 24
(b) New encoding

Table 2: Number of valid cells for $k$-regular $l$-colored graphs

(a) $3$-regular $2$-colored

(b) $3$-regular $3$-colored

(c) $3$-regular $4$-colored

(d) $4$-regular $2$-colored

(e) $4$-regular $3$-colored

(f) $5$-regular $2$-colored

Figure 2: Runtime for counting $k$-regular $l$-colored graphs

In the examples so far, our $\textbf{C}^{2}$ sentences contained only one
$\forall\exists^{=k}$ sentence. Directed $k$-(bi)regular graphs without loops,
requiring both the number of outgoing and incoming edges to be exactly $k$ for
each vertex, contain two such counting sentences, putting larger emphasis on
our upper bounds. We encode such graphs in $\Gamma_{3}$:

$\displaystyle\Gamma_{3}$ $\displaystyle=\left(\forall x\;\neg
E(x,x)\right)\wedge\left(\forall
x\exists^{=k}y\;E(x,y)\right)\wedge\left(\forall
x\exists^{=k}y\;E(y,x)\right)$

Runtimes for counting over such digraphs may be inspected in Figure 3. Table 3
depicts valid cells counts, which turn out to be quite high. Due to those high
values, which end up being polynomial degrees in our upper bounds, the problem
is considerably more difficult. Even for $k=3$, the old encoding was extremely
inefficient, hence, we only provide runtimes for counting with the new
encoding in that case.888Note, that for the case of $k=3$, the corresponding
OEIS sequence at https://oeis.org/A007105 only contains elements up to $n=14$,
which is the same as we managed to compute within a time limit of $10^{5}$
seconds.

$k$ | 2 | 3 | 4 | 5
---|---|---|---|---
$p_{old}$ | 16 | 64 | 256 | 1024
$p_{new}$ | 9 | 16 | 25 | 36
Table 3: Number of valid cells for $k$-regular digraphs

(a) $2$-regular digraphs

(b) $3$-regular digraphs

Figure 3: Runtime for counting $k$-regular digraphs

####  5.1.2 Sentences with the Linear Order Axiom

We also consider sentences from the language of $\textbf{C}^{2}$ extended with
the linear order axiom, i.e., one of the known extensions of $\textbf{C}^{2}$
that is still domain-liftable (Tóth and Kuželka, 2023). Sentence $\Gamma_{4}$
encodes a graph similar to the Model A of the Barabási-Albert model (Albert
and Barabási, 2002), an algorithm for generating random networks.

$\displaystyle\Gamma_{4}$ $\displaystyle=\forall x\;Eq(x,x)$
$\displaystyle\wedge(|Eq|=n)$ $\displaystyle\wedge\exists^{=k+1}x\;K(x)$
$\displaystyle\wedge\forall x\;\neg R(x,x)$ $\displaystyle\wedge\forall
x\forall y\;K(x)\wedge K(y)\wedge\neg Eq(x,y)\Rightarrow R(x,y)$
$\displaystyle\wedge\forall x\exists^{=k}y\;R(x,y)$
$\displaystyle\wedge\forall x\forall y\;R(x,y)\wedge\neg\left(K(x)\wedge
K(y)\right)\Rightarrow y\leq x$ $\displaystyle\wedge\forall x\forall
y\;K(x)\wedge\neg K(y)\Rightarrow x\leq y$ $\displaystyle\wedge Linear(\leq)$

In a sense, the graph encoded by $\Gamma_{4}$ on $n$ vertices is gradually
_grown_. We start by ordering the vertices using the linear order axiom. Then,
a complete graph $K_{k+1}$ is formed on the first $k+1$ vertices. Afterwards,
we start growing the graph by _appending_ remaining vertices
$i\in\\{k+2,k+3,\ldots,n\\}$ one at a time. When appending a vertex $i$, we
introduce $k$ outgoing edges that can only connect to the vertices
$\\{1,2,\ldots,i-1\\}$, i.e., all the new edges have a form $(i,j)$ where
$j\in\\{1,2,\ldots,i-1\\}$. Ultimately, when counting the number of such
graphs, we may not be interested in the same solutions differing by vertex
ordering only, so we can divide the final number by $n!$. The ordering through
the linear order axiom is, however, a very useful modelling construct—without
it, modelling graphs such as the one above would likely not be possible in a
domain-lifted way.

From now on, let us refer to graphs defined by the sentence $\Gamma_{4}$ as
BA$(k)$. Figure 4 depicts the runtime for counting the graphs BA(3) on $n$
vertices using the old and the new encoding. The problems lead to 16 and 8
valid cells, respectively.

Figure 4: Runtime for counting BA(3) graphs

####  5.1.3 Closing Remarks on Performance

The experiments confirm that the new encoding is indeed more efficient,
outperforming the old encoding on all tested instances. While that should not
come as a surprise, since we have derived a bound provably better than the old
one, it is also not completely obvious because FastWFOMC uses many algorithmic
tricks that partially make up for the inefficiencies of the old encoding.
However, not even our new bound allowed us to compute WFOMC within reasonable
time for large domain sizes on all the tested problems.

Still, one should keep in mind that the alternative, that is solving WFOMC by
propositionalization to WMC, scales extremely poorly as was repeatedly shown
in the lifted inference literature (Meert et al., 2014). Thus, we must rely on
algorithms operating at the lifted level. Our work extends the domains that
can be efficiently handled by lifted algorithms, but more work is needed to
extend the reach of lifted inference algorithms further.

###  5.2 Lifted Inference in Markov Logic Networks

Markov Logic Networks (MLNs) are a popular first-order probabilistic language
based on undirected graphs (Richardson and Domingos, 2006). An MLN $\Phi$ is a
set of weighted first-order logic formulas (possibly with free variables) with
weights taking on values from the real domain or infinity:

$\Phi=\\{(w_{1},\alpha_{1}),(w_{2},\alpha_{2}),\ldots,(w_{m},\alpha_{m})\\}$

Given a domain $\Delta$, the MLN defines a probability distribution over
possible worlds such as

$\displaystyle
Pr_{\Phi,\Delta}(\omega)=\frac{\llbracket\omega\models\Phi_{\infty}\rrbracket}{Z}\exp\left(\sum_{(w_{i},\alpha_{i})\in\Phi_{\mathds{R}}}w_{i}\cdot
N(\alpha_{i},\omega)\right)$

where $\Phi_{\mathds{R}}$ denotes formulas with real-valued weights (soft
constraints), $\Phi_{\infty}$ denotes formulas with infinity-valued weights
(hard constraints), $\llbracket\cdot\rrbracket$ is the indicator function, $Z$
is the normalization constant ensuring valid probability values and
$N(\alpha_{i},\omega)$ is the number of substitutions to free variables of
$\alpha_{i}$ that produce a grounding of those free variables that is
satisfied in $\omega$.

Inference (and also learning) in MLNs is reducible to WFOMC (Van den Broeck et
al., 2014). It is thus possible to efficiently perform exact lifted inference
over an MLN using WFOMC as long as the network is encoded using a domain-
liftable language. The reduction works as follows: For each
$(w_{i},\alpha_{i}(\textbf{x}_{i}))\in\Phi_{\mathds{R}}$, introduce a new
formula
$\forall\textbf{x}_{i}:\xi_{i}(\textbf{x}_{i})\Leftrightarrow\alpha_{i}(\textbf{x}_{i})$,
where $\xi_{i}$ is a fresh predicate, and set
$w(\xi_{i})=\exp(w_{i}),\overline{w}(\xi_{i})=1$ and $w(Q)=\overline{w}(Q)=1$
for all other predicates $Q$. Formulas in $\Phi_{\infty}$ are added to the
theory as additional constraints. Denoting the new theory by $\Gamma$ and a
query by $\phi$, we can compute the inference as

$\displaystyle
Pr_{\Phi,\Delta}(\phi)=\frac{\textup{WFOMC}(\Gamma\wedge\phi,|\Delta|,w,\overline{w})}{\textup{WFOMC}(\Gamma,|\Delta|,w,\overline{w})}.$

We consider an MLN defined on the network BA($k$), i.e., encoded using the
sentence $\Gamma_{4}$. We extend the sentence with the predicate $Fr/2$
encoding undirected edges and we consider the standard MLN scenario where a
smoker’s friend is also a smoker. That property, however, does not hold
universally, instead, it is weighed, determining how important it is for an
interpretation to satisfy it. Putting it all together, we obtain an MLN in
$\Phi_{1}$, namely

$\displaystyle\Phi_{1}=\\{$ $\displaystyle\left(\infty,\forall
x\;Eq(x,x)\right),$ $\displaystyle\left(\infty,(|Eq|=n)\right),$
$\displaystyle\left(\infty,\exists^{=k+1}x\;K(x)\right),$
$\displaystyle\left(\infty,\forall x\;\neg R(x,x)\right),$
$\displaystyle\left(\infty,\forall x\forall y\;K(x)\wedge K(y)\wedge\neg
Eq(x,y)\Rightarrow R(x,y)\right),$ $\displaystyle\left(\infty,\forall
x\exists^{=k}y\;R(x,y)\right),$ $\displaystyle\left(\infty,\forall x\forall
y\;R(x,y)\wedge\neg\left(K(x)\wedge K(y)\right)\Rightarrow y\leq x\right),$
$\displaystyle\left(\infty,\forall x\forall y\;K(x)\wedge\neg K(y)\Rightarrow
x\leq y\right),$ $\displaystyle\left(\infty,Linear(\leq)\right),$
$\displaystyle\left(\infty,\forall x\forall
y\;Fr(x,y)\Leftrightarrow\left(R(x,y)\vee R(y,x)\right)\right),$
$\displaystyle\left(\ln w,Sm(x)\wedge Fr(x,y)\Rightarrow Sm(y)\right)\\}$

We will be interested in the probability of there being exactly $m$ smokers.
To put the result into some context, we will compare them to a situation,
where the underlying network is a random $k$-regular graph, i.e.,

$\displaystyle\Phi_{2}=\\{$ $\displaystyle\left(\infty,\forall x\;\neg
Fr(x,x)\right),$ $\displaystyle\left(\infty,\forall x\forall
y\;Fr(x,y)\Rightarrow Fr(y,x)\right),$ $\displaystyle\left(\infty,\forall
x\exists^{=k}y\;Fr(x,y)\right),$ $\displaystyle\left(\ln w,Sm(x)\wedge
Fr(x,y)\Rightarrow Sm(y)\right)\\}.$

Figure 5 shows the inference results for $n=8$ and various weights $w$. For
both graphs, the distribution starts as binomial for small $w$. Obviously, if
we do not care about satisfying the smoker-friend property, random assignment
of truth values to $Sm(t_{1}),Sm(t_{2}),\ldots,Sm(t_{n})$ will lead to a
binomial distribution.

As we increase the weight, the distributions gradually _reverse_ to the
opposite scenario, a U-shaped distribution that prefers the extremes. That is
also intuitive, as we mostly work with one connected component where everyone
is everyone’s friend. However, a random $3$-regular graph appears to go
through the uniform distribution whereas our BA model seems not to. That is
due to the fact that the BA model is, by construction, always one connected
component as opposed to a 3-regular graph that can also consist of two
connected components on $n=8$ vertices.

(a) $w=1$

(b) $w=\frac{3}{2}$

(c) $w=2$

(d) $w=5$

Figure 5: Probability of $m$ smokers

##  6 Related Work

This work builds on a long stream of results from the area of lifted inference
(Poole, 2003; de Salvo Braz et al., 2005; Jha et al., 2010; Gogate and
Domingos, 2011; Taghipour et al., 2013; Braun and Möller, 2016; Dilkas and
Belle, 2023). Particularly, we continue in the line of research into the task
of weighted first-order model counting (Van den Broeck et al., 2011; Van den
Broeck, 2011; Van den Broeck et al., 2014; Beame et al., 2015; Kazemi et al.,
2016; Kuusisto and Lutz, 2018; Kuželka, 2021; van Bremen and Kuželka, 2021b;
Tóth and Kuželka, 2023; Malhotra and Serafini, 2023; Malhotra et al., 2023).

To the best of our knowledge, there is no other literature available on the
exact complexity of computing WFOMC for $\textbf{C}^{2}$ sentences. The
closest resource is the one proving $\textbf{C}^{2}$ to be domain-liftable
(Kuželka, 2021), which we directly build upon and, in some sense, extend.
Another relevant resource, concerned with designing an efficient algorithm for
computing WFOMC over $\textbf{FO}^{2}$, is van Bremen and Kuželka (2021a)
whose FastWFOMC algorithm remains state-of-the-art and which can be used as a
WFOMC oracle required to deal with cardinality constraints.

##  7 Conclusion

The best existing bound for time complexity of computing WFOMC over
$\textbf{C}^{2}$ is polynomial in the domain size (Kuželka, 2021). However, as
we point out, the degree of the polynomial is exponential in the parameter $k$
of the counting quantifiers. Using the new techniques presented in this paper,
we reduce the dependency of the degree on $k$ to a quadratic one, thus
achieving super-exponential speedup of the WFOMC runtime with respect to the
counting parameter $k$.

The new encoding has the potential of improving any applications of WFOMC over
$\textbf{C}^{2}$, or making some applications tractable in the practical
sense. We support this statement further in an experimental section, where we
provide runtime measurements for computing WFOMC of several $\textbf{C}^{2}$
sentences and sentences from a domain-liftable $\textbf{C}^{2}$ extension.

It remains an open question whether the complexity can be reduced even
further. Thus, we only consider our new bound as a bound to beat and we
certainly hope that someone will beat it in the future.

## Acknowledgments

This work has received funding from the European Union’s Horizon Europe
Research and Innovation program under the grant agreement TUPLES No 101070149.
JT’s work was also supported by a CTU grant no. SGS23/184/OHK3/3T/13.

##  Appendix A Bit Complexity

All of the bounds presented in our paper assume mathematical operations to
take constant time, which is a common assumption when it comes to asymptotic
complexity. However, in the context of WFOMC, it is quite common that the
algorithm ends up working with extremely large values. Consider counting the
number of undirected graphs without loops on $n$ vertices, i.e., computing
WFOMC of a formula

$\displaystyle\varphi=\left(\forall x\;\neg E(x,x)\right)\wedge\left(\forall
x\forall y\;E(x,y)\Rightarrow E(y,x)\right)$

with $w(E)=\overline{w}(E)=1$. Then

$\displaystyle\textup{WFOMC}(\varphi,n,w,\overline{w})=2^{\binom{n}{2}}$

and for $n=12$, we already obtain

$\textup{WFOMC}(\varphi,n,w,\overline{w})=73786976294838206464,$

i.e., a value requiring more than 64 bits for its machine
representation,999The formula along with the value for $n=12$ can be checked
at https://oeis.org/A006125. leading to situations where bit complexity should
also be considered.

In Kuželka (2021), the author derives a bound on the number of bits required
to represent each summand in the WFOMC computation, which turns out to be
polynomial in $n$ and $\log M$, where $M$ is a bound on the number of bits
required to represent the weights. Total number of such summands is then also
polynomial in $n$. Thus, the polynomial bound for domain-liftability is not
violated.

The derivation itself is rather involved. We refer interested readers to
Proposition 2 and its proof in Kuželka (2021). For our purposes, it suffices
to say that the derivation would remain unchanged under our WFOMC
transformations.

## References

  * Albert and Barabási [2002] Réka Albert and Albert-László Barabási.  Statistical mechanics of complex networks.  Reviews of modern physics, 74(1):47, 2002.
  * Barvínek et al. [2021] 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 Inductive Logic Programming: 30th International Conference, ILP 2021, Virtual Event, October 25–27, 2021, Proceedings, page 17–25, Berlin, Heidelberg, 2021. Springer-Verlag.
  * 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, PODS ’15, page 313–328, New York, NY, USA, 2015. Association for Computing Machinery.
  * Braun and Möller [2016] Tanya Braun and Ralf Möller.  Lifted junction tree algorithm.  In KI 2016: Advances in Artificial Intelligence: 39th Annual German Conference on AI, Klagenfurt, Austria, September 26-30, 2016, Proceedings 39, pages 30–42. Springer, 2016.
  * de Salvo Braz et al. [2005] Rodrigo de Salvo Braz, Eyal Amir, and Dan Roth.  Lifted first-order probabilistic inference.  In Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, pages 1319–1325. Morgan Kaufmann San Francisco, 2005.
  * Dilkas and Belle [2023] Paulius Dilkas and Vaishak Belle.  Synthesising recursive functions for first-order model counting: Challenges, progress, and conjectures.  In Proceedings of the 20th International Conference on Principles of Knowledge Representation and Reasoning, KR 2023, Rhodes, Greece, September 2-8, 2023, pages 198–207, 2023.
  * Gogate and Domingos [2011] Vibhav Gogate and Pedro Domingos.  Probabilistic theorem proving.  In Proceedings of the Twenty-Seventh Conference on Uncertainty in Artificial Intelligence, UAI’11, page 256–265, Arlington, Virginia, USA, 2011. AUAI Press.
  * Hinrichs and Genesereth [2006] Timothy Hinrichs and Michael Genesereth.  Herbrand logic.  Technical Report LG-2006-02, Stanford University, Stanford, CA, 2006.  http://logic.stanford.edu/reports/LG-2006-02.pdf.
  * Jha et al. [2010] Abhay Jha, Vibhav Gogate, Alexandra Meliou, and Dan Suciu.  Lifted inference seen from the other side: The tractable features.  Advances in Neural Information Processing Systems, 23, 2010.
  * Kazemi et al. [2016] Seyed Mehran Kazemi, Angelika Kimmig, Guy Van den Broeck, and David Poole.  New liftable classes for first-order probabilistic inference.  In Proceedings of the 30th International Conference on Neural Information Processing Systems, NIPS’16, page 3125–3133, Red Hook, NY, USA, 2016. Curran Associates Inc.
  * 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, LICS 2018, pages 619–628, 2018.
  * Kuželka [2021] Ondřej Kuželka.  Weighted first-order model counting in the two-variable fragment with counting quantifiers.  Journal of Artificial Intelligence Research, 70:1281–1307, 2021.
  * Malhotra and Serafini [2023] Sagar Malhotra and Luciano Serafini.  Weighted first order model counting with directed acyclic graph axioms.  ArXiv, abs/2302.09830, 2023.
  * Malhotra et al. [2023] Sagar Malhotra, Davide Bizzaro, and Luciano Serafini.  Lifted inference beyond first-order logic.  ArXiv, abs/2308.11738, 2023.
  * Meert et al. [2014] Wannes Meert, Guy Van den Broeck, and Adnan Darwiche.  Lifted inference for probabilistic logic programs.  Technical report, KU Leuven and University of California, 2014.
  * Meert et al. [2016] Wannes Meert, Jonas Vlasselaer, and Guy Van den Broeck.  A relaxed tseitin transformation for weighted model counting.  In International Workshop on Statistical Relational AI, February 2016.
  * Poole [2003] David Poole.  First-order probabilistic inference.  In Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence, volume 3, pages 985–991, 2003.
  * Richardson and Domingos [2006] Matthew Richardson and Pedro Domingos.  Markov logic networks.  Machine Learning, 62(1–2):107–136, feb 2006.
  * Svatoš et al. [2023] Martin Svatoš, Peter Jung, Jan Tóth, Yuyi Wang, and Ondřej Kuželka.  On discovering interesting combinatorial integer sequences.  In Edith Elkind, editor, Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI-23, pages 3338–3346. International Joint Conferences on Artificial Intelligence Organization, 8 2023.  Main Track.
  * Taghipour et al. [2013] Nima Taghipour, Daan Fierens, Jesse Davis, and Hendrik Blockeel.  Lifted variable elimination: Decoupling the operators from the constraint language.  Journal of Artificial Intelligence Research, 47:393–439, 2013.
  * Tóth and Kuželka [2023] Jan Tóth and Ondřej Kuželka.  Lifted inference with linear order axiom.  In Proceedings of the AAAI Conference on Artificial Intelligence, volume 37(10), pages 12295–12304, 2023.
  * van Bremen and Kuželka [2021a] Timothy van Bremen and Ondřej Kuželka.  Faster lifting for two-variable logic using cell graphs.  In Cassio de Campos and Marloes H. Maathuis, editors, Proceedings of the Thirty-Seventh Conference on Uncertainty in Artificial Intelligence, volume 161 of Proceedings of Machine Learning Research, pages 1393–1402. PMLR, 27–30 Jul 2021.
  * van Bremen and Kuželka [2021b] 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.
  * 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 Toby Walsh, editor, Proceedings of the Twenty-Second International Joint Conference on Artificial Intelligence (IJCAI), 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 Proceedings of the Fourteenth International Conference on Principles of Knowledge Representation and Reasoning, KR’14, page 111–120. AAAI Press, 2014.
  * Van den Broeck [2011] Guy Van den Broeck.  On the completeness of first-order knowledge compilation for lifted probabilistic inference.  In Proceedings of the 24th International Conference on Neural Information Processing Systems, NIPS’11, page 1386–1394, Red Hook, NY, USA, 2011. Curran Associates Inc.