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.