Equivalence.java

A simple example that demonstrates the canonicity property of BDDs.

Queens.java

The N-queen problem with BDDs (pretty much equivalent to the code in BuDDy).

If you are into optimisations, be sure to read the little notice in the code

Queens2.java

Another, "more efficient", implementation of the N-queen problem where you get one constraint for free. It turns out that you get less variables but an uglier BDD, and as a direct consequence, this one performs worse than Queens.java :(

This is a great opportunity to test your BDD optimisation skills (hint: operation scheduling + restrict operator).

IQueens.java

Interactive version of the N-queen problem. Inspired by the example from Config-It web page (check the on-line demos).

Note: you will also need to download Queens2.java for this example

Knight.java

A variant of the Knights tours problem (not the original 400-year old Knights Tour that was solved by Löbbing and Wegener in 1996). This example illustrates a sequential problem while the previous problems were all purely logical.

DIMACS solver

A very simple (~130 lines, in your face MiniSAT :) implementation of a SAT-solver that reads CNF Formulas in DIMACS file format. This is also a very good example of when not to use BDDs!