Compact Shared Reduced Binary Decision Diagrams with negated identifiers Consider a BDD implementation in which each bdd in the system has a unique positive integer identifying it (thanks to canonicity and as common implementation designs follow, by utilizing a hashmap). I was thinking of assigning a negative integer to a bdd in order to represent its negation. So say bdd id -3 will be bdd id 3 with just flipping the terminal nodes when processing them. The building blocks for new bdds would be the terminal T,F nodes, and the "ith var" bdd, where if the ith var is false then we get an id being the negation of the id of the bdd representing the ith var being true.

My question is whether such design breaks canonicity, or I can still rely on bdds having same (positive or negative) identifier to be equal.
Found the answer in the paper Shared Binary Decision Diagram with Attributed Edges for Efficient Boolean function Manipulation.

more accurate treatment can be found in section 2.3 in Proving circuit correctness using formal comparison between expected and extracted behaviour (pdf download available).

in short, canonicity is preserved if, quoting from tvandijk.nl/pdf/mscthesis.pdf page 15 "Complement edges" (The Parallelization of Binary Decision Diagram operations for model checking, thesis by Tom van Dijk):

"Minato [35] proposes the following constraints:

1) Only 0 is used as the value of a leaf.

Alternative rule 1 : only 1 is used as the value of a leaf.

Alternative rule 2 : do not allow complement edges on leaves.

2) No complement edges are allowed on 0-edges.

Alternative rule: no complement edges are allowed on 1-edges"

note that this is not a "true" restriction as if we decide that only hi edges are complemented, and we want to create a node with its lo edge being complemented, we just negate the whole node, like a?b:not(c) == not(a?not(b):c).