Genconstr.java
/*版权所有2023,Gurobi O狗万app足彩ptimization, LLC */ /*在这个例子中，我们展示了对一些常用表达式建模的通用约束的使用。我们使用sat问题作为一个例子,我们希望看到如果可以满足至少四(或者全部)条款的逻辑L = (x0或~ x1和x2)和(x1 ~ x2或x3)和(x2 ~ x3或x0)和(x3 ~ x0或x1)和(~ x0或~ x1和x2)和(~ ~ x1和x2或x3)和(x2 ~ ~ x3或x0)和(~ x3 ~ x0或x1)我们通过引入两个变量为每个文字(本身和它的否定价值),一个变量对于每一个条款,然后两个变量指示如果我们能满足四个,另一个是确定子句的最小值(所以如果是一个，我们可以满足所有的子句)，并把这两个变量放在目标中。即目标函数将最大化Obj0 + Obj1 Obj0 = MIN(Clause1，…，从句1 = 1 ->从句1 +…+ Clause8 >= 4因此，当且仅当满足所有子句时，客观值为2;当且仅当至少四个条款可以满足时为1，否则为0。*/进口gurobi.*;公共类Genconstr{公共静态最终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()); } } }
