Communications of the ACM

sufficient since each atom A has nA(S) groundings, and all ground atoms are independent because the CNF is satisfied irrespective of their truth values. Note that nA(S) is the number of groundings of A consistent with S that can be formed using all the constants in the original CNF.

5. 2. Lifting the decomposition step

Clearly, if C can be decomposed into two or more CNFs such that no two CNFs share any unifiable literals, a lifted decomposition of C is possible (i.e., a decomposition of C into first-order CNFs on which LWMC can be called recursively). But the symmetry of the first-order representation can be further exploited. For example, if the CNF C can be decomposed into k CNFs C1, . . . , Ck sharing no unifiable literals and such that for all i, j, Ci is identical to Cj up to a renaming of the variables and constants, then LWMC(C) = [LWMC(C1)]k.

We formalize these conditions below.

Definition 1. The set of first-order CNFs {C1, 1, ... , C1,m1, ... , Ck, 1, . . . , Ck,mk} is called a lifted decomposition of CNF C under substitution constraints S if, given S, it satisfies the following three properties: (i) C = C1, 1 ∧ . .. ∧;Ck,mk; (ii) no two Ci, j’s share any unifiable literals; (iii) for all i, j, j′, such that j ≠ j′, Ci, j is identical to Ci, j′.a Proposition 1. If {C1, 1, . . . , C1, m1 . . . , Ck, 1, . . . , Ck,mk} is a lifted decomposition of C under S, then

( 3)

Rules for identifying lifted decompositions can be derived in a straightforward manner from the inversion argument in de Salvo Braz8 and the power rule in Jha et al. 15 An example of such a rule is given in the definition and proposition below.

Definition 2. A set of variables X = {x

1

, ... , x m

} is called a decomposer of a CNF C if it satisfies the following three properties: (i) for each clause Cj in C, there is exactly one variable xi in X such that xi appears in all atoms in Cj; (ii) if xi ∈ X appears as an argument of predicate R (say at position k in an atom having predicate symbol R), then all variables in all clauses that

Theorem 2. Algorithm WMC(C,W) correctly computes the weighted model count of CNF C under literal weights W.

Proof sketch. If all clauses in C are satisfied, all assignments to the atoms in C satisfy it, and the corresponding total weight is ∏A∈A(C )( WA + W¬A). If C has an empty unsatisfied clause, it is unsatisfiable given the truth assignment so far, and the corresponding weighted count is 0. If two CNFs share no atoms, the WMC of their conjunction is the product of the WMCs of the individual CNFs. Splitting on an atom produces two disjoint sets of worlds, and the total WMC is therefore the sum of the WMCs of the two sets, weighted by the corresponding literal’s weight. 

5. FIRST-ORDER CASE

We now lift PTP to the first-order level. We consider first the case of PKBs without existential quantifiers. Algorithms 2 and 3 remain essentially unchanged, except that formulas, literals and CNF conversion are now first-order. In particular, for Theorem 1 to remain true, each new atom Ai in Algorithm 2 must now consist of a new predicate symbol followed by a parenthesized list of the variables and constants in the corresponding formula Fi. The proof of the first-order version of the theorem then follows by propositionalization. Lifting Algorithm 4 is the focus of the rest of this section.

We begin with some necessary definitions. A substitution constraint is an expression of the form x = y or x ≠ y, where x is a variable and y is either a variable or a constant. (Much richer substitution constraint languages are possible, but we adopt the simplest one that allows PTP to subsume both standard function-free theorem proving and first-order variable elimination.) Two literals are unifiable under a set of substitution constraints S if there exists at least one ground literal consistent with S that is an instance of both, up to the negation sign. A (C, S) pair, where C is a first-order CNF whose variables have been standardized apart and S is a set of substitution constraints, represents the ground CNF obtained by replacing each clause in C with the conjunction of its groundings that are consistent with the constraints in S. For example, using upper case for constants and lower case for variables, and assuming that the PKB contains only two constants A and B, if C = R(A, B) ∧ (¬R(x, y) ∨ S(y, z) ) and S = {x = y, z ≠ A}, (C, S) represents the ground CNF R(A, B) ∧ (¬R(A, A) ∨ S(A, B) ) ∧ (¬R(B, B) ∨ S(B, B) ). Clauses with equality substitution constraints can be abbreviated in the obvious way (e.g., T(x, y, z) with x = y and z = C can be abbreviated as T(x, x, C) ).

We lift the base case, decomposition step, and splitting step of Algorithm 4 in turn. The result is shown in Algorithm 5. In addition to the first-order CNF C and weights on first-order literals W, LWMC takes as an argument an initially empty set of substitution constraints S which, similar to logical theorem proving, is extended along each branch of the inference as the algorithm progresses.

5. 1. Lifting the base case

The base case changes only by raising each first-order atom

A’s sum of weights to nA(S), the number of groundings of

A compatible with the constraints in S. This is necessary and

Algorithm 5 LWMC(CNF C, substs. S, weights W)

// Lifted base case
if all clauses in C are satisfied then
return ∏A∈A(C)(WA + W¬A)nA (S)
if C has an empty unsatisfied clause then return 0
// Lifted decomposition step
if there exists a lifted decomposition {C1, 1, . . . , C1,m1, . . . ,
Ck, 1, . . . , Ck,mk} of C under S then
return [LWMC (Ci, 1, S, W )]mi