<p>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: <span class="math-container">$\mathsf{apply}(C,C',\circ)$</span> is done by bottom-up dynamic programming where for each pair of nodes <span class="math-container">$\alpha \in C, \beta \in C'$</span> structured similarly (same variable tested for OBDD or same node in the vtree respected for d-DNNF/SDD), one construct a product gate <span class="math-container">$v_{\alpha,\beta}$</span> computing <span class="math-container">$\alpha \circ \beta$</span>. 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).</p>
<ol>
<li><p><em>UniqueD</em>: it is well-defined from Theorem 10 stating that given a Boolean function, there exists a unique canonical compressed and trimmed SDD.</p>
</li>
<li><p>&quot;<em>alpha and beta are normalized for the same vtree node</em>&quot;: it means that both <span class="math-container">$\alpha$</span> and <span class="math-container">$\beta$</span> respects the same node <span class="math-container">$v$</span> of the vtree. It indeed means that <span class="math-container">$\alpha$</span> and <span class="math-container">$\beta$</span> use the same vtree, this is exactly what you need in order to make <span class="math-container">$\mathsf{apply}$</span> work. It actually is stated in the paper (under the pseudocode): to ensure normalization, if <span class="math-container">$\alpha$</span> respects <span class="math-container">$v$</span>, then its prime has to respect <span class="math-container">$v_l$</span> and its subs have to respect <span class="math-container">$v_r$</span> (the left/right children of <span class="math-container">$v$</span>).</p>
</li>
<li><p>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]).</p>
</li>
</ol>

CC BY-SA 4.0
2022-04-26T09:18:01.397Z
2022-04-26T09:18:01.397Z
holf
<p>I've been recently reading about decision diagrams and their variants and came across sentential decision diagrams (paper here <a href="http://reasoning.cs.ucla.edu/fetch.php?id=121&amp;type=pdf" rel="nofollow noreferrer">http://reasoning.cs.ucla.edu/fetch.php?id=121&amp;type=pdf</a>). 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.</p>
<p><a href="https://i.sstatic.net/nomPV.png" rel="nofollow noreferrer"><img src="https://i.sstatic.net/nomPV.png" alt="SDD Apply pseudocode" /></a></p>
<p>The first thing that I am failing to understand is the definition of <code>UniqueD()</code>, specifically the case where γ is neither true nor false. What does &quot;the unique SDD with elements γ&quot; mean? Would it be sufficient to use an arbitrary (consistent) mechanism for ordering the elements?</p>
<p>I'm also confused by the wording in the description of the algorithm, namely that &quot;alpha and beta are normalized for the same vtree node&quot;. Does this mean the vtrees of both have to fully match? or that they need to cover the same variables?</p>
<p>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 &quot;is consistent&quot;, the author means that the boolean function represented by that SDD has at least 1 satisfying assignment.</p>
<p>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.</p>

<implementation><binary-decision-diagrams>
Operations on Sentential Decision Diagrams
Lev Knoblock
# Operations on Sentential Decision Diagrams

(Asked by: username_0 on 2022-04-24)

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.

[![SDD Apply pseudocode](https://i.sstatic.net/nomPV.png)](https://i.sstatic.net/nomPV.png)

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.

**Tags:** implementation, binary-decision-diagrams


---

## 1 answers

### Answer by username_1 on 2022-04-26. Score: 2 | Accepted answer

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]).


---

