Version 19 of Simple BDD

Updated 2016-09-19 18:19:08 by SEH

BDD - Binary Decision Diagram.

One of the packages to work with them is BuDDy . It can be used to compute logical formulas, search for SAT problem solutions, etc.

Nuri's SAT Algorithms page contains a simple SAT generator for factorization problem. Also it contains two solvers, both in Perl.


Biddy is a multi-platform academic Binary Decision Diagrams package. It includes bddview, a pure Tcl/Tk script for visualization of BDDs, and BDD Scout, a demo application demonstrating the capability of Biddy and bddview. Packages for different operating systems are available, including those for GNU/Linux and MS Windows.

http://biddy.meolic.com/bddscout1.2-screenshot2-small.png

Biddy is free software released under GPL. Biddy uses ROBDDs with complement edges. Biddy supports automatic garbage collection and sifting algorithm. Biddy is oriented towards readable and comprehensible source code in C. Biddy is used in EST , a tool for formal verification of systems.

BDD Scout v1.4 has been updated on Aug 25, 2015


Cucumber is a professionally-supported open source BDD testing/"executable specification" tool with multiple language implementations, including Tcl.


Below is a BDD package in Tcl using algebraic types. It was written after my implementation in Haskell, and, actually, compares very well to Haskell implementation - 228 Tcl lines (~150 lines of pure code) with comments and tests against 108 lines without comments and just one test.

 # --------------------------------------------------------------
 # BDD - Binary Decision Diagram (a variant of)
 # It is a tool to manipulate logical formulas by their
 # truth tables, solving small SAT problems, optimizing formulas,
 # etc.
 #
 # You can read about BDD at BuDDy homepage:
 # http://www.itu.dk/research/buddy/
 #
 # Presented here is a variant of BDD described by
 # algebraic types.
 #
 # Functions and procedures:
 # T - total true
 # F - total false
 # lx n - get a BDD for x_$n logical variable
 # lnot e - logical inverse of BDD
 # land a b - logical and of two BDD's
 # lor a b - logical or of two BDD's
 # lsatset e - compute a list of satisfy sets for
 #             CNF represented by BDD.
 #
 # Note that for any non-trivial logical formula the size of
 # its BDD depends on variable ordering very much.

 # Use the [Algebraic Types]:
 source atypes.tcl

 # --------------------------------------------------------------
 # BDD structure:
 # F - total false
 # T - total true
 # D bdd1 bdd2 - decision point
 # R bdd - a case of D bdd1 bdd2 where bdd1==bdd2==bdd
 atype BDD                \
        {F}                \
        {T}                \
        {D bdd1 bdd2}        \
        {R bdd}

 # Pair is a tuple is a product of two sets.
 # We use it for matching of two different values simultaneously.
 atype Pair {Pair a b}

 # --------------------------------------------------------------
 # Simplest operation on BDD is inversion, negation, logical NOT - whatever.
 # It does not change structure (D and R), it only changes values -
 # F to T and T to F.
 # The most easy way to describe it is to use recursion:
 proc lnot {bdd} {
        match $bdd {
                {F} { return [T] }
                {T} { return [F] }
                {D $bdd1 $bdd2} { return [D [lnot $bdd1] [lnot $bdd2]]}
                {R $bdd} { return [R [lnot $bdd]]}
        }
 }

 # --------------------------------------------------------------
 # We can create representation for logical variables, represented
 # by their order position. We will start from 1 instead of 0 for
 # reasons explained later.
 # Also you should note that truth table for x_1 is
 # 01, 0011, 00001111, etc, depending on what total number of variables
 # is in the BDD.
 # Truth table for x_2 is 0101, 00110011, 0000111100001111 - just as
 # easy.
 # Truth table for ~x_1 is 10, 1100...

 # Auxiliary routine that compute a structure for variable representation.
 proc _lx {n} {
        set r [D [F] [T]]
        while {$n>1} {
                set r [R $r]
                incr n -1
        }
        return $r
 }

 # n (variable position number) has special meaning here.
 # Positive values of n means that we want to get BDD for x_n, while
 # negative values of n means that we want to get BDD for ~x_n.
 # That's why n shouldn't be zero.
 proc lx {n} {
        if {$n>0} {
                return [_lx $n]
        } else {
                return [lnot [_lx [expr -($n)]]]
        }
 }

 # --------------------------------------------------------------
 # Okay, lets define logical and.
 # We again start from auxiliary routine that does straight computation
 # of land without any twists.
 proc _land {a b} {
        # First four matches use facts about
        # zero (F) and unit (T) of logical and.
        # The we _land different structures.
        match [Pair $a $b] {
                {Pair {F} _} { return [F] }
                {Pair {T} $x} { return $x }
                {Pair _ {F}} { return [F] }
                {Pair $x {T}} { return $x }
                {Pair {D $a $b} {D $x $y}} {
                        return [D [_land $a $x] [_land $b $y]]
                }
                {Pair {R $a} {R $x}} {
                        return [R [_land $a $x]]
                }
                {Pair {D $a $b} {R $x}} {
                        return [D [_land $a $x] [_land $b $x]]
                }
                {Pair {R $a} {D $x $y}} {
                        return [D [_land $a $x] [_land $a $y]]
                }
        }
 }

 # Define equality relation for our structure.
 proc _leq {a b} {
        match [Pair $a $b] {
                {Pair F F} { return 1 }
                {Pair T T} { return 1 }
                {Pair {D $a $b} {D $x $y}} { return [expr [_leq $a $x] && [_leq $b $y]] }
                {Pair {R $a} {R $x}} { return [_leq $a $x] }
                {_} { return 0 }
        }
 }

 # Then we have to simplify expression, for example
 # D T T -> T
 # D {D T F} {D T F} -> R {D T F}
 # etc.
 proc _lsimp {e} {
        match $e {
                {D $a $b} {
                        set a [_lsimp $a]
                        set b [_lsimp $b]
                        # If both legs are equal, then we may reduce
                        # structure to R and try to simplify further
                        if {[_leq $a $b]} {
                                return [_lsimp [R $a]]
                        } else {
                                return [D $a $b]
                        }
                }
                {R $x} {
                        set x [_lsimp $x]
                        match $x {
                                {T} { return [T] }
                                {F} { return [F] }
                                $x { return [R $x]}
                        }
                }
                $x { return $x }
        }
 }

 # Now we ready for full implementation of land:
 proc land {a b} {
        # Straight and:
        set r [_land $a $b]
        # And simplify before return:
        return [_lsimp $r]
 }

 # --------------------------------------------------------------
 # Then we may define logical or:
 proc lor {a b} {
        return [lnot [land [lnot $a] [lnot $b]]]
 }

 # --------------------------------------------------------------
 # Auxillary function for searching of satisfaction sets.
 proc _lsatsub {e i} {
        set ii [expr $i + 1]
        match $e {
                {F} { return {}}
                {T} { return {{}}}
                {D $a $b} {
                        set al [_lsatsub $a $ii]
                        set bl [_lsatsub $b $ii]
                        set r {}
                        foreach l $bl {
                                lappend r [linsert $l 0 $ii]
                        }
                        set ii [expr -($ii)]
                        foreach l $al {
                                lappend r [linsert $l 0 $ii]
                        }
                        return $r
                }
                {R $a} {
                        # We ignore current input.
                        set r [_lsatsub $a $ii]
                }
        }
 }
 # Find satisfaction sets for CNF.
 proc lsatset {e} {
        return [_lsatsub $e 0]
 }

 # --------------------------------------------------------------
 # Tests:
 puts "x1 : [set x1 [lx 1]]"
 puts "x2 : [set x2 [lx 2]]"
 puts "x3 : [set x3 [lx 3]]"
 puts "ix1 : [set ix1 [lx -1]]"
 puts "ix2 : [set ix2 [lx -2]]"
 puts "ix3 : [set ix3 [lx -3]]"

 puts "a12 : [set a12 [land $x1 $x2]]"
 puts "a13 : [set a13 [land $x1 $x3]]"
 puts "ai12 : [set ai12 [land $ix1 $x2]]"
 puts "ai13 : [set ai13 [land $ix1 $x3]]"
 puts "ai1i2 : [set ai1i2 [land $ix1 $ix2]]"
 puts "ai1i3 : [set ai1i3 [land $ix1 $ix3]]"

 foreach v {a12 a13 ai12 ai13 ai1i2 ai1i3} {
        puts "Solution(s) for $v: [lsatset [set $v]]"
 }

 # --------------------------------------------------------------
 # Now you're ready to solve SAT problems of not very
 # big size.

Mac Cody: I added some code to the tests for clarity. I'm also trying to figure out how to relate the solutions to a more traditional Boolean or other logical representation (Karnaugh maps maybe?). For example, is there a more classical representation for the output of the test code above:

 x1 : D F T
 x2 : R {D F T}
 x3 : R {R {D F T}}
 ix1 : D T F
 ix2 : R {D T F}
 ix3 : R {R {D T F}}
 a12 : D F {D F T}
 a13 : D F {R {D F T}}
 ai12 : D {D F T} F
 ai13 : D {R {D F T}} F
 ai1i2 : D {D T F} F
 ai1i3 : D {R {D T F}} F
 Solution(s) for a12: {1 2}
 Solution(s) for a13: {1 3}
 Solution(s) for ai12: {-1 2}
 Solution(s) for ai13: {-1 3}
 Solution(s) for ai1i2: {-1 -2}
 Solution(s) for ai1i3: {-1 -3}

I'm just starting to get my mind around SAT. Here [L1 ] is pointer to a brief explanation to SAT and CNF which is helpful.