iSAT Library: An extended incremental SAT API

Table of Contents


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.


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)


The package includes some example programs using iSAT Library.

  • Graph Coloring
    /* */
    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);
            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){
            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");
          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 
    $ java -cp .:../iSATLibrary-1.0.4.jar:../jna-4.3.0.jar GCP 

    Output example is below.

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

Date: 2017-02-21T17:54+0900

Author: Tatsuya Sako

Org version 7.9.3f with Emacs version 24

Validate XHTML 1.0