iSAT Library: An extended incremental SAT API

iSAT Library is an incremental SAT API, the extension of "IPASIR" in SAT-Race 2015.

This enables users to handle problems more briefly and use more conveniently in Java.

Documents of the methods in iSAT Library (Javadoc) are here.

• ISatSolver.html
• ISatLibrary.html

For using iSAT Library, GlueMiniSat 2.2.5 (or Glucose 4.0) and jna.jar are needed.

See README about the detailed usage.

(Latest version : 1.0.4)

• iSATLibrary-1.0.4.zip
  • supports glueminisat-2.2.8
  • add iSugar-1.1.0
    • added some optimization strategies
    • supports MaxCSP
  • some bug fix
• iSATLibrary-1.0.3.zip
  • add iSugar-1.0.0
  • some bug fix
• iSATLibrary-1.0.2.zip
  • add source for Glucose-4.0
  • reduce the number of generated library files (from two to one)
  • some bug fix
• iSATLibrary-1.0.1.zip
• iSATLibrary-1.0.0.zip

The package includes some example programs using iSAT Library.

• Graph Coloring
  

  /* GCP.java */
  import iSATLibrary.ISatSolver;
  import iSATLibrary.SatSolverForNative;
  
  public class GCP {
  
      int nodes = 4;
      int colors = 3; 
      int[][] edges = {{1,2}, {1,3}, {2,3}, {2,4}, {3,4}};
  
      public int v(int i, int j){ return (i-1) * colors + j; }
  
      public void encode(ISatSolver solver){
          for (int i=1; i<=nodes; i++){
             int[] cl = new int[colors];
             for (int j=1; j<=colors; j++)
                cl[j-1] = v(i,j);
             solver.addClause(cl);
          }        
          for (int[] edge: edges) {
             for (int j=1; j<=colors; j++)
                solver.addClause(new int[] {-v(edge[0],j), -v(edge[1],j)});
          }
      }
  
      public boolean solve(ISatSolver solver){
          return solver.solve()==10;
      }
  
      public void decode(ISatSolver solver){
          System.out.println("SATISFIABLE");
          int[] model = solver.getIntModel();
          for (int i=1; i<=nodes; i++) {
              for (int j=1; j<=colors; j++)
                  if (model[v(i,j)-1] > 0) System.out.println("Node " + i + "'s color : " + j);
          }
      }
  
      public static void main(String[] args) {
        GCP gcp = new GCP();
        ISatSolver solver = new SatSolverForNative("glueminisat");
        solver.setVerbosity(0);
        gcp.encode(solver);
        if (gcp.solve(solver)) gcp.decode(solver); else System.out.println("UNSATISFIABLE");
      }
  
  }
  

  To solve GCP with any other graph, edit the values of nodes, colors and edges in this program.

  Run this program with the following command:

  $ javac -cp ../iSATLibrary-1.0.4.jar:../jna-4.3.0.jar GCP.java 
  $ java -cp .:../iSATLibrary-1.0.4.jar:../jna-4.3.0.jar GCP 
  

  Output example is below.

  SATISFIABLE
  Node 1's color : 1
  Node 2's color : 3
  Node 3's color : 2
  Node 4's color : 1