This is a SAT solver that takes in input constraints expressed using the language in formula.ml and reduces them to a Reduced Ordered Binary Decision Diagram (ROBDD). It then uses the generated ROBDD to identify satsifying assignments and can also output the ROBDD as a graph in GraphViz dot (.dot) format.
For an example graph, see nqueens4.png for an image of the ROBDD for the 4-Queens problem generated from nqueens4.dot. There is also a similar example graph for the 5-Queens problem - nqueens5.png, nqueens5.dot. The graph contains variables of the form cij where i and j are numbers and this variable represents the existence of a queen on row i and column j of the board. A satisfying assignment to these variables is given by any path that leads from the root of the ROBDD to the value 1 at the bottom of the ROBDD and the assignment itself for a variable is given by whether the edge taken from that variable in the chosen path is 1 (true) or 0 (false).
formula.ml: Basic structure of formulas accepted by solver.bdd.mli: Interface of bdd solver module.bdd.ml: Implementation of bdd solver module.A2.ml: The functions in this file uses the BDD module to solve the n_queens problem.
You can compile the whole project as
ocamlc formula.ml bdd.mli bdd.ml A2.ml
To run the package on an n-queen problem:
- Append
let ro = n_queen <N>;;to the end of A2.ml, where<N>is replaced with the board-size for which you need a satisfying solution - Compile using the above command
- Execute the
a.outfile generated
The package would generate a bdd.dot file encoding the ROBDD for the corresponding N-Queens problem.