how to plot a BDD as having two leaf nodes

[Nithin-Kamineni]

If I have a negation in the boolean expression I am getting the wrong boolean expression

In the case of the image I tried adding F2 : (x /\ y) / ~ z as a boolean expression to convert it into bdd. But it's not rightly pointing to give the correct output as shown in the image.

If the library developers want to investigate this issue I can provide the code to re-create this issue.

[slivingston]

@Nithin-Kamineni thanks for your report. Always best to give a minimal code example that demonstrates the issue. (It saves developers' time...)

[Nithin-Kamineni]

Sorry about that. Just want to make sure the project is still live.

The minimal code to recreate the error is below.

The code has 3 functions:
path.BooleanExpresions_to_BDD(...) # Code that needs to be debugged
path.BDD_to_NetworkXGraph() #for your ease of visualization (do not change)
path.VisuvaliseNetworkXGraph() #for your ease of visualization (do not change)

When I try to convert this boolean expression into a bdd it generates a slightly wrong bdd as you can see in the image.
(c low is going to 0 and c high is going to 1, but it must be reversed as in c low to 1 and c high to 0)

I stored the details of bdd in print('self.TreeMapInNodes', self.TreeMapInNodes) by traversing the bdd. you can use it to debug.

The output of the code is this:

from dd.autoref import BDD
import networkx as nx
import matplotlib.pyplot as plt
from matplotlib.colors import ListedColormap
import itertools

class PATH:
    def __init__(self, CrossbarGridSize = 16):
        self.CrossbarGridSize = CrossbarGridSize
        
        self.BDD = None
        self.Graph = None
        self.Expressions = None
        self.NodeIDMap = None
        self.TreeMapInNodes = {}

    def BooleanExpresions_to_BDD(self, variables, expressions):
        # Initialize the BDD manager
        self.BDD = BDD()
        self.BDD.configure(reordering=True)
        
        # Declare variables
        self.BDD.declare(*variables)
        
        # Define Boolean expressions
        self.expressions = expressions

        print('expressions', expressions)
        
        self.Expressions = {expression: self.BDD.add_expr(self.expressions[expression]) for expression in self.expressions}
        
        self.BDD.collect_garbage()
        self.BDD.reorder()

        #Traversing the nodes in the BDD and storing them in Dicts
        self.TreeMapInNodes = {}
        for rootKey in self.Expressions:
            queue = [self.Expressions[rootKey]]
            while(queue):
                curr_ele = queue.pop(0)
                [lvl, node1, node2] = self.BDD.succ(curr_ele)

                # Store current node structure in TreeMapInNodes
                lowValue = None
                highValue = None


                if node1.var:
                    lowValue = str(node1)
                else:
                    lowValue = 1 if not node1.negated else 0
                    
                if node2.var:
                    highValue = str(node2)
                else:
                    highValue = 1 if not node2.negated else 0

                self.TreeMapInNodes[str(curr_ele)] = {
                    "variable": curr_ele.var,
                    "level": lvl,
                    "negation": curr_ele.negated,
                    "low": lowValue,
                    "high": highValue
                }
                
                if node1.var!=None:
                        queue.append(node1)
                if node2.var!=None:
                    queue.append(node2)
        print('---------------------------------')
        print('self.TreeMapInNodes', self.TreeMapInNodes)
        print('---------------------------------')
        

    def BDD_to_NetworkXGraph(self):
        #Traversing the BDD
        self.NodeIDMap = {}
        for rootKey in self.Expressions:
            queue = [self.Expressions[rootKey]]
            id_lst = set()
            while(queue):
                curr_ele = queue.pop(0)
                [lvl, node1, node2] = self.BDD.succ(curr_ele)
        
                id_lst.add((str(curr_ele), curr_ele.var, curr_ele.negated))
                if(str(curr_ele) not in self.NodeIDMap):
                    self.NodeIDMap[str(curr_ele)]=[0,set()]
                self.NodeIDMap[str(curr_ele)][0]+=1
                self.NodeIDMap[str(curr_ele)][1].add((curr_ele.var, lvl))
                
                if node1.var!=None:
                    queue.append(node1)
                else:
                    if(str(node1) not in self.NodeIDMap):
                        self.NodeIDMap[str(node1)]=[0,{('0' if node1.negated else '1', 0)}]
                    self.NodeIDMap[str(node1)][0]+=1
                    
                if node2.var!=None:
                    queue.append(node2)
                else:
                    if(str(node2) not in self.NodeIDMap):
                        self.NodeIDMap[str(node2)]=[0,{('0' if node2.negated else '1', 0)}]
                    self.NodeIDMap[str(node2)][0]+=1
            
        
        # Initialize an undirected graph
        self.Graph = nx.DiGraph()
        ExpressionsRev = {str(self.Expressions[key]):key for key in self.Expressions}

        #adding nodes
        for id in self.NodeIDMap:
            literal = next(iter(self.NodeIDMap[id][1]))[0]
            level = next(iter(self.NodeIDMap[id][1]))[1]
            ExpressionRoot = None
            if(id in ExpressionsRev):
                ExpressionRoot = ExpressionsRev[id]
                literal = literal + '('+str(ExpressionsRev[id])+')'
                
            attributes = {'ID': id, 'literal': literal, 'level':level, 'ExpressionRoot': ExpressionRoot, 'BipartitePart':None}
        
            # Add nodes with attributes to the graph
            self.Graph.add_node(id, **attributes)
        
        # #Adding edges
        for rootKey in self.Expressions:
            queue = [self.Expressions[rootKey]]
            while(queue):
                curr_ele = queue.pop(0)
                [lvl, node1, node2] = self.BDD.succ(curr_ele)
                self.Graph.add_edge(str(curr_ele), str(node1), label='0')
                self.Graph.add_edge(str(curr_ele), str(node2), label='1')
                
                if node1.var!=None:
                    queue.append(node1)
                if node2.var!=None:
                    queue.append(node2)

    def VisuvaliseNetworkXGraph(self, bipartite=False):
        # Initialize position dictionary
        pos = {}
        
        # Parameters for positioning
        HORIZONTAL_SPACING = 1.0  # Horizontal distance between nodes
        VERTICAL_SPACING = 3.0    # Vertical distance between layers
        
        # Separate nodes into categories
        root_nodes = [node for node in self.Graph.nodes if self.Graph.in_degree(node) == 0]
        leaf_nodes = [node for node in self.Graph.nodes if self.Graph.out_degree(node) == 0]
        intermediate_nodes = [node for node in self.Graph.nodes if node not in root_nodes + leaf_nodes]

        if(bipartite):
            # Separate nodes by BipartitePart
            u1_nodes = [node for node in self.Graph.nodes if self.Graph.nodes[node].get('BipartitePart') == 'U1']
            u2_nodes = [node for node in self.Graph.nodes if self.Graph.nodes[node].get('BipartitePart') == 'U2']
    
            # Assign positions to U1 nodes (left column)
            for i, node in enumerate(u1_nodes):
                pos[node] = (0, (i * VERTICAL_SPACING))

            # Assign positions to U2 nodes (right column)
            for i, node in enumerate(u2_nodes):
                pos[node] = (2, (i * VERTICAL_SPACING))
                    
        else:
            # Assign positions to ExpressionRoot nodes (top layer)
            for i, node in enumerate(root_nodes):
                pos[node] = (i * HORIZONTAL_SPACING, 0)
                # print((i * HORIZONTAL_SPACING, 0))
            
            # Assign positions to Intermediate nodes based on BFS layers
            # Start BFS from all ExpressionRoot nodes
            layers = list(nx.bfs_layers(self.Graph, root_nodes))
            
            for lvl, nodes in enumerate(layers):
                # print("Layer:")
                for i, node in enumerate(nodes):
                    if node in intermediate_nodes:  # Only position intermediate nodes
                        # print(next(iter(idSet[node][1]))[0], end=",")
                        pos[node] = (i * HORIZONTAL_SPACING, -VERTICAL_SPACING * (lvl))
                        # print((i * HORIZONTAL_SPACING, -VERTICAL_SPACING * (lvl)))
                # print("\n")
    
            leafnodeYaxis = len(layers)
            if(self.Graph.nodes[layers[0][0]].get('literal')=="1"):
                leafnodeYaxis = leafnodeYaxis - 1
            
            # print("Literals")
            # Assign positions to Literal nodes (bottom layer)
            for i, node in enumerate(leaf_nodes):
                pos[node] = (i * HORIZONTAL_SPACING, -VERTICAL_SPACING * (leafnodeYaxis))
                # print((i * HORIZONTAL_SPACING, -VERTICAL_SPACING * (leafnodeYaxis)))
        
        # Draw nodes with labels
        node_colors = []
        for node in self.Graph.nodes:
            if self.Graph.nodes[node].get('ExpressionRoot') is not None:
                node_colors.append('orange')
            elif self.Graph.nodes[node].get('literal') == '0':
                node_colors.append('red')
            elif self.Graph.nodes[node].get('literal') == '1':
                node_colors.append('green')
            else:
                node_colors.append('lightblue')  # Default color for intermediate nodes

        nx.draw(self.Graph, pos, with_labels=False, node_color=node_colors, node_size=3000, font_size=10, arrows=True, arrowstyle='->', arrowsize=20)
        
        # Draw literals as node labels
        node_labels = nx.get_node_attributes(self.Graph, 'literal')
        nx.draw_networkx_labels(self.Graph, pos, labels=node_labels, font_size=12, font_color='black')
        
        # Draw edge labels
        edge_labels = nx.get_edge_attributes(self.Graph, 'label')
        nx.draw_networkx_edge_labels(self.Graph, pos, edge_labels=edge_labels, font_color='red')
        
        # Display the graph
        plt.title("0. BDD creation")
        plt.show()

path = PATH()
path.BooleanExpresions_to_BDD(variables = ['a', 'b', 'c'], expressions = {'F2': 'a & b | ~c'})
path.BDD_to_NetworkXGraph()
path.VisuvaliseNetworkXGraph()

[Nithin-Kamineni]

I kinda found what the issue is, whenever a node is negated the rest of the subtree's literal zeros and ones are different, and for the rest of the tree below the nodes that's having a negated node. This could be corrected by swapping the output to the opposite literal (0 to 1 or 1 to 0) for all the rest of the nodes that are negated nodes.

For example, taking the boolean expression input in the above code into consideration 'c' is wrong because c's negation is True. So we need to swap the 0 to 1 and 1 to 0. The same is the case for all the child nodes of c.

This could be easily corrected for a boolean expression by swapping the results 0 and 1 for negated nodes. But if we have multiple boolean expressions in the BDD it becomes almost impossible to make that change.

In case 1, we are getting the correct bdd(single boolean expression):
F2 : a1 & ~a0

but in case 2, we are getting wrong bdd(multiple boolean expression):
F2 : a1 & ~a0
F0 : a0

[johnyf]

Thank you for the question. For the expression (x /\ y) \/ ~ z mentioned above (appearing also in the form 'a & b | ~c' in the code above), a picture of the BDD can be created with:

import dd.autoref as _bdd


bdd = _bdd.BDD()
bdd.declare('x', 'y', 'z')
u = bdd.add_expr(r' (x /\ y) \/ ~ z ')
bdd.dump('bdd.png', roots=[u])

The result is the following. It is a BDD represented with negated edges, which are described in the documentation https://github.com/tulip-control/dd/blob/main/doc.md.

Any edge labeled with -1 is a negated one. Traversing a negated edge applies a negation (~) to the value of the Boolean function that the edge points to. For example, the node labeled with z has an outgoing dashed edge that connects to True. This edge is labeled with -1, so the result is ~ TRUE, which is FALSE. The edge is dashed, meaning that it is traversed when z takes the value FALSE.

So for example the path from the root node @7 to the x node, then to the z node, and to the True node via the solid edge from the z node means the following. It corresponds to the values x = FALSE and z = TRUE. The value of the BDD is FALSE, because along this path there is one negated edge (from the x node to the z node), which negates the TRUE value from the leaf node.

In contrast, the path from @7 to the x node, to the y node, to the z node, and to the True node via z = FALSE (the dashed edge from z) means the following. It corresponds to the values x = TRUE, y = FALSE, and z = FALSE. In total this path traverses two negated edges, so the BDD is TRUE in this case. The value TRUE results by the double negation ~ ~ TRUE (due to the two negated edges traversed).

In other words, the BDD with negated edges is as expected, for the expression (x /\ y) \/ ~ z.

The same Boolean function ((x /\ y) \/ ~ z) can be represented using a BDD without negated edges. Such a BDD has two leaf nodes, one node for FALSE, and one node for TRUE. Code for creating such a plot starting from a BDD that has negated edges can be found at: #41 (comment)
The result for the expression (x /\ y) \/ ~ z is the following, which is as expected. Node labels prefixed with - are negated Boolean functions, so the node -True is the leaf node for FALSE.

For example, the path from @7 for x = TRUE and y = TRUE leads to the node labeled True. The path from @7 for x = FALSE and z = FALSE leads to the node labeled True. In both cases the BDD value is TRUE, same as for the expression (x /\ y) \/ ~ z.

Also relevant: #29