# --------------------------------------------------------------
 # 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.