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