If you don't know what a BDD is check out the great wikipedia page. Donald Knuth calls BDDs "one of the only really fundamental data structures that came out in the last twenty-five years". You can watch an excellent lecture by him about BDDs here.
You may either scroll through the examples or enter your own boolean formulas in the ENTER YOUR FORMULA box. Select build BDD (or build minimum BDD) to build the BDD. A .png graph is generated and displayed below and stats about the BDD and formula are displayed in the OUTPUT box. The language was created to be robust and intuitive, but for info see the examples or the language spec.
You may either specify a variable ordering using the "Var_Order" keyword or the variables will be ordered in an unspecified way. The main expression must be specified using the "Main_Exp" keyword.
The implementation of the BDD is based off of Anderson's notes here.
The implementation recently incorporated an optimized ite build described in the paper: Efficient Implementation of a BDD Package
The minimum BDD implementation is described in paper: Dynamic Variable Ordering for Ordered Binary Decision Diagrams
PyBool can handle parse DIMACS files, but also a more expressive in-house language.
A short summary of the language is as follows:
Variables : Can be named anything alpha numeric, except for keywords. Literal variables must
be declared in a Var_Order statement.
Var_Order : declares variables and order of variables (important for BDDs) used as such:
Var_Order : {variable name}
You can have multi Var_Order statements, just don't declare variables multiple times.
Variables storing sub-formulas should not be in Var_Order statements
Constants : Represents logical True or False in expressions
1 - True
0 - False
Sub-Formulas : Pretty much a place holder for boolean expressions, allows you to
create large formulas easily. Is not considered in the actual BDD unless specified
in the Main_Exp.
variable = Expression
variable now refers to expression and can be used later on.
Expressions : A boolean expression, defined recursively as:
Expression {operator Expression}
Where the base cases are Variables or constants as expressions
Operators : Boolean operators applied to expressions (all binary except negation):
They are listed in order of precedence, and => associates from right to left.
Main_Exp : The only expression considered by the BDD. simply
Main_Expr : Expression
Comments : denoted with #
Please view the examples on the main BDD page for better understanding.