appear as the same argument (namely at position k) of R are
included in X; and (iii) no pair of variables x
i
, x
j
∈ X such
that i ≠ j appear as different arguments of a predicate R in C.
For example, {x
1
, x
2
} is a decomposer of the CNF (R(x
1
) ∨
S(x
1
, x
3
) ) ∧ (R(x
2
) ∨ T(x
2
, x
4
) ) while the CNF (R(x
1
, x
2
) ∨ S(x
2
,
x
3
)) ∧ (R(x
4
, x
5
) ∨ T(x
4
, x
6
)) has no decomposer. Given a
decomposer {x1, ... , xm} and a CNF C, it is easy to see that for
every pair of substitutions of the form SX = {x1 = X, ... , xm = X}
and SY = {x1= Y, ... , xm = Y}, with X ≠ Y, the CNFs CX and CY
obtained by applying SX and SY to C do not share any unifiable
literals. A decomposer thus yields a lifted decomposition.
Given a CNF, a decomposer can be found in linear time.
When there are no substitution constraints on the variables in the decomposer, as in the example above, all CNFs
formed by substituting the variables in the decomposer with
the same constant are identical. Thus, k = 1 in Equation ( 3)
and m1 equals the number of constants (objects) in the PKB.
However, when there are substitution constraints, the CNFs
may not be identical. For example, given the CNF (R(x
1
) ∨
S(x
1
, x
3
)) ∧ (R(x
2
) ∨ T(x
2
, x
4
)) and substitution constraints
{x
1
≠ A, x
2
≠B}, the CNF formed by substituting {x
1
= A,
x
2
= A} is not identical to the CNF formed by substituting
{x
1
= C, x
2
= C}. Specifically, the first CNF is (R(A) ∨ T(A,
x
4
)) (since the clause (R (x
1
) ∨ S(x
1
, x
3
) ) has no valid groundings for the substitution x1 = A given the constraint x1 ≠ A) while
the second CNF is (R(C) ∨ S(C, x
3
) ) ∧ (R(C) ∨ T(C, x
4
) ).
A possible approach for solving this problem is illustrated below. For simplicity, assume that each variable x
in the decomposer is involved in exactly one substitution
constraint of the form x ≠ X (or x = X) where X is a constant.
Consider all possible combinations (Cartesian product)
of the constraints and their negation on the decomposer.
Observe that for each clause in the CNF, the subset of con-
stants O that satisfy all constraints in a given combination
also satisfy the following property: for any two distinct con-
stants Xi and Xj in O, the clause (possibly having no valid
groundings) obtained by substituting the decomposer vari-
able in it by X
i
is identical to the one obtained by substi-
tuting the decomposer variable by X
j
(up to a renaming of
constants and variables). Thus, a simple approach to decompose the CNF into subsets of identical but disjoint CNFs is to
partition the constants, with each part corresponding to a
possible combination of the constraints and their negation.
For instance, in our example CNF, given the decomposer X = {x
1
, x
2
}, and the constraints {x ≠ A, x ≠ B} where
x ∈ X, we have the following four combinations of constraints and their negation: ( 1) (x ≠ A, x ≠ B); ( 2) (x ≠ A,
x = B); ( 3) (x = A,x ≠ B); and ( 4) (x = A,x = B). Notice
that the last combination is inconsistent (has no solution) and therefore we can ignore it. Assuming that there
are five constants {A, B, C, D, E} in the domain, the three
consistent combinations given above yield the following
partition of the constants: {{C, D, E}, {A}, {B}}. The three
corresponding parts of the lifted decomposition of the
CNF are (for readability, we do not standardize variables
apart): ( 1) (R(x1) ∨ S(x1, x3) ) ∧ (R(x2) ∨ T (x2, x4) ), {x1, x2 ∈
{C, D, E}, x1 ≠ A, x2 ≠ B}; ( 2) (R (x1) ∨ S (x1, x3))∧(R(x2)
∨ T(x2, x4) ), {x1, x2 ∈ {B}, x1 ≠ A, x2 ≠ B}; and ( 3)
(R(x
1
) ∨S(x
1
, x
3
) ) ∧ (R(x
2
) ∨ T(x
2
, x
4
) ), {x
1
, x
2
∈ {A}, x
1
≠ A,
x
2
≠ B}.
In general, the partitioning problem described above can be
solved using constraint satisfaction techniques. In summary:
Proposition 2. Let X be a decomposer of a CNF C and let S be a
set of substitution constraints over C. Let {{X
1, 1, .. . , X1, m1}, . . . , {Xk, 1,
... , Xk, mk}} be a partition of the constants in the domain and let
C′ = {C1, 1, ... , C1, m 1, ... , Ck, 1, ... , Ck, m k} be such that (i) for all i, j,
j′, j ≠ j′, Ci, j is identical to Ci, j′ given S, and (ii) Ci, mi is a CNF
formed by substituting each variable in X by Xi, mi. Then C′ is a
lifted decomposition of C under S.
5. 3. Lifting the splitting step
Splitting on a non-ground atom means splitting on all groundings of it consistent with the current substitution constraints S.
Naively, if the atom has c groundings consistent with S this
will lead to a sum of 2c recursive calls to LWMC, one for each
possible truth assignment to the c ground atoms. However,
in general these calls will have repeated structure and can
be replaced by a much smaller number. The lifted splitting
step exploits this.
We introduce some notation and definitions. Let σA, S denote
a truth assignment to the groundings of atom A that is consistent with the substitution constraints S, and let ΣA,S denote
the set of all possible such assignments. Let C|σA, S denote the
CNF formed by removing A and ¬A from all clauses that satisfy
S, and setting to Satisfied all ground clauses that are satisfied
because of σA, S. This can be done in a lifted manner by updating the substitution constraints associated with each clause.
For instance, consider the clause R(x) ∨ S(x, y) and substitution constraint {x ≠ A}, and suppose the domain is {A, B, C}
(i.e., these are all the constants appearing in the PKB). Given
the assignment R(B) = True, R(C) = False and ignoring satisfied clauses, the clause becomes S(x, y) and the constraint
set becomes {x ≠ A, x ≠ B}. R(x) is removed from the clause
because all of its groundings are instantiated. The constraint
x ≠ B is added because the assignment R(B) = True satisfies
all groundings in which x = B.
Definition 3. The partition of ΣA,S is called a
lifted split of atom A for CNF C under substitution constraints
S if every part satisfies the following two properties: (i) all
truth assignments in have the same number of true
atoms; (ii) for all pairs σj, , C|σj is identical to C|σk.
Proposition 3. If is a lifted split of A for C
under S, then
where , ti, and fi are the number of true and
false atoms in σ respectively, and Si is S augmented with the
substitution constraints required to form C|σ.
Again, we can derive rules for identifying a lifted split
by using the counting arguments in de Salvo Braz8 and the
generalized binomial rule in Jha et al. 15 We omit the details
for lack of space. In the worst case, lifted splitting defaults
to splitting on a ground atom. In most inference problems,
