BDD Visualizer

This tool generates visualizations of BDDs.

Specify the BDDs you would like to see in the textbox below and press the “Submit” button.

Filename used to save the BDD visualization(s):

Multiple print statements are supported when using file extensions “ps”, “ps2”, “pdf”, “dot”, and “txt”. Using any other file extension will cause the graph of only the first print statement to be generated.

; Sample input - creates 2 BDDs and displays them both joined and separate
; Text following a semicolon is ignored (comment)
; T,t and F,f are reserved for True and False, respectively
; Variables parsed first will occur near the leaves of the BDD
; Variables parsed last will occur near the root of the BDD

order(var1, var3, var2) ; This is used to control BDD variable ordering
                        ; The list can be any length>0 and is terminated by ')'

or(var1, var2, var3) ; BDD $1 Created

ite(x, xor(y, var1, T), or(y, F)) ; BDD $2 Created

print($1, $2) ; Prints BDDs $1, $2 to page 1 of the file
              ; Node sharing between BDDs is maintained
              ; 'print' statements do not create BDDs

print($1) ; Prints BDD $1 to page 2 of the file

print($2) ; Prints BDD $2 to page 3 of the file

;-------------------------------------------------------------------------

; Example from Lewis Carrol -
; Coloured flowers are always scented.
; I dislike flowers that are not grown in the open air.
; No flowers grown in the open air are colourless.
; Do I dislike all flowers that are not scented?
; If the conjunction is exactly 'False' then the answer to the question
; is yes, otherwise the answer is no and a path to True gives the reason
print(
      and(
          imp(Coloured, Scented)
          imp(-OpenAir, -Like)
          imp(OpenAir, Coloured)
          not(imp(-Scented, -Like))
      )
) ; Prints a BDD to page 4 of the file.

A tutorial can be found here: BDD Visualizer Tutorial - Part 1, Part 2, Part 3.

Some more examples can be found here: Constructing BDDs QuickStart.

This tool makes use of SBSAT and Graphvis.

Comments and suggestions are welcome.

BDD Visualizer