Merging ZDD with the master branch

[trolando]

I just had a first good look at the ZDD branch that needs to be merged eventually with master.

Most of is it good state.

Unfortunately the examples are not all working well, the satdd program has a weird crash that I need to figure out first. And I'm also not completely happy with all the code duplication related to reference management.

I also noticed that I was working on an inventory of desirable ZDD functions, based on what is supported by CUDD and the EXTRA extension to ZDD. What I actually implemented in the ZDD branch is everything I needed to play with "representing SAT clauses using a ZDD" which is still somewhat limited, although usable. So I need to convert this into a better overview or maybe a roadmap of some sorts.

Another observation is that a lot of the functionality that is in MTBDD would be useful for ZDD. For example, why should we duplicate all the leaf management? First of all most use cases probably don't have mixed decision diagrams. So the only expected leaves would be either the int/double/fraction/custom leaf that is expected, or False if some input is not in the domain of the set.

Then another thing I noticed is that I was experimenting with a kind-of complement edge to have a little bit of compression on the tree. It's not a true complement edge, they don't work well with ZDDs. But I don't completely recall the semantics and how it was supposed to work. I'd have to reverse engineer that.

[SSoelvsten]

With regards to complement edges: The semantics of attribute edges for Zero-suppressed decision diagrams as given in Section 2.5 of Zero-suppressed BDDs and their applications by Shin-ichi Minato:

Minato[16] presented a similar technique for ZBDDs, called 0-element edge, but the function of the attribute is slightly different from conventional ones. This attribute indicates that the pointing subgraph includes the null combination vector \00 : : : 0" in the set of combinations

For example, the result of ( P U { 00 : : : 0 } ) depends only on whether or not P includes the null combination. In such a case, we can get the result in a constant time when using 0-element edges; otherwise we have to repeat the expansion until P becomes a terminal node.

In other words. The 0-element edge is set, if the all-false path from the root should lead to the true sink.

[trolando]

This might also have been how I did it in my implementation, but I am not quite sure because I don't remember it like that. Or maybe I just came at the same result from a different angle.

[SSoelvsten]

I've been taking a look at the zdd branch, and here are some comments of mine. You should take into account, that I primarily think ZDDs in terms of families of subsets of the natural numbers/set of bitvectors as they were presented originally by Shin-ichi Minato and later by Donald Knuth. I'm also definitely biased towards this view, since my own zdd branch exclusively focuses on this family of sets intuition in the interface.

So, if you aim for a "same use and way to think about it" but with the strength of ZDDs, you should take many of these questions/suggestions with a grain of salt.

• zdd_nithvar makes semantically little sense. The return zdd_makenode(var, zdd_true, zdd_false); will always apply the reduction rule to just return zdd_true.

  • So, the zdd_nithvar essentially represents the set of the empty set { Ø }.
  • If you want to keep the BDD-like semantics, you'd need a second argument with the domain, such that all other's can be don't care variables, while this one is forced to false (i.e. skipped). Or, I suppose you intend the zdd_ite to compensate for this? If the prior, what about zdd_ithvar should it not also have a don't care on the remaining domain?

• You have a zdd_from_mtbdd and a zdd_to_mtbdd function. I'd advocate for either adding two aliases mtbdd_from_zdd and mtbdd_to_zdd or rename zdd_to_mtbdd into mtbdd_from_zdd (the latter inspired by OCaml etc.)

• Given the original family of sets interpretation of ZDDs it probably is a good idea to clarify that the zdd_set_union function is not the union per se but rather that would be zdd_or. I think this primarily is providing a good distinction in the documentation.

• The 0xffffffff variable would be more self-explanatory if it was placed in a global constant/macro.

• zdd_exists:

  • Let me start with something different. It will make sense for the next bulletpoint.

    The subset0 and subset1 functions, in which one or more variables are fixed to a specific value (similar to restrict in the original sense by Bryant), are not provided. For that one, the semantics would be that one needs to recursively solve the children, and then (depending on the assignment to the variable) keep the node or not.

  • But, on the other hand in zdd_exists the node is always kept.

    result = zdd_makenode(vars_var, result, result);
    

    I'm not exactly sure how existential quantification should be understood semantically. I see arguments for both sides. On the one side, it follows the BDD semantics and it also works better in conjunction with other operations. On the other hand, given a family of sets F where you want to existentially quantify the variable x_i you essentially construct the following family.

    • { {x_i} ∪ s | s ∈ F} ∪ { s \ {x_i} | s ∈ F}

• zdd_ite:

  • For readability's sake (and performance's), you may want to change this line into minvar = c_var < minvar ? c_var : minvar.

  • Forwarding through the domain can be made a little neater with a do-while loop.

  • Based on your own comment you are missing a trivial case. Or is it taken over by the if (a == c || c == zdd_false) return zdd_and(a, b);? If so, maybe a comment about that would be good. Reiterating in the same comment, that the domain is the conjunction of the variables would also be good.

These comments aside, the zdd_or, zdd_and, and zdd_diff matches the pseudocode of Minato (Notice, the original "Zero-suppressed BDDs for Set Manipulation in Combinatorial Problems" has an error in one of these). The zdd_not function seems correct to me, since it also given the universe (dom) to be able to compute the complement.

[trolando]

Quick response before I head out of the office to one particular thing, the "zdd_set_XXX" methods are a bit misleading as they are about the "domain sets" which are a unique Sylvan thing (compared to CUDD). In CUDD a manager has a global "variable domain" where the same variables are expected in all decision diagrams in the manager. Sylvan does not do this, instead it often expects a "variable domain" which is called a "set" in Sylvan currently. I agree that this is confusing and should consider renaming this so it does not introduce more confusion.

[SSoelvsten]

I still have to read the Master Thesis of Hajighasemi in detail, but a quick glance at it repeats the same idea of a more BDD-like view on most algorithms. If that is the case, then many of the comments above turn into an "all good". :-)

[SSoelvsten]

I just fell over this figure in Minato's paper on ZDDs . It shows the intended rule for the attribute edge - I'll leave it here, assuming it could potentially be of some value.

[trolando]

There is now some ZDD support in the master branch, but a lot of interesting ZDD functionality is not yet implemented.

[SSoelvsten]

Here is a list of not yet implemented features that were not mentioned in the comments of sylvan/sylvan_zdd.h.

• [ ] C++ support
• [ ] Boolean Polynomials as used in PolyBoRi

[SSoelvsten]

It should also be noted, if C++ support is added, you almost for free get multiple benchmarks ready to evaluate Sylvan's performance against CUDD. Specifically, the following three combinatorial problems that test the Apply function (and its equivalents) and the SatCount function:

• [x] N-Queens: Number of possible ways to place N queens places on a NxN board, such that they do not threaten eachother.
• [x] Tic-Tac-Toe: The number of draws possible in a 4x4x4 Tic-Tac-Toe with N crosses placed.
• [x] Knights-Tour: Number of hamiltonian paths/cycles on an MxN chessboard

As I am getting closer to Adiar v2.0, I ams also getting these two benchmarks to work for ZDDs:

• [x] Picotrav: Given two circuits, create the ZDDs for each output gate and verify they are equivalent. (This also investigates the product construction as above but also negation and equality checking)
• [ ] QBF: Given a QCIR circuit for a Quantified Boolean Formula (QBF), solve the circuit, and if possible provide a witness/counter-example. (This focuses on multi-variable quantification)