genconstr_cs.cs
/*版权2019,Gurobi Opt狗万app足彩imization, 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_cs{公共const int n = 4; public const int NLITERALS = 4; // same as n public const int NCLAUSES = 8; public const int NOBJ = 2; static void Main() { 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; // Create environment GRBEnv env = new GRBEnv("genconstr_cs.log"); // Create initial model GRBModel model = new GRBModel(env); model.ModelName = "genconstr_cs"; // 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, string.Format("X{0}", i)); NotLit[i] = model.AddVar(0.0, 1.0, 0.0, GRB.BINARY, string.Format("notX{0}", i)); } GRBVar[] Cla = new GRBVar[NCLAUSES]; for (i = 0; i < NCLAUSES; i++) { Cla[i] = model.AddVar(0.0, 1.0, 0.0, GRB.BINARY, string.Format("Clause{0}", i)); } GRBVar[] Obj = new GRBVar[NOBJ]; for (i = 0; i < NOBJ; i++) { Obj[i] = model.AddVar(0.0, 1.0, 1.0, GRB.BINARY, string.Format("Obj{0}", 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, string.Format("CNSTR_X{0}", 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, string.Format("CNSTR_Clause{0}", 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.ModelSense = GRB.MAXIMIZE; // Save problem model.Write("genconstr_cs.mps"); model.Write("genconstr_cs.lp"); // Optimize model.Optimize(); // Status checking status = model.Status; if (status == GRB.Status.INF_OR_UNBD || status == GRB.Status.INFEASIBLE || status == GRB.Status.UNBOUNDED ) { Console.WriteLine("The model cannot be solved " + "because it is infeasible or unbounded"); return; } if (status != GRB.Status.OPTIMAL) { Console.WriteLine("Optimization was stopped with status {0}", status); return; } // Print result double objval = model.ObjVal; if (objval > 1.9) Console.WriteLine("Logical expression is satisfiable"); else if (objval > 0.9) Console.WriteLine("At least four clauses can be satisfied"); else Console.WriteLine("Not even three clauses can be satisfied"); // Dispose of model and environment model.Dispose(); env.Dispose(); } catch (GRBException e) { Console.WriteLine("Error code: {0}. {1}", e.ErrorCode, e.Message); } } }
