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 😛

If you liked this article, you might be interested in my Twitter feed as well.
 
 

Related Posts

  • November 5, 2011 Simulated Annealing Project (1)
    For a school project, I have to implement Simulated Annealing meta heuristic. Thanks to many open source web tools, I've been able to quickly do the project and have a pretty display. CoffeeScript, Raphael, Highcharts, Three.js, Twitter Bootstrap, jQuery and Web […]
  • November 10, 2011 Diablofans Theme Improvement (1)
    Diablofans.com needed a bit of love. It is really gratifying to be able to visually improve a website by an order of magnitude just by changing some colors and fixing broken layout :) Here are some of the changes I made: Post Poll Blizzquote
  • August 27, 2011 Start a technical blog, it’s worth it! (6)
    Lately, I've been advocating to all my student friends to start a blog. Here's an article with the most common questions answered :) What are the benefits? Being known as an expert. The majority of my blog posts are about advanced Javascript topics. As a result, I'm being tagged as […]
  • September 11, 2011 World of Warcraft HTML Tooltip Diff (1)
    MMO-Champion is a World of Warcraft news website. When a new patch is released, we want to show what has changed in the game (Post Example). An english summary of each spell change is hand written, but we want to show the exact tooltip changes. jsHTMLDiff is available on […]
  • January 11, 2012 Javascript Ray Tracer (2)
    Here is a report of the Ray Tracer written by myself Christopher Chedeau. I've taken the file format and most of the examples from the Ray Tracer of our friends Maxime Mouial and Clément Bœsch. The source is available on Github. It is powered by Open Source technologies: glMatrix, […]