Inclusion–exclusion with an incomplete containment test#
This page proves that the inclusion–exclusion rule of the lifted solver (see Lifted probabilistic inference) computes the exact probability of a query, although the containment test it uses to cancel terms is not complete.
Statement of the problem#
For a conjunction \(K_1 \land \dots \land K_n\) of clauses with the same
free variables,
inclusion_exclusion_conjunction()
computes a weighted sum of the probabilities of the disjunctions
\(f(S) = \bigvee_{i \in S} K_i\), \(S\) a non-empty subset of
\(\{1, \dots, n\}\), lifting only the disjunctions whose weight is not
0. The weights are the Möbius weights of an order \(\preceq\) between
the disjunctions, which is built with
is_contained(). This test is
sound but not complete: it looks for a homomorphism between the
disjunctions, and a negated atom \(\lnot R(\bar x)\) is matched only by
the same negated atom, through the relation \(\bar R\) of
NegatedSymbol (negations_as_atoms), so that an implication that
holds because of a negation can be missed. The question is whether the
weighted sum is then still the probability of the conjunction.
The lemma#
Lemma. Let \(\preceq\) be a partial order on the non-empty subsets of \(\{1, \dots, n\}\) such that
(H1) \(T \subseteq S\) implies \(T \preceq S\), and
(H2) \(T \preceq S\) implies \(f(T) \models f(S)\).
Let \(\mu\) be defined by \(\sum_{T \preceq S} \mu(T) = 1\) for every \(S\), and \(w(S) = (-1)^{|S| + 1}\). Then for every probability measure,
A partial order is reflexive and transitive: transitivity is the third hypothesis, with (H1) and (H2).
The proof#
The second equality is the inclusion–exclusion principle. For the first, call \(C\) closed when \(T \preceq C\) implies \(T \subseteq C\). For closed \(C\), \(\{T : T \preceq C\} = \{T : \emptyset \neq T \subseteq C\}\) by (H1).
Closed sets are stable under non-empty intersection: if \(T \preceq U \cap V\), then \(U \cap V \subseteq U\) gives \(U \cap V \preceq U\) by (H1), so \(T \preceq U\) by transitivity and \(T \subseteq U\); likewise for \(V\). Every \(S\) thus has a smallest closed superset \(c(S)\), and for closed \(C\), \(c(S) \subseteq C\) if and only if \(S \subseteq C\).
\(c(S)\) is reached by iterating \(S \mapsto S \cup \bigcup \{T : T \preceq S\}\), which stays within every closed superset of \(S\). Each step keeps the event: \(T \preceq S\) gives \(f(T) \models f(S)\) by (H2), so \(f(S \cup T) \equiv f(S)\); hence \(P[f(c(S))] = P[f(S)]\).
For \(\varphi \in \{\mu, w\}\) and closed \(C\), put
For \(w\) this is the alternating sum, \(F_w(C) = 1\); for \(\mu\) it is the recursion at \(C\) together with the first description of \(\{T : T \preceq C\}\), \(F_\mu(C) = 1\). Möbius inversion on the poset of closed sets ordered by inclusion gives
for every closed \(C\). Grouping both sums of the lemma by \(c(S)\), and using \(P[f(c(S))] = P[f(S)]\), gives the claim. \(\square\)
Equivalently, with a bottom element \(\hat 0\) added, \(w(S) = -\mu_B(\hat 0, S)\) on the Boolean lattice of the subsets and \(\mu(S) = -\mu_\preceq(\hat 0, S)\) on the order \(\preceq\); \(S \mapsto c(S)\) is a closure operator on both, with the same quotient \(L\), as \(\preceq\) and \(\subseteq\) coincide on closed sets. Rota’s closure theorem [Rota1964] then gives \(\sum_{c(S) = C} w(S) = -\mu_L(\hat 0, C) = \sum_{c(S) = C} \mu(S)\). Spiegel and O’Donnell [Spiegel1997] treat the Möbius function of incidence algebras at length.
Completeness of the containment test is never used: a containment that is
not found only makes the closure coarser, cancelling fewer terms, and never
makes the sum wrong. A term that is not cancelled is lifted like the
others; if the algorithm cannot lift it, it is marked NonLiftable, the
plan is impure, and the query is declined unless another rule lifts it.
What the implementation guarantees#
_formulas_weights receives each non-empty set \(S\) of indices of
clauses with the disjunctive normal form of \(f(S)\), which
inclusion_exclusion_conjunction computes with convert_ucq_to_ccq.
It builds the relation \(T \preceq S\) when \(T \subseteq S\), or
when is_contained(f(S), f(T)) holds, that is when the test finds that
\(f(T)\) implies \(f(S)\), both directions being recorded when both
hold. It closes the relation transitively (Warshall’s algorithm on the
\(2^n - 1\) sets), and merges the sets contained in each other into
classes, each represented by one of its sets with the most clauses. The
order between the representatives is passed to mobius_weights, whose
mobius_function computes \(\mu(S) = 1 - \sum_{T \prec S} \mu(T)\).
inclusion_exclusion_conjunction lifts the formula of each
representative whose weight is not 0, and WeightedNaturalJoin adds the
probabilities of the answers, multiplied by the weights.
(H2) holds: a subset gives a disjunction of fewer clauses, which implies the other;
is_containedis sound; and implication is transitive.(H1) holds: every subset is recorded, whatever
is_containedfinds.Transitivity holds by the closure.
On the sets, the relation is reflexive and transitive but need not be antisymmetric, when two sets are in the same class. The proof does not use antisymmetry: it uses the recursion only at closed sets, and the weights that the code gives, the weight of a class to its representative and 0 to its other sets, satisfy the recursion for every set, as the classes below a set are those below its representative. Within a class the disjunctions are equivalent by (H2), so lifting the representative alone gives the probability of each.
For an answer \(\theta\) of the free variables, the lemma applies to the events \(f(S)\theta\). The weighted join keeps the answers in the plans of all the terms it adds; an answer missing from the plan of a term \(f(S)\) has \(P[f(S)\theta] = 0\), hence, \(K_i\) implying \(f(S)\) for \(i \in S\), a clause of probability 0, and probability 0 for the conjunction.
Relation to the literature#
Dalvi and Suciu [Dalvi2012] cancel the terms of inclusion–exclusion with the Möbius function of the lattice of the disjunctions, ordered by implication: this is the case of the lemma where \(\preceq\) is the full implication order, and their identity \(P(Q) = -\sum_{v < \hat 1} \mu_L(v, \hat 1)\, P(d_v)\) is the special case of the lemma for it.
The “improved inclusion–exclusion identities” of Narushima [Narushima1982], Dohmen [Dohmen1999] and Chen and Qian [Chen2018] also use a closure operator on the lattice of the subsets, but they drop terms of the sum rather than reweighting them, and are not what the implementation does.
References#
Y. Chen and J. Qian. Inclusion-exclusion by ordering-free cancellation. arXiv:1801.04706, 2018.
K. Dohmen. On sums over partially ordered sets. The Electronic Journal of Combinatorics, 6, R34, 1999.
H. Narushima. Principle of inclusion-exclusion on partially ordered sets. Discrete Mathematics, 1982. doi:10.1016/0012-365X(82)90221-7.
G.-C. Rota. On the foundations of combinatorial theory I. Theory of Möbius functions. Zeitschrift für Wahrscheinlichkeitstheorie und verwandte Gebiete, 2, 340–368, 1964.
E. Spiegel and C. J. O’Donnell. Incidence Algebras. Monographs and Textbooks in Pure and Applied Mathematics 206. Marcel Dekker, 1997.
[Dalvi2012] is listed in Lifted probabilistic inference.