Saffron is a preprocessor which serves as a front end for Sat4j. Saffron is to Sat4j as a higher level language is to an assembler. The user expresses his/her problem by writing a Java application using the Saffron API. When the application is run, Saffron creates a corresponding SAT problem, then applies the Sat4j API to find a solution. The Sa…
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
Saffron 2.0
LICENSE.md
README.md

README.md

Saffron-2.0

Saffron is a preprocessor which serves as a front end for Sat4j. Saffron is to Sat4j as a higher level language is to an assembler. The user expresses his/her problem by writing a Java application using the Saffron API. When the application is run, Saffron creates a corresponding SAT problem, then applies the Sat4j API to find a solution. The Sat4j solution is analyzed by Saffron, and the bit assignments provided by Sat4j are used to construct the solution values of the original problem.

Getting Started

  1. Download Saffron source files.
  2. Download these (or later) versions of the following Sat4j libraries:
    • Windows
      • org.sat4j.core_2.3.5.v201308161310.jar
    • Mac
      • org.sat4j.core_2.3.0.v20110329.jar
      • org.sat4j.pb_2.3.0.v20110329.jar
  3. To familiarize yourself with the use of Saffron, run the numerous demo applications in the package named (of all things): demos. Extensive javadoc files can be found in the folder called: doc

A Typical Saffron Application

// Package specification
package positronic.satisfiability.demos.naturalnumber;

// Necessary imports
import java.util.List;
import positronic.satisfiability.elements.BooleanLiteral;
import positronic.satisfiability.elements.Conjunction;
import positronic.satisfiability.elements.IBooleanLiteral;
import positronic.satisfiability.elements.IProblem;
import positronic.satisfiability.elements.Problem;
import positronic.satisfiability.naturalnumber.INaturalNumber;
import positronic.satisfiability.naturalnumber.NaturalNumber;
import positronic.satisfiability.naturalnumber.NaturalNumberAdder;
import positronic.satisfiability.naturalnumber.NaturalNumberFixer;

// Class definition
public class NaturalNumberAdderDemo
{
	// Main method
	public static void main(String[] args) throws Exception
	{
		// Declare and allocate necessary variables.	
		INaturalNumber X = new NaturalNumber("X");
		INaturalNumber Y = new NaturalNumber("Y");
		INaturalNumber Z = new NaturalNumber("Z");
		INaturalNumber C = new NaturalNumber("C");

		// For each constraint of the problem to be solved, 
		// construct an instance of the Problem class:
		
		// Constrain X to equal 127
		IProblem nnfx = new NaturalNumberFixer(X, 127);
		// Constrain Y to equal 121
		IProblem nnfy = new NaturalNumberFixer(Y, 121);
		// Constrain Z to equal the sum of X and Y
		// and constrain C to be the integer formed by the carry bits
		IProblem nna = new NaturalNumberAdder(X, Y, Z, C);

		// Construct the IProblem that combines all of these constraints
		IProblem prob = new Conjunction(nnfx, nnfy, nna);
		
		// Call Sat4j via the findModel method to produce a List
		// of IBooleanLiterals that solve a SAT problem corresponding to prob
		List<IBooleanLiteral> solnlist = prob.findModel(Problem.defaultSolver());
		
		// Use the interpret method to load X, Y, Z and C with their solution values
		if (solnlist != null && solnlist.size() > 0)
		{
			BooleanLiteral.interpret(solnlist);
			System.out.println("X = " + X);
			System.out.println("Y = " + Y);
			System.out.println("Z = " + Z);
			System.out.println("C = " + C);
		} 
		else 
			System.out.println("No solution.");
	}
}

Running From The Windows Terminal

For instance, here's how the NaturalNumberAdderDemo app runs in my particular Java configuration:

cd C:\Users\Kerry\.AndroidStudio2.2\system\restart\jre\bin\

java.exe -classpath "C:\Users\Kerry\git\Saffron-2.0\Saffron 2.0\bin;C:\Users\Kerry\Development\eclipse\plugins\org.sat4j.core_2.3.5.v201308161310.jar" demos.NaturalNumberAdderDemo

Running From The Mac Terminal

For instance, here's how the NaturalNumberAdderDemo app runs in my particular Java configuration:

cd /Library/Java/JavaVirtualMachines/jdk1.8.0_144.jdk/Contents/Home/bin/

java -classpath "/Users/kerrysoileau/git/Saffron 2.0/Saffron 2.0/bin:/Applications/eclipse/plugins/org.sat4j.core_2.3.0.v20110329.jar:/Applications/eclipse/plugins/org.sat4j.pb_2.3.0.v20110329.jar" demos.NaturalNumberAdderDemo

Built With

Author

License

This project is licensed under the GPLv3 License - see the LICENSE.md file for details.

Acknowledgment

  • Daniel Le Berre provided invaluable guidance in connecting the Saffron code to the Sat4j API.