in propositional inference that can be ported to LWMC
include pure literals, clause learning, clause indexing, and
random restarts. 2, 3, 23
Caching/Memoization In a typical inference, LWMC will
be called many times on the same subproblems. The solutions of these can be cached when they are computed, and
reused when they are encountered again. (Notice that a
cache hit only requires identity up to renaming of variables
and constants.) This can greatly reduce the time complexity of LWMC, but at the cost of increased space complexity.
If the results of all calls to LWMC are cached (full caching),
in the worst case LWMC will use exponential space. In practice, we can limit the cache size to the available memory and
heuristically prune elements from it when it is full. Thus, by
changing the cache size, LWMC can explore various time/
space tradeoffs. Caching in LWMC corresponds to both caching in model counting23 and recursive conditioning4 and to
memoization of common subproofs in theorem proving.
Knowledge-Based Model Construction KBMC first uses
logical inference to select the subset of the PKB that is relevant to the query, and then propositionalizes the result and
performs standard probabilistic inference on it. 25 A similar
effect can be obtained in PTP by noticing that in Equation
2 factors that are common to Z(K ∪ {(Q, 0)}) and Z(K) cancel
out and do not need to be computed. Thus we can modify
Algorithm 3 as follows: (i) simplify the PKB by unit propagation starting from evidence atoms, etc.; (ii) drop from the
PKB all formulas that have no path of unifiable literals to
the query; (iii) pass to LWMC only the remaining formulas,
with an initial S containing the substitutions required for
the unifications along the connecting path(s).
We now state two theorems (proofs are provided in the
extended version of the paper) which compare the efficiency
of PTP and first-order variable elimination (FOVE). 8, 18
Theorem 4. PTP can be exponentially more efficient than FOVE.
Theorem 5. LWMC with full caching has the same worst-case
time and space complexity as FOVE.
De Salvo Braz’s FOVE8 and lifted BP24 completely shatter
the PKB in advance. This may be wasteful because many of
those splits may not be necessary. In contrast, LWMC splits
only as needed.
PTP yields new algorithms for several of the inference
problems in Figure 1. For example, ignoring weights and
replacing products by conjunctions and sums by disjunctions
in Algorithm 5 yields a lifted version of DPLL for first-order
theorem proving.
Of the standard methods for inference in graphical
models, propositional PTP is most similar to recursive
conditioning4 and AND/OR search9 with context-sensitive
decomposition and caching, but applies to arbitrary PKBs,
not just Bayesian networks. Also, PTP effectively performs
formula-based inference13 when it splits on one of the auxiliary atoms introduced by Algorithm 2.
PTP realizes some of the benefits of lazy inference for
relational models10 by keeping in lifted form what lazy inference would leave as default.
the PKB will contain many hard ground unit clauses (the evidence). Splitting on the corresponding ground atoms then
reduces to a single recursive call to LWMC for each atom.
In general, the atom to split on in Algorithm 5 should be
chosen with the goal of yielding lifted decompositions in
the recursive calls (e.g., using lifted versions of the propositional heuristics23).
Notice that the lifting schemes used for decomposition
and splitting in Algorithm 5 by no means exhaust the space of
possible probabilistic lifting rules. For example, Jha et al. 15
and Milch et al. 16 contain examples of other lifting rules.
Searching for new probabilistic lifted inference rules, and
positive and negative theoretical results about what can be
lifted, looks like a fertile area for future research.
The theorem below follows from Theorem 2 and the arguments above.
Theorem 3. Algorithm LWMC(C, 0/, W) correctly computes the
weighted model count of CNF C under literal weights W.
5. 4. Extensions and discussion
Although most probabilistic logical languages do not include
existential quantification, handling it in PTP is desirable for
the sake of logical completeness. This is complicated by the
fact that skolemization is not sound for model counting
(skolemization will not change satisfiability but can change
the model count), and so cannot be applied. The result of
conversion to CNF is now a conjunction of clauses with universally and/or existentially quantified variables (e.g., [∀x∃y
(R(x, y) ∨ S(y))] ∧ [∃u∀v∀wT(u, v, w)]). Algorithm 5 now
needs to be able to handle clauses of this form. If no universal quantifier appears nested inside an existential one, this
is straightforward, since in this case an existentially quantified clause is just a compact representation of a longer one.
For example, if the domain is {A, B, C}, the unit clause ∀x∃y
R(x, y) represents the clause ∀x (R(x, A) ∨ R(x, B) ∨ R(x, C) ).
The decomposition and splitting steps in Algorithm 5 are
both easily extended to handle such clauses without loss
of lifting (and the base case does not change). However, if
universals appear inside existentials, a first-order clause
now corresponds to a disjunction of conjunctions of propositional clauses. For example, if the domain is {A, B}, ∃x∀y
(R(x, y) ∨ S(x, y) ) represents (R(A, A) ∨ S(A, A) ) ∧ (R(A, B) ∨
S(A, B)) ∨ (R(B, A) ∨ S(B, A)) ∧ (R(B, B) ∨ S(B, B)). Whether
these cases can be handled without loss of lifting remains
an open question.
Several optimizations of the basic LWMC procedure in
Algorithm 5 can be readily ported from the algorithms PTP
generalizes. These optimizations can tremendously improve
the performance of LWMC.
Unit Propagation When LWMC splits on atom A, the
clauses in the current CNF are resolved with the unit
clauses A and ¬A. This results in deleting false atoms, which
may produce new unit clauses. The idea in unit propagation is to in turn resolve all clauses in the new CNF with
all the new unit clauses, and continue to do this until no
further unit resolutions are possible. This often produces
a much smaller CNF, and is a key component of DPLL
that can also be used in LWMC. Other techniques used