Introduction

In this post, I will show you how to use the jdd Java library with Scala in Eclipse Neon 3 IDE a Java BDD library.

Requirements

Eclipse Neon 3, you can download it here
You also need to get JDD Jar file. So you can clone the git repository or directly download the jar file.

How to use it in Scala

In this part, I will show you how to use the JDD library in Scala to get all solutions of SAT formula or just one.
You have first to import the library :

import jdd.bdd.BDD

Initialization

You need to initialize a BDD object by specify the size of initial node table and cache. We will use the values 1000 for the both parameters :

val bdd: BDD = new BDD(1000,1000)

Create variables

After the BDD object is created, you can define some BDD variables like this :

val v1: Int = bdd.createVar()
val v2: Int = bdd.createVar()

Specify formula

Finally, you can specify the formula you want to solve, just by calling the BDD operations :

val and: Int = bdd.and(v1,v2);
val or: Int = bdd.or(v1,v2)
val not: Int = bdd.not(v1)

Get one solution of SAT formula

Now, if you want to get one solution from a formula, call the method oneSat from a BDD object with the reference of the formula and an array of size of the number of result of your formula, here it will be 2 :

val oneSolution: Array[Int] = bdd.oneSat(and, new Array(2))
oneSolution.map(f=>print(f))

// Result
11

Get all solutions of SAT formula

If you want to get all solution from a formula, call the method printSet from a BDD object :

bdd.printSet(or)

// Result
01
1-

You can notice the result is "simplified", in fact the result you was maybe expecting would be something like that (see below) but the BDD library simplified the result with a "-" when it's possible :

01
10
11

By the way, the method printSet doesn't return anything so if you want to get the result, you have to redirect the output stream, like this :

val baos = new ByteArrayOutputStream(); // Create a stream to hold the output
val ps = new PrintStream(baos); 
val old = System.out;            // Store the current output stream
System.setOut(ps);               // Redefine the output stream 
bdd.printSet(or)                 // Call the method with the print statement
System.out.flush();              // Flush the print statement into the PrintStream ps
System.setOut(old);              // Restore the previous state of the output stream

for (line <- baos.toString().split("\n")) // Get the result line by line
{
   println(line)
}

// Result
01
1-

Sources

Eclipse Neon, Scala IDE
JDD Bitbucket
Method to redirect the output stream

Also if you want to use different BDD library for different language like C, Python or an other language ; I recommend you to visit this web page which list some BDD libraries.