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
// Lifted splitting step
Choose an atom A
Let {∑( 1) A,S , . . ., ∑(l) A,S} be a lifted split of A for C under S
return ∑(l ) i = 1;ni W ti A W fi ¬A LWMC (C|σj; Sj, W )
where ni, ti, fi, σj and Sj are as in Proposition 3
a Throughout this paper, when we say that two clauses are identical, we mean
that they are identical up to a renaming of constants and variables.