directly be transformed into a sum of products. Computing the probability of DNF formulae thus involves solving the disjoint-sum-problem, and therefore is itself a \#P-hard problem. Various algorithms have been developed to tackle this problem. The pD-engine HySpirit [@Fuhr00] uses the inclusion-exclusion principle, which is reported to scale to about ten proofs. For ICL, which extends PHA by allowing non-disjoint proofs, [@Poole00] proposes a symbolic disjoining algorithm, but does not report scalability results. Our implementation of ProbLog employs Binary Decision Diagrams (BDDs) [@Bryant86], an efficient graphical representation of a Boolean function over a set of variables, which scales to tens of thousands of proofs; see Section \[sec:BDD\] for more details. PRISM [@SatoKameya:01] and PHA [@Poole:93] differ from the systems mentioned above in that they avoid the disjoint-sum-problem by requiring the user to write programs such that proofs are guaranteed to be disjoint.

On the other hand, as the *explanation probability* $P_x$ exclusively depends on the probabilistic facts used in one proof, it can be calculated using a simple branch-and-bound approach based on the SLD-tree, where partial proofs are discarded if their probability drops below that of the best proof found so far.

Approximative Inference
-----------------------

As the size of the 