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

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.

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.

- Input a boolean expression from the user and parse it.
- Create ROBDDs from parsed expressions.
- Apply boolean operators to ROBDDs.

Legality

For simplicity you can

assumeall 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)"

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.

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

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.

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

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.

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.