BDD - Binary Decision Diagram. One of the packages to work with them is BuDDy [http://www.itu.dk/research/buddy/]. It can be used to compute logical formulaes, search for SAT problem solutions, etc. Nuri SAT Algorithms [http://www8.pair.com/mnajtiv/sat/sat.html] page contains a simple SAT generator for factorisation problem. Also it contains two solvers, both in Perl. 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 formulaes by their # truth tables, solving small SAT problems, optimizing formulaes, # 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 formulae 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... # Auxillary 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 auxillary 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 represenation 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 [http://fortnow.com/lance/complog/archive/2003_01_12_archive.html#90173925] is pointer to a brief explanation to SAT and CNF which is helpful. ---- !!!!!! %| [Category Mathematics] |% !!!!!!