genconstr.py
#!/usr/bin/env python3.7 # Copyright 2021, 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 is 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 gurobipy as gp from gurobipy import GRB import sys try: NLITERALS = 4 n = NLITERALS # Example data: # e.g. {0, n+1, 2} means clause (x0 or ~x1 or x2) Clauses = [[ 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]] # Create a new model model = gp.Model("Genconstr") # initialize decision variables and objective Lit = model.addVars(NLITERALS, vtype=GRB.BINARY, name="X") NotLit = model.addVars(NLITERALS, vtype=GRB.BINARY, name="NotX") Cla = model.addVars(len(Clauses), vtype=GRB.BINARY, name="Clause") Obj0 = model.addVar(vtype=GRB.BINARY, name="Obj0") Obj1 = model.addVar(vtype=GRB.BINARY, name="Obj1") # Link Xi and notXi model.addConstrs((Lit[i] + NotLit[i] == 1.0 for i in range(NLITERALS)), name="CNSTR_X") # Link clauses and literals for i, c in enumerate(Clauses): clause = [] for l in c: if l >= n: clause.append(NotLit[l-n]) else: clause.append(Lit[l]) model.addConstr(Cla[i] == gp.or_(clause), "CNSTR_Clause" + str(i)) # Link objs with clauses model.addConstr(Obj0 == gp.min_(Cla), name="CNSTR_Obj0") model.addConstr((Obj1 == 1) >> (Cla.sum() >= 4.0), name="CNSTR_Obj1") # Set optimization objective model.setObjective(Obj0 + Obj1, GRB.MAXIMIZE) # Save problem model.write("genconstr.mps") model.write("genconstr.lp") # Optimize model.optimize() # Status checking status = model.getAttr(GRB.Attr.Status) if status in (GRB.INF_OR_UNBD, GRB.INFEASIBLE, GRB.UNBOUNDED): print("The model cannot be solved because it is infeasible or " "unbounded") sys.exit(1) if status != GRB.OPTIMAL: print("Optimization was stopped with status ", status) sys.exit(1) # Print result objval = model.getAttr(GRB.Attr.ObjVal) if objval > 1.9: print("Logical expression is satisfiable") elif objval > 0.9: print("At least four clauses can be satisfied") else: print("Not even three clauses can be satisfied") except gp.GurobiError as e: print('Error code ' + str(e.errno) + ": " + str(e)) except AttributeError: print('Encountered an attribute error')
