Operations on Sentential Decision Diagrams

Question

I've been recently reading about decision diagrams and their variants and came across sentential decision diagrams (paper here http://reasoning.cs.ucla.edu/fetch.php?id=121&type=pdf). The paper describes a polytime algorithm for combining two SDDs via some boolean operation and I'm having a hard time understanding exactly what the pseudocode is describing.

The first thing that I am failing to understand is the definition of UniqueD(), specifically the case where γ is neither true nor false. What does "the unique SDD with elements γ" mean? Would it be sufficient to use an arbitrary (consistent) mechanism for ordering the elements?

I'm also confused by the wording in the description of the algorithm, namely that "alpha and beta are normalized for the same vtree node". Does this mean the vtrees of both have to fully match? or that they need to cover the same variables?

I'd also appreciate if someone could confirm that my understanding of line 10 of the algorithm is correct. If I'm not misunderstanding, by "is consistent", the author means that the boolean function represented by that SDD has at least 1 satisfying assignment.

I've tried to watch Darwiche's videos on SDDs, but they only really mention the algorithm in passing, and looking at the code of the SDD package did not help me at all. Also, my apologies if this belongs more on the CS stackexchange given the nature of the question. Considering the topic I wasn't sure which site to ask on.

Answer 1

I try to address your questions one after the other. I agree that the description of the algorithm is really succinct. To understand it better, I would encourage you to parallel this algorithm with the one for OBDD and d-DNNF. The idea is always the same: $\mathsf{apply}(C,C',\circ)$ is done by bottom-up dynamic programming where for each pair of nodes $\alpha \in C, \beta \in C'$ structured similarly (same variable tested for OBDD or same node in the vtree respected for d-DNNF/SDD), one construct a product gate $v_{\alpha,\beta}$ computing $\alpha \circ \beta$. It differs a bit for SDD as the circuit is also normalized during this phase. Sidenote: this is exactly the same construction for product automata (DFA or tree automata).

1. UniqueD: it is well-defined from Theorem 10 stating that given a Boolean function, there exists a unique canonical compressed and trimmed SDD.

2. "alpha and beta are normalized for the same vtree node": it means that both $\alpha$ and $\beta$ respects the same node $v$ of the vtree. It indeed means that $\alpha$ and $\beta$ use the same vtree, this is exactly what you need in order to make $\mathsf{apply}$ work. It actually is stated in the paper (under the pseudocode): to ensure normalization, if $\alpha$ respects $v$, then its prime has to respect $v_l$ and its subs have to respect $v_r$ (the left/right children of $v$).

3. Line 10 is exactly what you understand. You do not need to add inconsistent primes (they will never evaluate to true; and this case is excluded from the definition of partitions [Definition 1]).