ROBDDs

1. Assignment Goals

  1. Read BDD introduction text (PostScript document, sections 1,...,5).
  2. Get a hands-on "feel" how to use ROBDDs.
  3. Implement a Java package named robdd.

2. Using ROBDDs

A visualization tool like JADE will help you to get the "feel" of ROBDDs. It can also help you debug your code. Try playing with some functions and variable ordering. For example, the function (x1 xor x2) and (x3 xor x4)will give a nice ROBDD for one ordering and a bad for another.

3. Interactive Java Shell

We need an interpreter to experiment with. We'll be using BeanShell, which is a ready-made scripting shell for Java. It speeds up debugging and eases experimentation. Follow its Quick Start to get started. You don't need all the features! Find the commands you need in Commands Overview and skip the rest. Here is an example to start with. You can use my Interpreter code.

4. Package Requirements

5. Detailed Requirements

5.1 Input

Legality

For simplicity you can assume all input are legal.

Variable Naming:

We use variable names x1, x2, x3,... When used in context of variable, the integer index '2' denotes x2.

Constants:

0, 1

Variables:

x1, x2, ...

Operators:

Name and arguments Meaning (see text for details)
not(expr) negation
and(lexpr, rexpr) conjunction
or(lexpr, rexpr) disjunction
->(lexpr, rexpr) implication
<->(lexpr, rexpr) bi-implication

Valid Input Examples:

"and( ->( not( x1 ), <->( 1 , x2 ) ), not( x2 ) )"

" or ( or( x1, x2), 1) "

"or(or(x1,x2),1)"

5.2 Parsing

The input are given as strings. We use a parenthesized prefixed notation to simplify the parsing. White spaces shouldn't effect the expression (the last two valid examples are equal). Your parser should implement the Parser interface, and should output a boolean expression that extends the BooleanExpression abstract class.

5.3 ROBDD Operations

The ROBDD is encapsulated as a Java class. The class should implement all the methods in Robdd interface. Here is a brief summary:

Method Use
<constructor> construct an ROBDD using a boolean expression
anySat find a satisfying assignment
apply apply a boolean operator on two ROBDDs
applyExistQuantifier apply an existential quantification to an ROBDD
nodeCount count the nodes in the ROBDD
restrict restricted an ROBDD to a given truth assignment
satCount count the number of satisfying assignments
toString return an INF string representation of the ROBDD

5.4 Modularization

Before you begin, understand the modularization of the code. It was designed to allow easy component replacement. It can help when checking your assignment - if a certain component doesn't work properly, we can replace it and still check the others.

5.5 Documentation

The assignment should have internal documentation within the code, and an external readme file in either plain text or HTML format.

6. Running Experiments

When your package is ready consider the following expressions:

expr1 =

or(or(or( and(and( not(x1), not(x2)), x3), and( not(x1), and(x2, x3))), and(x1, and(not(x2), not(x3)))), or( or(and (and(x1, not(x2)), x3), -> (<-> (0, x4), x3)), or(and(x1, and(x2, not(x3))), and( and(x1, x2), x3))))

expr2 =

or(or(or( and(and( not(x3), not(x2)), x1), and( not(x2), and(x3, x1))), and(x3, and(not(x2), not(x2)))), or( or(and (and(x3, not(x2)), x1), -> (<-> (0, x4), x2)), or(and(x2, and(x1, not(x3))), and( and(x3, x1), x2))))

expr3 =

or(x1, or(x3, x4))

Which of the expressions are equivalent?
Use your package to prove their equivalence or to find a counter example.

7. Submission

Please submit your assignment using the submission system. Make sure to include run examples in your .bsh script.

Detailed submission instructions and further info about this exercise were given in Tirgul 6.