{'fraction_non_alphanumeric': 0.051156462585034014, 'fraction_numerical': 0.012585034013605442, 'mean_word_length': 4.024094326725906, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 19, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Weighted Model Counting in the two variable fragment with Cardinality Constraints: A Closed Form Formula

Weighted First-Order Model Counting (WFOMC) computes the weighted sum of the models of a first-order theory on a given finite domain. WFOMC has emerged as a fundamental tool for probabilistic inference. Algorithms for WFOMC that run in polynomial time w.r.t. the domain size are called lifted inference algorithms. Such algorithms have been developed for multiple extensions of FO2(the fragment of first-order logic with two variables) for the special case of symmetric weight functions. We introduce the concept of lifted interpretations as a tool for formulating polynomials for WFOMC. Using lifted interpretations, we reconstruct the closed-form formula for polynomial-time FOMC in the universal fragment of FO2, earlier proposed by Beame et al. We then expand this closed-form to incorporate existential quantifiers and cardinality constraints without losing domain-liftability. Finally, we show that the obtained closed-form motivates a natural definition of a family of weight functions strictly larger than symmetric weight functions.


Introduction
Statistical Relational Learning (SRL) attempts to reason about probabilistic distributions over properties of relational domains [1,2]. Most SRL frameworks use formulas in a logical language to provide a compact representation of the domain structure. Probabilistic knowledge on relational domain can be specified by assigning a weight to every interpretation of the logical language. One of the advantages of this approach is that probabilistic inference can be cast as Weighted Model Counting [3]. First-Order Logic (FOL) allows specifying structural knowledge with formulas that contain individual variables that range over all the individuals of the domain. Probabilistic inference on domains described in FOL requires the grounding (aka instantiation) of all the individual variables with all the occurrences of the domain elements. This grounding leads to an exponential blow up of the complexity of the model description and hence the probabilistic inference.
Lifted inference [4,5] aims at resolving this problem by exploiting symmetries inherent to the FOL structures. In recent years, Weighted First-Order Model Counting has emerged as a useful formulation for probabilistic inference in statistical relational learning frameworks . Formally, WFOMC refers to the task of calculating the weighted sum of the models of a formula Φ over a domain of a finite size wfomc(Φ, w, n) = ω|=Φ w(ω) where n is the cardinality of the domain and w is a weight function that associates a real number to each interpretation ω. FOL theories Φ and weight functions w which admit an algorithm that computes wfomc(Φ, w, n) in a polynomial time w.r.t. n are called domain-liftable [6].
In the past decade, multiple extensions of FO 2 (the fragment of FOL with two variables) have been proven to be domain-liftable [7][8][9][10][11]. These results are formulated over a special class of weight functions known as symmetric weight functions [12] and utilise lifted inference rules which are able to exploit the symmetry of FOL formulas in a rule based manner.
In this paper instead of relying on an algorithmic approach to WFOMC, as in [6], our objective is to find a closed-form for WFOMC in FO 2 that can be easily extended to larger classes of first-order formulas. To this aim we introduce the novel notion of lifted interpretation: a completely first-order concept independent of the domain. Lifted interpretations allows us to reconstruct the closed-form formula for First Order Model Counting (FOMC) in FO 2 proposed in [12] and to extend it to larger classes of FO formulas. We see the following key benefits of the presented formulation: 1. The formula is easily extendeds to FO 2 with cardinality constraints without losing domain-liftability. A cardinality constraint on an interpretation is a constraint on the number of elements for which a certain predicate holds. Earlier approaches to dealing with cardinality constraints involves either using Discrete Fourier Transform [13] over complex numbers or evaluating lagrange interpolation [11]. 2. The formula deals with equality in constant time w.r.t the domain cardinality.
Previous works in WFOMC [12] require additional n+1 calls to the WFOMC oracle, where n is the domain cardinality. 3. The proposed formula solves the model counting problem without introducing (negative) weights. This has the advantage of allowing separate treatment for model counting from weighted model counting. Furthermore, though it has been shown that WFOMC is well defined also with negative weights, the connections between negative weights and probability turns out to be less clean, as it leads to negative and larger than one probability values [14]. 4. The formula computes WFOMC for a class of weight functions strictly larger than symmetric weight functions. This extended class of weight functions allow to model the recently introduced count distributions [15].
Most of the paper focuses on FOMC. We then show how weighted model counting can be obtained by multiplying each term of the resulting formula for FOMC with the corresponding weight. This allows us to separate the treatment of the counting part from the weighting part. The paper is therefore structured as follows: The next section describes the related work in the literature on WFOMC.
We then present our formulation of closed-form formula for FOMC given in [12] for the universally quantified fragment of FO 2 . We then extend this formula to incorporate cardinality constraints. In the successive section, we show how this formula can be used to compute FOMC also in the presence of existential quantifiers. The last part of the paper extends the formula for FOMC to WFOMC for the case of symmetric weight functions and for a larger class of weight functions that allow to model count distributions [15].

Related work
Weighted First Order Model Counting (WFOMC) was initially defined in [6]. The paper provides an algorithm for WFOMC over universally quantified theories based on a knowledge compilation technique, which transforms an FOL theory to a first order deterministic decomposable normal form (FO d-DNNF) 3 . A successive paper [8] has formalized the notion of domain lifted theory i.e. a first order theory for which WFOMC can be computed in polynomial time in the size of the domain. The same paper shows that a theory composed of a set of universally quantified clauses containing at most two variables is domain liftable. This is done by combining knowledge compilation with a technique called domain recursion. In domain recursion, WFOMC of a theory on a domain of n elements is rewritten in terms of WFOMC of the same theory in a domain with n − 1 elements, by partially grounding the theory with a single element of the domain. A successive paper [17] extends this procedure to theories in full FO 2 (i.e, where existential quantification is allowed) by applying skolemization to remove existentially quantified variables. The major drawback of these technique is that it introduces negative weights, and therefore it makes it more complex to use it for probabilistic inference which requires non-negative weights. These results are theoretically analysed in [12], which provides a closed-form formula for WFOMC in FO 2 . [10] extends the domain liftability results to FO 2 with a functionality axiom, and for sentences in uniform one-dimensional fragment U 1 [18]. It also proposes a closed-form formula for WFOMC in FO 2 with functionality constraints. [11] recently proposed a uniform treatment of WFOMC for FO 2 with cardinality constraints and counting quantifiers, proving these theories to be domain-liftable. Finally, [14] re-investigates the problem of skolemization arguing that negative weights can be prohibitive and that the skolemization procedure is computationally expensive. The paper gives examples of theories for which skolemization can be bypassed using domain recursion. With respect to the state of the art approaches to WFOMC, we propose an approach that provides a closed-form for WFOMC with cardinality constraints from which the PTIME complexity is immediately evident. Importantly, this doesn't require the introduction of negative weights. Furthermore, w.r.t. the closed-form proposed in [10] and [12], our proposal for FOMC does not use weights, keeping the counting and the weighting part separate. Finally, [15] introduces Complex Markov Logic Networks, which use complex-valued weights and allow for full expressivity over a class of distributions called count distributions. We show in the last section of the paper that our formalization is complete w.r.t. this class of distributions.

FOMC for Universal Formulas
Let L be a first-order function free language with equality. A pure universal formula in L is a formula of the form where X = {x 1 , . . . , x m } is a set of m distinct variables occurring in Φ(x 1 , . . . , x m ), and Φ(x 1 , . . . , x m ) is a quantifier free formula that does not contain any constant symbol. We use the compact notation Φ(x) for Φ(x 1 , . . . , x m ), where x = (x 1 , . . . , x m ). Notice that we distinguish between the m-tuple of variables x and the set of variables denoted by X. For every σ = (σ 1 , . . . , σ m ), m-tuple of constants or variables, Φ(σ) denotes the result of uniform substitution of x i with σ i in Φ(x). If Σ ⊆ X ∪ C is the set of constants or variables of L and Φ(x) a pure universal formula then Φ(Σ) denotes the formula: Lemma 1. For any arbitrary pure universal formula ∀xΦ(x), the following equivalence holds: Proof. For any x ′ ∈ X m , we have that ∀xΦ(x) → ∀xΦ(x ′ ) is valid. Which implies that ∀xΦ(x) → x ′ ∈X m ∀xΦ(x ′ ) is also valid. Since ∀ and ∧ commute, we have that ∀x.Φ(x) → ∀x.Φ(X). The viceversa is obvious since Φ(x) is one of the conjuncts in Φ(X).
Notice that in Φ(X) we can assume that two distinct variables x and y are grounded to different domain elements. Indeed, the cases in which x and y are grounded to the same domain element is taken into account by the conjunct in which y is replaced by x. See for instance the first and the last conjunct of (4).

Definition 1 (Lifted interpretation).
A lifted interpretation τ of a quantifier free formula Φ(x) is a function that assigns to each atom of Φ(X) either 0 or 1 (0 means false and 1 true) and assigns 1 to Lifted interpretations allow associating truth values to pure universal formulas. The truth value of Φ(x) under the truth assignment τ , denoted by τ (Φ(x)), is obtained by applying the classical propositional logic of the connectives. Notice that τ is not an FOL interpretation as it assigns truth values to atoms that contain free variables, and not to their groundings.
Example 2. Following is the example of a lifted interpretation for the formula (4) of Example 1: We omit the truth assignments of equality atoms, since it is fixed. We have that τ ((4)) = 0.
As highlighted in the previous example, any lifted interpretation τ can be split into a set of partial lifted interpretations τ X ′ , where X ′ ⊆ X is a non-empty subset of variables occurring in Φ. In the example X = {x, y} and τ {x} (simply denoted by τ x ) contains the assignments to the atoms containing only x and we can similarly define τ y . We also have τ {x,y} , written as τ xy , containing the assignments to the atoms that contain both x and y.
Example 3. Consider the assignment of example 2 and the one obtained by the permutation π that exchanges x and y It is easy to see that τ ((4)) = τ π ((4))) = 0. This is not a coincidence, it is actually a property that derives from the shape of Φ(X). This is stated in the following property.
From now on, we concentrate on the special case where X = {x, y} i.e. FO 2 . A closed-form formula for fomc in FO 2 has been proved in [12]. In the following we reconstruct this result using the notion of lifted interpretations. As it will be clearer later, using lifted interpretation allows us to seamlessly extend the closed-form to larger extensions of FO 2 formulas.
For any lifted interpretation τ of Φ(X), let τ x and τ y be the partial lifted interpretation that assign only the atoms containing x and y respectively. Notice that if P (x) is an atom of Φ(X), so is P (y) and vice-versa. This implies that τ x and τ y assign two sets of atoms that are isomorphic under the exchange of x with y. Let u be the number of atoms contained in each of these two sets and let P 0 , . . . , P u−1 be an enumeration of the predicate symbols of these atoms. In other words, we have τ x that assigns truth value to P 0 (x), . . . , P u−1 (x) and τ y that assigns to P 0 (y), . . . , P u−1 (y). 4 This implies that τ x and τ y can be represented by two integers i and j respectively between 0 and 2 u − 1, such that τ x = i if and only if τ x (P k (x)) = bin(i) k , and τ y = j if and only if τ y (P k (y)) = bin(j) k , where bin(i) k refers to the k th number (0 or 1) of the binary encoding of the integer i. For every 0 ≤ i, j ≤ 2 u − 1, we define n ij as the number of lifted interpretations of Φ(X) which are extensions of the partial lifted interpretations τ x = i and τ y = j. Hence, n ij can be written as follows (where we consider variables as constants) where ¬ 0 is the empty string and ¬ 1 is ¬. Notice that Proposition 1 guarantees that n ij = n ji . For any set of constants C and any 2 u -tuple k = (k 0 , . . . , Note there are 3 1,0,2,0 = 3 such partitions, and all the Φ(C k ) for such partitions will have the same model count. These observations have been formalized in lemma 2 Proof. Let C k and C ′ k , be two partitions with the same k. Notice that C ′ k can be obtained by applying some permutation on C from C k . From Proposition 1 we have that Since there are n k partitions of C, of the form C k , then Notice, theorem 1 deals with equality implicitly in the lifted interpretations, which requires constant time w.r.t domain cardinality.
Proof. Notice that fomc(φ(x), n) = mc(Φ(C)) for a set of constants C with |C| = n. Therefore, by Lemma 2, to prove the theorem it is enough to show that for all k, mc(Φ(C k )) = 0≤i≤j≤2 u −1 n k(i,j) ij . By the Lemma 3 we have that mc(Φ(C k )) = c =d n ici d . Then: Example 6 (Example 1 cont'd). Consider a domain of 3 elements (i.e., n=3). Each term of the summation (6) is of the form which is the number of models with k 0 elements for which A(x) and R(x, x) are both false; k 1 elements for which A(x) is false and R(x, x) true, k 2 elements for which A(x) is true and R(x, x) is false and k 3 elements for which A(x) and R(x, x) are both true. For instance 3 2, 0, 0, 1 n 1 00 n 2 03 = 3 2, 0, 0, 1 is the number of models in which 2 elements are such that A(x) and R(x, x) are false and 1 element such that A(x) and R(x, x) are both true.
As a final remark for this section, notice that the computational cost of computing n ij is constant with respect to the domain cardinality. We assume the cost of multiplication to be constant. Hence, the computational complexity of computing (6) depends on the domain only through the multinomial coefficients n k and the multiplications involved in ij n k(i,j) . The computational cost of computing n k is polynomial in n and the total number of n k are n+2 u −1 2 u −1 , which has e·(n+2 u −1) as an upper-bound [19]. Also, the ij n k(i,j) term has O(n 2 ) multiplication operations. Hence, we can conclude that the (6) is computable in polynomial time with respect to the domain cardinality.

FOMC for Cardinality Constraints
Cardinality constraints are arithmetic constraints on the number of true interpretations of a set of predicates in a given FOL formula. In Example 6, we showed how different values of k can represent different unary predicate cardinalities. Let's formalize the correspondence between the multinomial factor n k and the cardinality of the unary predicates of the models that satisfy Φ(C k ) . For every k with k = n and for every unary predicate P j , we define The following lemma states that k(P j ) is the number of c ∈ C such that ω(P j (c)) = 1.

Lemma 4.
For every 2 u -tuple of non-negative integers k with k = n, and every unary predicate P j , and every truth assignment ω, if ω |= Φ(C k ) then c∈C ω(P j (c)) = k(P j ).
Proof. The lemma follows immediately from the definition of Φ(C k ) given in equation (5).
Let ρ({P i }) be any arithmetic constraint on the integer variables representing the cardinality of unary predicates in the n-tuple {P i }. We say that k |= ρ({P i }), if ρ is satisfied when each integer variable, representing cardinality of P i , is substituted for the integer k(P i ) in ρ.

Corollary 1 (of Theorem 1). For every cardinality restriction ρ on unary predicates,
Example 7. To count the models of (4) with the additional constraint that A is balanced i.e., n 2 ≤ |A| ≤ n+1 2 , we have to consider only the terms where k is such n 2 ≤ k(A) ≤ n+1 2 . Equivalently in equation (8) we should consider only the k such that n 2 ≤ k 2 + k 3 ≤ n+1 2 . (Notice that k 2 is the number of elements that satisfy A(x) and ¬R(x, x) and k 3 is the number of elements that satisfy A(x) and R(x, x)).
To count models that satisfy cardinality restriction on binary predicates, we need to extend the result of Theorem 1. Similar to what we have done for unary atoms, let R 0 (x, y), R 1 (x, y), . . . , R b (x, y) be an enumeration of the atoms of Φ(X) that contain both variables x and y. Notice that the order of variables accounts towards different predicates, for instance in Example 1, we have two predicates R 1 (x, y) = R(x, y) and R 2 (x, y) = R(y, x). Every assignment of a lifted interpretation to these predicates can be represented with an integer v, with 0 ≤ v ≤ 2 b − 1, with the usual convention that, if τ xy = v, then τ xy (R k (x, y)) = bin(v) k . Now for every 1 ≤ i ≤ j ≤ 2 u − 1 and every 0 ≤ v ≤ 2 b − 1, n ijv = τ x τ y τ xy (Φ(X)), where τ x = i, τ y = j and τ xy = v. We start by observing that Example 8. For instance n 13 introduced in Example 4 expands to n 130 + n 131 + n 132 + n 133 where n 13v corresponds to the following assignments: Notice that n ijv is either 0 or 1. By replacing n ij in equation (6) with with its expansion (9) we obtain that fomc(Φ(x), n) is equal to where, for every 0 ≤ i ≤ j ≤ 2 u − 1, h ij is a vector of 2 b integers that sum up to k(i, j), and in (10), to simplify the notation, we define the term in the summation corresponding to k, h as Similarly to what we have done for unary predicates, we define h ij (R) for every binary predicate R as follows: (11) where l and r are the indices such that R l corresponds to R(x, y) and R r to R(y, x). For every predicate P we define (k, h)(P ) as k(P ) if P is unary and k(P )+ h(P ) if P is binary. For an n-tuple of predicates {P i }, we use (k, h)({P i }) to denote the n-tuple of non-negative integers {(k, h)(P i )}.

Example 9.
A graphical representation of the pair k, h for the formula (4) is provided in the following picture: This configuration represent the models in which a set C of n constants are partitioned in four sets C 0 , . . . , C 3 , each C i containing k i elements (hence k i = n). Furthermore, for each pair C i and C j the relation j)). For instance if the pair (c, d) ∈ D 12 2 it means that we are considering assignments that satisfy Let ρ({P i }) be any arithmetic constraint on the integer variables representing the cardinality of the set of predicates {P i }. We write (k, h) |= ρ({P i }) to denote that the cardinality constraint ρ((k, h){P i }) is satisfied.

Corollary 2 (of Theorem 1). For every cardinality restriction ρ({P i }), and every pure universal formula
Example 10. Consider formula (4) with the additional conjunct |A| = 2 and |R| = 2. The constraint |A| = 2 implies that we have to consider k such that k 2 + k 3 = 2. |R| = 2 constraint translates to only considering monomials with

FOMC for Existential Quantifiers
Any arbitrary formula in FO 2 can be reduced to an equisatisfiable reduction called Scott's Normal Form(SNF) [20], see equation (18) . [10] prove that SNF also preserves WFOMC of the FO 2 formulas. In this section, we reconstruct the result given in [12] by extending our result for FOMC in universally quantified formulas to the whole FO 2 fragment by providing an FOMC formula for SNF. The main difference w.r.t. [12] is that we explicitly use the inclusion and exclusion principle, instead of introducing negative weights. We first consider the following simpler case: where Φ(x, y) and Ψ(x, y) are formulae without quantifiers. First of all notice that: fomc((12), n) = fomc(∀xy.Φ(x, y), n) (13) − fomc(∀xy.Φ(x, y) ∧ ∃x∀y¬Ψ(x, y), n) The first term of (13) can be computed by Theorem 1; for the second term we need to prove an auxiliary lemma, which uses the following notation: where P is a new unary predicate. In the following lemma we show that e m can be expressed as a function of p i 's.
The equality of (15) and (16) can be obtained by expanding the summation and showing that all the terms of every internal summation cancel but one. We omit this expansion since it is routinary.
Example 11. An expansion of the statement of Lemma 5 with m = 3 and n = 4 is e 2 = 2 2 p 2 − 3 2 p 3 + 4 2 p 4 Since p m is the first order model count of a pure universal formula with cardinality restriction, it can be computed by the formula of Corollary 1. Lemma 5 tells us how to compute also e m starting from the p m 's. Finally notice that, the second term of equation (13) can be computed by summing e m from 1 ≤ m ≤ n. This is possible since the set of models counted in e m are disjoint from the set of models counted in e m ′ , where m = m ′ . This allows us to state the following theorem: ¬Ψ(x, y)) and let n ij be the number of lifted interpretations of Φ ′ (X) which are extensions of the partial lifted interpretation τ x = i and τ y = j, then Proof.
fomc( (12) We generalize the previous result to compute first order model counting for FO 2 formulas in Scott's normal form.

Theorem 3. Consider a formula in Scott's normal form
Where, Φ(x, y) and Ψ i (x, y) are quantifier free formulas. Let Φ ′ (x, y) be the for- where P i 's are fresh unary predicates, let n ij be the number of lifted interpretations of Φ ′ (X) which are extensions of the partial lifted interpretation τ x = i and τ y = j, then Proof (outline). We generalize Lemma 5 as follows: For every m = (m 1 , . . . , m q ) with 0 ≤ m i ≤ n we define The proof of Lemma 5 can be generalized to show that: The proof of (19) can be obtained by replacing the e m with equation (21) and simplifying as in the proof of Theorem 2.
As a final remark, notice that FOMC for FO 2 formulas with cardinality on unary and binary predicate can be computed by first expanding (19) in order to take into account also h, and then restricting to the (k, h) that satisfy ρ. We, therefore, obtain that for an FO 2 formula Φ in Scott Normal Form fomc(Φ∧ρ, n) is equal to

Weighted First Order Model Counting
In FOMC every model of a formula contributes with one unit to the final result. Instead in WFOMC, models can be associated with different contributions, also called weights. The weight of an interpretation ω is provided by a weight function w that associates a real number to it. More formally: given a first order language L and an interpretation domain C a weight function w is a function w : ω → w(ω) ∈ R. WFOMC has been extensively studied for finite domains, and for weight functions that are independent of individual domain elements. In this case the definition of weighted model counting reduces to wfomc(Φ, w, n) = ω|=Φ w(ω) where n is the cardinality of the domain. We propose a new family of such weight functions on (k, h) vectors. A weight function w(k, h) associates a real number to each (k, h). Hence, we define WFOMC as follows : Definition 2. For all Φ in FO 2 and for arbitrary cardinality constraint ρ.
where w(k, h) is an arbitrary positive real valued function.

Symmetric Weight Functions
Symmetric weight function [12] is a family of weight functions that can be specified by a function w : P × {0, 1} → R, where P is the set of predicate symbols of L. The weight of an assignment ω is then defined as follows: The following theorem shows how symmetric weight functions can be expressed by w(k, h).
Theorem 4. For all Φ in FO 2 and for arbitrary cardinality constraint ρ, symmetric-WFOMC can be obtained from FOMC by defining the following weight function: where (k, h)(¬P ) = n − k(P ) if P is unary and n 2 − (k, h)(P ) if P is binary.
Proof. The proof is a consequence of the observation that F (k, h, {n ijv }) is the number of models of Φ that contains k(P ) elements that satisfies P , if P is unary, and (k, h)(P ) pairs of elements that satisfy P , if P is binary.

Expressing Count Distributions
Symmetric weight functions cannot express many interesting distributions. For instance, consider a set of domain elements C = {c 1 , . . . , c n } which have an attribute A. To impose a fairness constraint on A, one would like to have higher weights for interpretations ω in which the number instances of A being true and false are balanced, e.g., it is proportional to (|A ω | − |¬A ω |) 2 . A class of weight functions that allow modelling these type of situations have been introduced in [15]. These weight functions have been introduced to express count distributions, which are defined in the following definition.
Definition 3 (Count distribution [15]). Let Φ = {α i , w i } m i=1 be a Markov Logic Network defining a distribution over a set of possible worlds (we call them assignments) Ω. The count distribution of Φ is the distribution over mdimensional vectors of non-negative integers n given by where N (Φ, ω) = (n 1 , . . . , n m ), and n i is the number of grounding of α i that are true in ω. [15] shows that count distributions can be modelled by MLN's with complex weights. In the following, we show that if α i and Φ are in FO 2 , then we can express count distributions with positive real valued weights on (k, h).
Theorem 5. Every count distribution over a set of possible worlds Ω definable in FO 2 can be modelled with a weight function on (k, h), by introducing m new predicates P i and adding the axioms P i (x) ↔ α i (x) and P j (x, y) ↔ α j (x, y), if α i and α j has one and two free variables respectively, and by defining: where Z = wfomc(Ω, w, n) also known as the partition function.
Proof. The proof is a simple consequence of the fact that all the models agreeing with a count statistic N (Φ, ω) can be counted using cardinality constraints which agree with N (Φ, ω). Any such cardinality constraint correspond to a specific set of (k, h) vectors. Hence, we can express arbitrary probability distributions over count statistics by picking real valued weights for (k, h) vector. In the following we prove this statement formally: Since Ω is a FO 2 formula, then we can compute FOMC as follows: Let us define w(k, h) for each k, h as follows: Where p Φ,Ω (ω) is the probability of world ω, under count distribution q Φ (Ω, n). Our goal is to show that this weight function suffices to express count distributions. This definition implies that the partition function Z is equal to 1. Indeed: Which is exactly the probability of the worlds agreeing with the count statistic N (Φ, ω).
In [15], authors propose an example for which the probability cannot be expressed using Symmetric-WFOMC and obligates the use of complex valued weights. In the following, we present the same example and are able to express it's distribution with real valued weights on the (k, h) vector.
Example 12. In this example we wish to model a sequence of 4 coins being tossed such that the probability of getting odd number of heads is zero, and the probability of getting even number of heads is uniformly distributed. We introduce a predicate H(x) over a domain of 4 elements. Notice that such a distribution cannot be expressed using symmetric weights, as symmetric weights can only express binomial distribution for this language. But we can define weight function on (k, h) vector. In this case k = (k 0 , k 1 ) such that k 0 + k 1 = 4. Since there are no binary predicates we can ignore h. Intuitively, k 0 is the number of elements not in H and k 1 is the number of elements in H. If we define the weight function as w(k 0 , k 1 ) = 1 + (−1) k1 by applying (24) we obtain the following probabilities: q(Ω, (4, 0)) = We are able to capture count distributions without loosing domain liftability or introducing complex or even negative weights, making the relation between weight functions and probability rather intuitive.

Conclusion
In this paper we have presented a closed-form formula for FOMC of universally quantified formulas in FO 2 that can be computed in polynomial time w.r.t. the size of the domain. From this, we are able to derive closed-form expression for FOMC in FO 2 formulas in Scott's Normal Form, extended with cardinality constraints. All the formulas are extended to cope with weighted model counting in a simple way, admitting larger class of weight functions than symmetric weight functions. All the results have been obtained without introducing negative or imaginary weights, which makes the relation between weight functions and probability rather intuitive.