Lifted Probabilistic Inference by First-Order Knowledge Compilation

1 Introduction

Probabilistic logical languages, which combine the advantages of graphical models with those of first-order logic [Getoor and Taskar, 2007; De Raedt et al., 2008], have received much attention in recent years. Since these languages offer more expressivity than their logical and probabilistic counterparts, performing efficient inference is challenging. In order to reduce the cost of inference in these languages, Poole [2003] proposed performing lifted inference, which avoids repeated computation by treating indistinguishable groups of objects as one.

Various solutions have been proposed (e.g., [de Salvo Braz et al., 2005; Milch et al., 2008; Jha et al., 2010]). While significant progress has been made, we lack a complete understanding of how to perform lifted inference, that is, how to unify the principles of inference in first-order logic with those of inference in graphical models. The goal of lifted inference is analogous to that of the resolution principle in first-order logic as both try to perform inference at the first-order level and to ground out only when necessary.

In the literature on inference in graphical models, one can distinguish two types of approaches: probabilistic inference methods such as variable elimination and belief propagation and logical inference methods based on weighted model counting [Chavira and Darwiche, 2008]. Most existing lifted inference techniques have lifted probabilistic inference methods toward the use of first-order logic. What has been largely unexplored is applying techniques from inference in firstorder logic to lifted probabilistic inference.

The key contribution of this paper is that we introduce a first-order knowledge compilation approach to lifted probabilistic inference. We do so by upgrading propositional dDNNF (deterministic decomposable negation normal form) circuits to the first-order setting. Given a weighted clausal theory (i.e., weights are assigned to predicates), our approach compiles it into a first-order d-DNNF, which can perform weighted model counting in time polynomial in the size of the first-order d-DNNF. It is easy to show that several existing probabilistic logic representations such as parfactors [Poole, 2003] and Markov Logic [Singla and Domingos, 2008] can be transformed into an equivalent weighted first-order theory.

In this paper we present a model theoretic approach to lifted inference that builds on well known concepts from logical inference, such as model counting, unit propagation, and Shannon decomposition. We show essentially that existing concepts from lifted probabilistic inference have their model-theoretic counterpart. Furthermore, our WFOMC (weighted first-order model counting) approach exploits context-specific independencies [Boutilier et al., 1996], which arise when the probabilistic dependencies have an internal logical structure. We also show that WFOMC can lift more inference problems than alternative approaches.

2 Background and Notation

We first introduce standard notions of (function free) firstorder logic. An atom p(t1, . . . , tn) consists of a predicate p/n of arity n followed by n terms ti. Terms are either constants or variables. A literal l is an atom a or its negation ¬a. A clause is a disjunction l1 ∨ ... ∨ lk of literals. If k = 1, we have a unit clause. We often write clauses as their set of literals. Clauses are assumed to be universally quantified. A substitution θ = {v1 = t1, ..., vl = tl} is an assignment of terms ti to variables vi. A theory is a finite set of clauses denoting the conjunction of its clauses. An expression is an atom, literal, clause or theory. The set of all logical variables appearing in an expression e is denoted by Vars(e). The functions atom(e) and lit(e) map an expression to the atoms and literals it contains. An expression is ground if it does not contain any variables. A Herbrand interpretation is a set of ground atoms. All atoms in the interpretation are assumed to be true, while all other atoms belonging to the Herbrand base (the set of all possible ground atoms) are assumed to be false. An interpretation I satisfies a theory T , written as I |= T , if it satisfies all the clauses c ∈ T. An interpretation that satisfies the theory is a model for the theory and we denote the set of models of a theory T byM(T) = {I | I |= T}.

We now extend these notions by adding to each expression e a constraint set (CS) which is a set of constraints defined on Vars(e). The CS essentially represents a constraint satisfaction problem and denotes a conjunction of constraints of the form: 1) v ∈ D, where D is the domain of the variable v and v ∈ Vars(e); 2) vi ̸= vj with vi, vj ∈ Vars(e); 3) or, v ̸= k, with v ∈ Vars(e) and k a constant. Negations of these constraints are also allowed. A substitution θ = {v1 = t1, . . . , vl = tl} is a solution to a CS cs if and only if all constraints in csθ are ground and satisfied. When a solution to a CS exists, we say the CS is satisfiable. The set of assignments to variable v for which the CS is satisfiable is denoted by Sol(cs, v).

Expressions e together with their associated constraint set cs are called c-expressions and are written as (e, cs). Thus, we can talk about c-literals, c-clauses and c-theories. The functions atomc(e), litc(e) and cs(e) map an expression to its c-atoms, c-literals and CS. In the remainder of the paper we work with c-expressions and often drop the c for ease of exposition. Furthermore, constraints can be simplified or reduced using standard constraint solving techniques and we implicitly allow that. Space restrictions do not allow for a more detailed analysis. One particular type of reduction is to apply equalities of the form v = t, i.e., a c-expression (e, {cs, v = t}) is reduced to (e{v = t}, cs{v = t}). A substitution θ = {v1 = t1, . . . , vl = tl} can be regarded as a conjunction of equality constraints, e.g., v1 = t1 ∧ . . . ∧ vl = tl. Therefore, applying a substitution θ to a c-expression (e, cs) yields the c-expression (e, cs ∧ θ) which is equivalent to (eθ, csθ).

Two c-literals L1 = (l1, cs1) and L2 = (l2, cs2) cunify with substitution θ if and only if l1θ = l2θ and the CS (cs1 ∧ cs2)θ is satisfiable. The result is denoted as (l1θ, (cs1 ∧ cs2)θ), or θ = (l2θ, (cs1 ∧ cs2)θ). We write that L1θ ≃ L2θ. The most general unifier is denoted by θ = mgu(L1, L2). Two c-expressions e1 and e2 are independent, written as e1 ⊥⊥ e2, if no c-atom a1 ∈ atomc(e1) cunifies with a c-atom a2 ∈ atomc(e2). The set of groundings gr(e) of a c-expression e is the set of ground c-expressions eg s.t. ∃θ for which eg = eθ and cs(e)θ is satisfied. Intuitively, a clause c represents all its ground instances cθ, whereas a constrained clause (c, cs) represents all ground instances cθ such that csθ is true according to the constraint theory.

Example 1. Take the constrained literal

The mgu of l and flies(pigeon) is θ = {X = pigeon}, because it is the most general unifier of the unconstrained literals and csp(l)θ = (pigeon ̸= kiwi ∧ pigeon ∈ Bird) is satisfied. Constrained literal l is independent fromflies(kiwi) because the mgu of the unconstrained literals gives rise to the unsatisfied constraint kiwi ̸= kiwi .

3 Algorithm

Our approach to lifted inference converts the first-order probabilistic inference task to a weighted first-order model counting problem. We do so by compiling a clausal theory to a firstorder d-DNNF circuit, thereby lifting the knowledge compilation approach. In the next subsections we discuss the key elements of our approach: (i) how to cast probabilistic inference into a weighted model counting problem, (ii) which formula does a circuit represent, (iii) how to compile the theory to an equivalent circuit, and (iv) how to compute the weighted model count using the circuit.

3.1 Weighted First-Order Model Counting

Weighted First-Order Model Counting (WFOMC) augments a theory in first-order logic with a positive weight function w and a negative weight function w, which assign a weight to each predicate. The WFOMC problem for a theory T of c-clauses consists of computing

where HB(T) is the Herbrand base and Pred maps atoms to their predicate.

Representing existing probabilistic logical models such as Markov logic networks (MLN) or parfactors as WFOMC problems requires transforming them into a set of c-clauses.

Example 2. An MLN is a set of pairs (Fi, ri) where Fi is a formula in first-order logic and ri a real-valued number. Since WFOMC works on literals and not clauses, we reify each formula Fi in the MLN, creating a new atom f i(Vars(Fi)) ≡ Fi. The weight functions of the reified atom are w(fi) = eri and w(f i) = 1.

Take the MLN formula with weight 2:

We introduce a new predicate f that represents the truth value of this formula and which is assigned w(f) = e2 and w(f) = 1. The friends and smokes predicates are assigned w(.) = w(.) = 1. In the logical theory we put

The WFOMC of this theory is equal to the partition function of the MLN. Parfactors can be transformed into a set of c-clauses in a similar way.

3.2 First-Order d-DNNFs

Deterministic decomposable negation normal form (dDNNF) circuits [Darwiche and Marquis, 2002] are directed acyclic graphs whose leaves represent literals and whose inner nodes represent formulae in propositional logic. The inner node operators in propositional d-DNNFs are:

• Decomposable conjunction l ∧©r, representing the formula l ∧ r with the constraint that the operand formulas l and r are independent (l ⊥⊥ r).
• Deterministic disjunction l ∨©r, representing the formula l ∨ r with the constraint that the operands cannot be true at the same time (l ∧ r is unsatisfiable).

We generalize propositional d-DNNFs to first-order dDNNF (FO d-DNNF) circuits, where leaves represent firstorder literals and inner nodes represent first-order formulae. FO d-DNNFs are more compact than their propositional counterparts. In addition to the propositional operators in inner nodes, we define the following novel operators:

• Inclusion-exclusion IE(x, y, z), representing the formula x ∨ y with the extra operand z ≡ x ∧ y, which is required to perform (weighted) model counting in the circuit.
• Decomposable set-conjunction ∧©c over isomorphic operands, represented by a single child circuit c.
• Deterministic set-disjunction ∨©c over isomorphic operands, represented by a single child circuit c.

These last two operators differ from their propositional counterparts in that they have only one child node c, which represents a potentially large set of isomorphic operands.

Example 3. Figure 1 shows the FO d-DNNF circuit for the CNF of Example 2. Variables are in the domain People.

Example 4. Figure 2b represents a set-conjunction of |People| operands. Since all operands are isomorphic (identical up to the value of Skolem constant x), they are represented by a single child, parametrized in x. We will later see that these operands have identical weighted model counts.

Similarly, Figure 2c shows a set-disjunction of theories that are identical up to the value of FunPeople. Again, the circuit only contains a single child of the set-disjunction, which is parametrized in FunPeople.

3.3 Auxiliary Operations

Next, we introduce the auxiliary operations for splitting and shattering, which are needed in the compilation process. Whenever the pre-condition holds before applying the operation, the post-condition holds after applying it.

Splitting

Some compilation rules require that all c-clauses c in the theory be split w.r.t. a certain c-atom a.

Operator SPLIT(c, a) =

if ∀ ac ∈ atomc(c) : ac ⊥⊥ a∨gr(ac)\gr(a) = ∅ then {c}

else {SPLIT(cmgu, a)} ∪ ⋃cr∈Cr SPLIT(cr, a)

for some ac ∈ atomc(c) such that gr(ac) \ gr(a) ̸= ∅,

θ = mgu(a, ac),

cmgu = (lit(c), cs(c) ∧ θ ∧ cs(a)),

and Cr = {(lit(c), cs(c) ∧ ¬e)|e ∈ (θ ∧ cs(a))} \ {c}

Postconditions

The purpose of splitting is to divide a clause into an equivalent set of clauses (Postcondition 2) such that for each atom as in each clause, either as is independent from a or is subsumed by it, because it covers a subset of the ground atoms of a (Postcondition 1).

Example 5. Splitting

c = (flies(X) ∨ ¬ haswings(X), X ̸= kiwi ∧ X ∈ Animal ) a = (flies(X), X ̸= penguin ∧ X ∈ Bird ),

where domain Bird ⊂ Animal , results in cmgu = (flies(X) ∨ ¬haswings(X),X ̸= kiwi ∧ X ̸= penguin ∧ X ∈ Bird), c1r = (flies(penguin) ∨ ¬haswings(penguin)) and c2r = (flies(X) ∨ ¬haswings(X),X ̸= kiwi ∧ X ∈ Animal \ Bird).

After splitting, clauses c1r and c2r are independent from a, while the c-atom (flies(X), X ̸= kiwi ∧X ̸= penguin ∧X ∈ Bird) in cmgu is implied by a.

Finally, splitting an entire theory C with respect to c-atom ac is defined as SPLIT(C, ac) = ⋃c∈C SPLIT(c, ac). Splitting was introduced by Poole [2003] for parfactors. We apply it to clauses and extend it with set membership constraints.

Shattering

Some compilation rules require the theory C to be shattered.

Operator SHATTER(C) =

if ∃ a ∈ atomc(C) such that SPLIT(C, a) ̸= C then SHATTER(SPLIT(C, a)) else C Postcondition ∀a1, a2 ∈ atomc(SHATTER(C)) : a1 ⊥⊥ a2 ∨ gr(a1) = gr(a2)

Shattering performs splitting until convergence. The postcondition states that after shattering, all c-atom groundings are either disjoint or identical. The specific assignments to the logical variables cannot be distinguished any further. A variant of shattering on parfactors was proposed for FOVE [de Salvo Braz et al., 2005].

3.4 Compilation Rules

The purpose of the compilation rules is to transform a CNF into a set of simplified CNFs that are combined using a FO d-DNNF operator from Section 3.2. This requires that (1) the compiled circuit is equivalent to the original theory and (2) the (decomposable, deterministic) properties of the FO dDNNF operators hold. We continue compiling the simplified CNFs until they become unit clauses, the leafs of the FO dDNNF circuit.

Compiling a set of c-clauses C to FO d-DNNF is performed by the COMPILE(C) function, which tries to recursively apply the compilation rules in the order we present them here. A compilation rule applies when its preconditions are met.

Caching

Before compiling a theory, we attempt to retrieve its circuit from a cache of previously compiled theories. Reusing previously computed FO d-DNNFs turns the circuit from a tree into a DAG. Caching is an essential feature of propositional knowledge compilation algorithms. Currently, we employ a naive caching scheme that only recognizes the reuse of ground theories.

Unit Propagation

We now consider the case where the CNF contains unit clauses. First, we describe an auxiliary operation to perform unit propagation of a c-literal l on a single c-clause c, where a is the atom of l.

Precondition {c} = SPLIT(c, a) (c has been split w.r.t. a) Operator UPCLAUSE(c, l) =

Unit propagation distinguishes between two cases: if the clause contains a literal that unifies with the propagating literal l, the clause is removed. Otherwise, the clause atoms that unify with the propagating atom are removed from the clause.

This generalizes to a compilation rule on a set of clauses C containing a unit clause cu.

Postcondition Cup ⊥⊥ cu and C ≡ Cup ∧ cu

The Postcondition states that the returned conjunction is decomposable and equivalent to the original theory.

Example 6. Figure 2a shows unit propagation of the unit clause friends(X,X). The first two clauses require splitting w.r.t. the unit clause atom, which creates two copies of each clause: one where X = Y and one where X ̸= Y . Next, the first copy of the first clause is removed, because it is subsumed by the unit clause. In the first copy of the second clause, the atom that unifies with the unit clause atom is removed, because it must be false in any model. This yields the clause likes(X,X).

Finally, the unit clause becomes independent of the other clauses, and can be split off in a decomposable conjunction.

The unit clause is a leaf of the circuit, while the remainder of the theory requires further compilation.

Independence

When the theory contains two sets of independent clauses, we can split them using a decomposable conjunction.

Inclusion-Exclusion

Intuitively, when the theory contains a clause whose literals can be divided into two sets that do not share any logical variables or constraints, inclusion-exclusion is possible. The children of an inclusion-exclusion node are simpler than their parent, because they have shorter clauses.

Preconditions C is a set of c-clauses such that

1. C = {(L1 ∪L2, csL)} ∪CR
2. Vars(L1) ∩Vars(L2) = ∅
3. ¬∃v1 ∈ Vars(L1), v2 ∈ Vars(L2) : (v1 ̸= v2) ∈ csL

Operator INCEXC(C) =

IE(COMPILE(C1), COMPILE(C2), COMPILE(C3))

with C1 = {(L1, csL)} ∪ CR

C3 = {(L1, csL), (L2, csL)} ∪ CR.

Postconditions

Example 7. C-clause (helps(X) ∨ ¬succeeds(Y ),X ∈ People, Y ∈ Task) has two subclauses: c1 = (helps(X),X ∈ People) and c2 = (¬succeeds(X),X ∈ Task) which are not linked by a logical variable. The INCEXC operator results in an inclusion-exclusion node with child circuits for c1, c2 and c1 ∧ c2.

A special case of inclusion-exclusion, Shannon decomposition, occurs when L1 = {a} and L2 = {¬a} and a is a ground atom. Then C3 becomes a contradiction and C1 ∨C2 is a deterministic disjunction. This decomposition is always performed when the theory contains a ground atom, because adding the clause a ∨ ¬a to a theory containing a does not change the set of models. Shannon decomposition is a common operation in logical inference. We generalize it to inclusion-exclusion.

Example 8. Having a c-clause c = (fun(bob) ∨ ¬friends(bob,X),X ∈ People), applying Shannon decomposition results in a decomposable disjunction of the circuits for {{fun(bob)}, c} and {{¬fun(bob)}, c}, which after an application of UNITPROP results in fun(bob) ∨© (¬ fun(bob) ∧©¬ friends(bob, X), X ∈ People).

Shattered Compilation

For the next two operations, the theory needs to be shattered. Furthermore, shattering might introduce new opportunities for the independence, inclusion-exclusion or Shannon decomposition rules. Because we only shatter in this stage of the compilation process, the previous operators use what is called splitting as needed [Kisy´nski and Poole, 2009].

Preconditions C is a set of clauses

1. ∃a ∈ atomc(C) : SPLIT(C, a) ̸= C

Operator SHATTERCOMP(C) = COMPILE(SHATTER(C))

Independent Partial Groundings

Preconditions C is a set of c-clauses such that

1. ¬∃CI ⊂ C : CI ⊥⊥ C \ CI
2. A function root such that ∀ c ∈ C : root(c) ∈ Vars(c)
3. ∀ l1, l2 ∈ litc(C) : l1θk1 ⊥⊥ l2θk2 where θki = {(root(c) = ki)|c ∈ C} and k1, k2 arbitrary unique constants

Operator IPG(C) = ∧©k∈K COMPILE(Cθk)

with k a parameter for a constant,

and K such that ∀ c ∈ C : K = Sol(root(c), cs(c))

Postconditions

1. Cθk1 ⊥⊥ Cθk2 with k1, k2 arbitrary unique constants
2. C ≡ ∧k∈K Cθk
3. ∀k1, k2 ∈ K : COMPILE(Cθk1 ) ∼= COMPILE(Cθk2 ), meaning that all operand circuits are isomorphic.

Precondition 3 guarantees that every literal in the theory contains a variable in {root(c)|c ∈ C} and that the variable appears in the same positions of the argument lists of two unifying atoms. Consequently, any pair of atoms that previously unified, becomes independent after partially grounding to a different constant. Postcondition 2 states that the setconjunction of all operands is equivalent to the original theory. Postcondition 1 makes the set-conjunction decomposable and follows straightforwardly from Precondition 3.

The operands of a decomposable set-conjunction were defined to be isomorphic. If after shattering the theory contains no independent sets of clauses (Precondition 1), the constraints and domains of each root(c) are identical and each clause is grounded w.r.t. the same set of constants K. Applying independent partial grounding in a naive way would create |K| subcircuits - a potentially very large number. However, because the subcircuits are isomorphic (identical up to renaming of the grounding constant, Postcondition 3), the dDNNF for C is more succinctly represented by compiling only one child theory Cθk, where k is a parameter representing the grounding constant. This makes both the compilation complexity and FO d-DNNF size independent from |K|. Independent partial grounding is based on the same underlying ideas as partial inversion in FOVE and the power rule in CPs [Jha et al., 2010].

Example 9. Figure 2b shows a theory T where independent partial grounding can be applied by choosing the root function that maps each clause to its X variable. When these variables are grounded to different constants (Tθalice and Tθbob), the different groundings are independent, which means they form a decomposable conjunction. This naive approach would generate |People| subcircuits. We can do better by observing that the partially grounded theories are identical up to renaming of the constants, and so are the circuits. Therefore, it suffices to compile a single theory Tθx where x represents some constant in the domain People.

Independent partial grounding does not simplify the theory. By grounding logical variables, however, it creates new opportunities for other rules. For example, the bottom theory of Figure 2b contains a ground atom fun(x), which allows for Shannon decomposition. This is shown in Figure 3. In the branch where fun(x) is false (labeled with (2) in Figure 3), subsequent steps of unit propagation simplify the theory in a decomposable conjunction of unit clause leafs. The other branch (1) requires one more step of independent partial grounding and Shannon decomposition.

Atom Counting

Preconditions C is a set of c-clauses such that

1. ∃a ∈ atomc(C) : Vars(a) = {v}

Operator ATOMCOUNTING(C) =

∨©D⊆S COMPILE(C ∪ {cD, ¯ cD})

with S = Sol(v, cs(a)), D the domain parameter,

cD = ({a}, cs(a) ∧ (v ∈ D)),

and ¯

cD = ({¬a}, cs(a) ∧ (v /∈ D)).

Postconditions For F,G ⊆ S :

1. M(C ∪ {cF , ¯ cF }) ∩ M(C ∪ {cG , ¯ cG}) = ∅ ∨ F = G
2. COMPILE(C ∪ {cF , ¯ cF }) ∼= COMPILE(C ∪ {cG, ¯ cG}), meaning that all operand circuits are isomorphic.

When the theory contains an atom with a single logical variable v, we can partition the set of models depending on the values for v for which the atom is true. The disjunctions between these partitions are deterministic (Postcondition 1), because their models disagree in at least one atom.

Because the theory has been shattered, the individuals k ∈ D are indistinguishable. As a result, the operands of the deterministic disjunction are isomorphic (Postcondition 2) and their circuits only differ in the domain D. Again, we only compile a FO d-DNNF that is parametrized in D but whose size is independent of |D| and |S|. Atom counting by itself does not simplify the theory, but by introducing two new unit clauses, unit propagation will be able to eliminate a from the theory entirely in subsequent compilation steps. Atom counting is inspired by counting elimination in FOVE and the generalized binomial rule in CPs.

Example 10. Figure 2c shows a theory T that only allows for atom counting. All logical variables are implicitly elements of domain People. The fun(X) atom has 2|People| partial interpretations (e.g., {fun(1), fun(2)}, {fun(1), ¬ fun(2)}, . . . , {¬fun(1), ¬fun(2)} when the number of people is 2). We can create a theory equivalent to T by conjoining each partial interpretation with T , and taking the disjunction over all partial interpretations. Because each partial interpretation differs in at least one truth assignment, this disjunction is deterministic.

Compiling the theory as such defies the point of lifted inference, because it creates 2|People| subcircuits. However, we can observe that all subcircuits are isomorphic. They are identical up to the set of constants c for which fun(c) is true. We only need to compile one single subcircuit, parametrized in the subset FunPeople of People. We will later see that evaluating the weighted model count using this circuit is only linear in |People|, which makes this operator lifted.

Atom counting only adds unit clauses to the theory. Figure 4 shows how three subsequent steps of unit propagation split off a unit clause leaf until the remaining theory becomes a unit clause leaf of the circuit itself.

Grounding

If no other compilation rule applies, we ground out a logical variable in the theory, after which compilation is retried. A good heuristic is to select the variable with the smallest number of solutions | Sol(v, cs(v))|.

3.5 First-Order Smoothing

Compilation steps such as unit propagation or inclusionexclusion may remove literals from branches of the d-DNNF. The groundings of these literals may go unaccounted for when doing model counting in the d-DNNF. This problem is solved by smoothing the circuit [Darwiche and Marquis, 2002], which we lift to the first-order level as well.

Smoothing first propagates a set of c-atoms upwards in the circuit, representing the groundings that are accounted for in the circuit. Binary conjunctions, disjunctions and inclusionexclusion nodes propagate the union of these sets. In setconjunctions with a parametrized constant kr, special care is taken to generalize the counted atoms of the child to the full set of operands by applying the inverse substitution θ-1 kr , which replaces the placeholder constant kr by the variables to which the root function maps. Similarly, for set-disjunctions parametrized in domain D, the set of counted atoms of the representative child is generalized to the full set of operands by removing the domain constraints v ∈ D and v /∈ D from the atoms.

Second, smoothing adds nodes to the circuit where operands of (set-)∨© or IE count different sets of atoms. When an atom a with constraints csa is missing from node n, the node is replaced by COMPILE({a, ¬a}, csa) ∧©n

Example 11. The circuit in Figure 3 is not smooth. The bottom disjunction's operands cover a different set of atoms. The right branch covers only friends(x, y) while the left branch covers friends(x, y) and dislikes(x, y). In this case, first-order smoothing is identical to propositional smoothing. It substitutes the right branch by a decomposable conjunction of the right branch and the circuit dislikes(x, y) ∨©¬ dislikes(x, y).

Example 12. The circuit in Figure 4 is not smooth. The theory in the root node (Figure 2c) covers atoms fun(X) and friends(X, Y ). The circuit below the root node covers fun(X) entirely, but is not accounting for the atoms friends(X, Y ),X ∈ FunPeople, Y ∈ FunPeople. Firstorder smoothing compensates for this by inserting a decomposable conjunction below the set-disjunction. The operands of the new conjunction are (1) the original child of the set-disjunction and (2) the compiled circuit for the theory friends(X, Y ) ∨ ¬friends(X, Y ),X ∈ FunPeople, Y ∈ FunPeople. As a result, all ground atoms of the original theory are being counted.

3.6 Propagating theWeightedModel Count

As for propositional d-DNNFs, smooth FO d-DNNFs permit weighted model counting in time polynomial in the size of the circuit, by interpreting the d-DNNF as an arithmetic circuit. In a leaf with c-atom a of predicate p:

As in propositional knowledge compilation and from Postconditions 1 and 2 of INCEXC:

For a set-conjunction coming from independent partial grounding, the operands are not only isomorphic, but they have the same WFOMCs, due to shattering. Its weighted model count is wmc(∧©k∈Kchildk) = wmc(childk)|K| , which can be computed in time independent of |K|.

Set-disjunction due to atom counting is more complicated. We know that the operands have d-DNNF circuits isomorphic to childD, but they have different weighted model counts. Iterating over all D ⊆ S would be intractable and defeats the purpose of lifted inference. However, with Dn = {D|D ⊆ S, |D| = n}, we observe that ∀D1,D2 ∈ Dn : wmc(childD1 ) = wmc(childD2 ). We can group together subsets of S of equal size, because they have identical WFOMCs. Furthermore, because set-disjunction is deterministic and |Dn| = (|S| n ), we find

While model counting for all other node types is independent of the domain sizes, model counting for set-disjunction is linear in |S|.

4 Empirical Evaluation

In this section, we evaluate our approach on common benchmarks in the lifted inference literature including competing workshops and workshop attributes [Milch et al., 2008], friends and smokers [Singla and Domingos, 2008], sick and death [de Salvo Braz et al., 2005] as well as a novel example. We compare the performance of WFOMC with counting first-order variable elimination (C-FOVE) [Milch et al., 2008]

and propositional variable elimination (VE). WFOMC is implemented in Scala 1 and we used the publicly available Java implementation of C-FOVE. 2

Figure 5 contains representive results on three different tasks. It plots how inference time varies with the domain size on each task. It includes two results for WFMOC, one which only measures circuit evaluation time and another that includes both compilation and evaluation time. Compilation is only needed once per theory and can be amortized across all domain sizes. For C-FOVE and ground VE, the plot shows inference time as these methods have no compilation phase.

For both the competing workshops and friends and smokers tasks, ground VE quickly runs out of memory and achieves worse performance than the lifted methods. When considering only inference time, WFOMC is the same or faster than C-FOVE. When considering both compilation and inference time, WFOMC is faster for larger domain sizes, but C-FOVE is slightly faster for small domain sizes.

We extended the friends and smokers example with an extra formula: friends(X, Y ) ∧ drinker(X) ⇒ drinker(Y ). WFOMC can lift this theory whereas C-FOVE cannot lift it. We omit the curve for C-FOVE because the implementation fails. 3 Ground VE quickly runs out of memory.

Lifted inference provides a significant advantage compared to ground inference. WFOMC can identify and lift more structures than C-FOVE making it more efficient in these cases. In cases where the operators in C-FOVE are sufficient to fully lift the theory, WFOMC's inference is faster, but has a small overhead associated with the compilation step. It is important to note that knowledge compilation only needs to be performed once per theory, that is, it is independent of the domain size (for a fixed evidence set).

5 RelatedWork

WFOMC builds upon the technique of probabilistic inference through knowledge compilation [Darwiche and Marquis, 2002]. To date, these approaches have only explored compiling propositional d-DNNF circuits [Chavira et al., 2006]. In contrast, we define first-order d-DNNF circuits and present an algorithm for compiling them.

Existing approaches to lifted inference have primarily focused on standard probabilistic inference algorithms such as variable elimination (e.g., [Poole, 2003; de Salvo Braz et al., 2005; Milch et al., 2008]) and belief propagation (e.g., [Singla and Domingos, 2008]). WFOMC differs from these types of methods in two significant ways. First, we take a model theoretic approach to inference. Second, our algorithm exploits local structure (e.g., context specific independence) within the the model. Considering local structure can substantially improve the efficiency of inference, and this type of structure is common in probabilistic logical models.

The approaches of Jha et al. [2010] and Gogate and Domingos [2010] are more similar in spirit to our approach. Jha et al. also approach the problem from the perspective of logical inference and identify a limited class of models where tractable lifted inference is possible. For example, their approach excludes models that contain a clause where the same predicate appears more than once. Furthermore, it only works if the inference can be done fully on the lifted level. Gogate and Domingos [2010] propose a lifted version of AND/OR search. The d-DNNF structure is closely related to AND/OR structures. However, as noted by Dechter and Mateescu [2007], d-DNNF's are theoretically more expressive. Gogate and Domingos' approach differs in that they approach the problem from a different angle and use weighted CNF clauses instead of weighted model counting. Furthermore, they do not support caching and have no operator equivalent to the inclusion-exclusion operator.

1 http://dtai.cs.kuleuven.be/wfomc/

2 http://people.csail.mit.edu/milch/blog/

3 In theory, C-FOVE should be able to solve this theory by grounding it and performing VE.

6 Conclusions

We proposed the first model theoretic approach to lifted probabilistic inference. We introduced first-order d-DNNF circuits and presented an algorithm to compile a first-order probabilistic theory into one of these circuits. Our algorithm exploits well known concepts from logical inference including model counting, unit propagation, and Shannon decomposition. Furthermore, we drew connections between our model theoretic inference rules and those proposed for probabilistic inference, bringing us closer to understanding the connection between lifted inference in first-order logic and graphical models.

Acknowledgements The authors would like to thank Maurice Bruynooghe for valuable feedback. Guy Van den Broeck is supported by the Research Foundation-Flanders (FWOVlaanderen). This research is supported by GOA/08/008 'Probabilistic Logic Learning'.