/* Copyright 2024, 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 for
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), a variable for each clause, and then two
variables for indicating if we can satisfy four, and another to identify
the minimum of the clauses (so if it one, we can satisfy all clauses)
and put these two variables in the objective.
i.e. the Objective function will be
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 clauses can be satisfied, and
zero otherwise.
*/
import 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());
}
}
}