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
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.
Recommended Posts