Hide navigation sidebar
Hide table of contents sidebar
Back to top
Toggle table of contents sidebar

# Genconstr.java

    /* Copyright 2025, Gurobi Optimization, LLC */

    /* In this example we show the use of general constraints for modeling
       some common expressions. We use as an example a SAT-problem where we
       want to see if it is possible to satisfy at least four (or all) clauses
       of the logical form

       L = (x0 or ~x1 or x2)  and (x1 or ~x2 or x3)  and
           (x2 or ~x3 or x0)  and (x3 or ~x0 or x1)  and
           (~x0 or ~x1 or x2) and (~x1 or ~x2 or x3) and
           (~x2 or ~x3 or x0) and (~x3 or ~x0 or x1)

       We do this by introducing two variables for each literal (itself and its
       negated value), one variable for each clause, one variable indicating
       whether we can satisfy at least four clauses, and one last variable to
       identify the minimum of the clauses (so if it is one, we can satisfy all
       clauses). Then we put these last two variables in the objective.
       The objective function is therefore

       maximize Obj0 + Obj1

        Obj0 = MIN(Clause1, ... , Clause8)
        Obj1 = 1 -> Clause1 + ... + Clause8 >= 4

       thus, the objective value will be two if and only if we can satisfy all
       clauses; one if and only if at least four but not all clauses can be satisfied,
       and zero otherwise.
     */

    import com.gurobi.gurobi.*;

    public class Genconstr {

      public static final int n = 4;
      public static final int NLITERALS = 4;  // same as n
      public static final int NCLAUSES = 8;
      public static final int NOBJ = 2;

      public static void main(String[] args) {

        try {
          // Example data:
          //   e.g. {0, n+1, 2} means clause (x0 or ~x1 or x2)
          int Clauses[][] = new int[][]
                            {{  0, n+1, 2}, {  1, n+2, 3},
                             {  2, n+3, 0}, {  3, n+0, 1},
                             {n+0, n+1, 2}, {n+1, n+2, 3},
                             {n+2, n+3, 0}, {n+3, n+0, 1}};

          int i, status, nSolutions;

          // Create environment
          GRBEnv env = new GRBEnv("Genconstr.log");

          // Create initial model
          GRBModel model = new GRBModel(env);
          model.set(GRB.StringAttr.ModelName, "Genconstr");

          // Initialize decision variables and objective

          GRBVar[] Lit     = new GRBVar[NLITERALS];
          GRBVar[] NotLit  = new GRBVar[NLITERALS];
          for (i = 0; i < NLITERALS; i++) {
            Lit[i]    = model.addVar(0.0, 1.0, 0.0, GRB.BINARY, "X" + String.valueOf(i));
            NotLit[i] = model.addVar(0.0, 1.0, 0.0, GRB.BINARY, "notX" + String.valueOf(i));
          }

          GRBVar[] Cla = new GRBVar[NCLAUSES];
          for (i = 0; i < NCLAUSES; i++) {
            Cla[i] = model.addVar(0.0, 1.0, 0.0, GRB.BINARY, "Clause" + String.valueOf(i));
          }

          GRBVar[] Obj = new GRBVar[NOBJ];
          for (i = 0; i < NOBJ; i++) {
            Obj[i] = model.addVar(0.0, 1.0, 1.0, GRB.BINARY, "Obj" + String.valueOf(i));
          }

          // Link Xi and notXi
          GRBLinExpr lhs;
          for (i = 0; i < NLITERALS; i++) {
            lhs = new GRBLinExpr();
            lhs.addTerm(1.0, Lit[i]);
            lhs.addTerm(1.0, NotLit[i]);
            model.addConstr(lhs, GRB.EQUAL, 1.0, "CNSTR_X" + String.valueOf(i));
          }

          // Link clauses and literals
          for (i = 0; i < NCLAUSES; i++) {
            GRBVar[] clause = new GRBVar[3];
            for (int j = 0; j < 3; j++) {
              if (Clauses[i][j] >= n) clause[j] = NotLit[Clauses[i][j]-n];
              else                    clause[j] = Lit[Clauses[i][j]];
            }
            model.addGenConstrOr(Cla[i], clause, "CNSTR_Clause" + String.valueOf(i));
          }

          // Link objs with clauses
          model.addGenConstrMin(Obj[0], Cla, GRB.INFINITY, "CNSTR_Obj0");
          lhs = new GRBLinExpr();
          for (i = 0; i < NCLAUSES; i++) {
            lhs.addTerm(1.0, Cla[i]);
          }
          model.addGenConstrIndicator(Obj[1], 1, lhs, GRB.GREATER_EQUAL, 4.0, "CNSTR_Obj1");

          // Set global objective sense
          model.set(GRB.IntAttr.ModelSense, GRB.MAXIMIZE);

          // Save problem
          model.write("Genconstr.mps");
          model.write("Genconstr.lp");

          // Optimize
          model.optimize();

          // Status checking
          status = model.get(GRB.IntAttr.Status);

          if (status == GRB.INF_OR_UNBD ||
              status == GRB.INFEASIBLE  ||
              status == GRB.UNBOUNDED     ) {
            System.out.println("The model cannot be solved " +
                   "because it is infeasible or unbounded");
            System.exit(1);
          }
          if (status != GRB.OPTIMAL) {
            System.out.println("Optimization was stopped with status " + status);
            System.exit(1);
          }

          // Print result
          double objval = model.get(GRB.DoubleAttr.ObjVal);

          if (objval > 1.9)
            System.out.println("Logical expression is satisfiable");
          else if (objval > 0.9)
            System.out.println("At least four clauses can be satisfied");
          else
            System.out.println("Not even three clauses can be satisfied");

          // Dispose of model and environment
          model.dispose();
          env.dispose();

        } catch (GRBException e) {
          System.out.println("Error code: " + e.getErrorCode() + ". " +
              e.getMessage());
        }
      }
    }

Help and Feedback

Press `/` or click to search this documentation | Gurobi website | Gurobi community forum
Go to other Gurobi documentation | Gurobi download | Contact support