AlgebraicDecisionDiagrams.jl

import Pkg; Pkg.add("http://github.com/denismaua/AlgebraicDecisionDiagrams.jl")

using AlgebraicDecisionDiagrams
# Use alias for convenience
const ADD = AlgebraicDecisionDiagrams 

# Boolean Decision Diagrams

## This creates a positive literal on variable 1
l1 = pliteral(1)
@show ¬l1 # obtains the negation of that literal
@show apply(~,l1) # alternatively, one can apply negation (~) to the function
@show l1 ∧ (¬l1) # contradiction
@show l1 ∨ (¬l1) # tautology

## The BDD in Fig. 7 in Bryant's paper [1]
l2, l3 = pliteral(2), pliteral(3)
@show ¬(l1 ∧ l3) ∨ (l2 ∧ l3)

# Algebraic Decision Diagrams

## Example from Fig. 1 in Bryant's paper, using 0/1 constants [1]
x1, x2, x3 = indicator(Int,1), indicator(Int,2), indicator(Int,3)
@show apply((¬x1)*x2, x1*x3, max)

## Example in Fig. 5 of Bryant's paper, using 0/1 constants [1]
@show ADD.reduce( # return canonical form
    Node(1, # variable index (integer)
        Node(2, # variable index
            zero(Int), # low child -> additivite identity for Int (0)
            indicator(Int,3)
        ), # high child -> indicator node on variable 3
        Node(2,
            indicator(Int,3), # low
            indicator(Int,3)  # high
        )
    )
)

## Example in Fig 1. in Bahar et al. 1997's paper [2]
x0 = indicator(Int,0)
x1 = indicator(Int,2)
y0 = indicator(Int,1)
y1 = indicator(Int,3)
@show graph = Terminal(2)*(¬x0)*(¬x1)*(¬y0)*y1 + Terminal(2)*(¬x0)*(¬x1)*y0*(¬y1) + Terminal(2)*(¬x0)*x1*(¬y0)*y1 + Terminal(2)*(¬x0)*x1*y0*(¬y1) + Terminal(4)*x0*(¬x1)*y0*y1 + Terminal(4)*x0*x1*(¬y0)*y1

## Diagram Traversal
# To collect all nonterminal nodes of the previous diagram
nt = filter(n -> isa(n,Node), collect(graph)) # node are traversed in depth-first order
# now obtain its set of variable indices (without repetition)
@show mapreduce(index,union,nt) # should contain 0,1,2,3

## Matrix examples in page 9
@show f = (¬x0)*(¬y0) + x0*y0
@show g = Terminal(4)*(¬x0) + Terminal(2)*x0
@show h = f + g
@info "Restriction"
@show restrict(h,0,false)
@show h | (1 => true)
@show (h | (index(x0) => true)) + (h | (index(x0) => false))
@show (h | (index(y0) => true)) + (h | (index(y0) => false))

# Parametrized ADDs: ADDs with Multilinear Expressions (MLE) constants

const MLE = MultilinearExpression # Alias

## Create some MLE examples
@show a = MLE(2.0,1,3) + MLE(2.0,3)
@show b = MLE(3.0,2) + MLE(1.0,2,4) + MLE(1.0,4)
@show c = a * b

## Now create PADDs
@show x1 = indicator(MLE,1) # equivalent to 
#@show x1 = Node(1, MLE(0.0), MLE(1.0))
@show x2 = indicator(MLE,2) # equivalent to
#@show x2 = Node(2, MLE(0.0), MLE(1.0))
@show x3 = x1 + x2
@show d1 = Node(1, 1 + MLE(-1.0,1), MLE(1,1))
@show m1 = x1 + d1
@show d2 = Node(2, 1 + MLE(-1.0,2), MLE(1,2))
@show m2 = x2 + d2
@show m3 = d1 * d2