This semester I have only two projects because it is my last semester at school (read my revaluation of study here). I am attending course called Functional and Logic Programming where we should learn this sort of programming languages. First project is written in Haskell and I chose to implement disjunctive normal form (DNF) to binary decision diagram (BDD) convertor. You can get the impression what this means from Formal Analysis and Verification lecture about BDDs on page 4 and further. As usual you can find the code at my github. It can print truth table of given formula, create ordered BDD and reduce it to ROBDD.

Check the results with example formula

```
$ ./formula-2-bdd -t tests/6.dnf
P Q R
0 0 0 0
0 0 1 1
0 1 0 1
0 1 1 1
1 0 0 1
1 0 1 1
1 1 0 0
1 1 1 0
$./formula-2-bdd -b tests/6.dnf
P->Q->R->0
P->Q->R=>1
P->Q=>R->1
P->Q=>R=>1
P=>Q->R->1
P=>Q->R=>1
P=>Q=>R->0
P=>Q=>R=>0
$ ./formula-2-bdd -r tests/6.dnf
P->Q->R->0
P->Q->R=>1
P->Q=>1
P=>Q->1
P=>Q=>0
```

Format of BDD is simple: “->” means low edge and “=>” means high edge, e.g. if you have P = 1, Q = 1 and R equals whatever result of function is 1.

#### Update:

I decided to extend my little program with Apply function as is defined in mentioned lecture at page 15. Now I can perform disjunction on two ROBDD:

```
$ ./formula-2-bdd "||" tests/v1.dnf tests/v2.dnf
a->b->0
a->b=>1
a=>b->1
a=>b=>0
./formula-2-bdd "&&" tests/v1.dnf tests/v2.dnf
0
```