During the course "Introduction to Model Checking" by Alexandre Duret-Lutz we've been assigned to create a Binary Decision Diagram library. Contrary to most people, I've been writing mine in Javascript instead of C++. Overall it is running slower but by an acceptable factor (around x5).
Display
I've written a BDD display using the graph library called Dracula which is built on-top of RaphaëlJS. The API of the lib is really neat but there are only 2 available node layout algorithms and none of them really fit my needs. I'd love to have the ones available in GraphViz.
In order to enter a formula, I've written a small parser that accepts most common binary operations. The little dice gives you some random formula. Also, on the left, you have all the evaluations that satisfy your formula.
Use Case
Binary Decision Diagram are used in Boolean Satisfiability Problem and Model Checking. As a benchmark example, we use the BDD to solve the 8-Queens problem.
A version using web-workers is available. However, using more than one worker will be slower as the cost of communication (through JSON serialization) is really high (hundreds of thousands nodes). You can also try to use a random ordering for the variables, but beware, the execution time varies a lot (up to x100 for the fastest/slowest)!
Conclusion
It was a really fun project to do. You can view the sources and probably use them as a base if you ever need to use a BDD in your life 😛