/* 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. */#include<stdlib.h>#include<stdio.h>#include<math.h>#include<string.h>#include"gurobi_c.h"#define MAXSTR    128#define NLITERALS 4#define NCLAUSES  8#define NOBJ      2#define NVARS     (2 * NLITERALS + NCLAUSES + NOBJ)#define LIT(n)    (n)#define NOTLIT(n) (NLITERALS + n)#define CLA(n)    (2 * NLITERALS + n)#define OBJ(n)    (2 * NLITERALS + NCLAUSES + n)intmain(void){GRBenv*env=NULL;GRBmodel*model=NULL;interror=0;intcind[NVARS];doublecval[NVARS];charbuffer[MAXSTR];intcol,i,status;doubleobjval;/* Example data */constintClauses[][3]={{LIT(0),NOTLIT(1),LIT(2)},{LIT(1),NOTLIT(2),LIT(3)},{LIT(2),NOTLIT(3),LIT(0)},{LIT(3),NOTLIT(0),LIT(1)},{NOTLIT(0),NOTLIT(1),LIT(2)},{NOTLIT(1),NOTLIT(2),LIT(3)},{NOTLIT(2),NOTLIT(3),LIT(0)},{NOTLIT(3),NOTLIT(0),LIT(1)}};/* Create environment */error=GRBloadenv(&env,"genconstr_c.log");if(error)gotoQUIT;/* Create initial model */error=GRBnewmodel(env,&model,"genconstr_c",NVARS,NULL,NULL,NULL,NULL,NULL);if(error)gotoQUIT;/* Initialize decision variables and objective */for(i=0;i<NLITERALS;i++){col=LIT(i);sprintf(buffer,"X%d",i);error=GRBsetcharattrelement(model,"VType",col,GRB_BINARY);if(error)gotoQUIT;error=GRBsetstrattrelement(model,"VarName",col,buffer);if(error)gotoQUIT;col=NOTLIT(i);sprintf(buffer,"notX%d",i);error=GRBsetcharattrelement(model,"VType",col,GRB_BINARY);if(error)gotoQUIT;error=GRBsetstrattrelement(model,"VarName",col,buffer);if(error)gotoQUIT;}for(i=0;i<NCLAUSES;i++){col=CLA(i);sprintf(buffer,"Clause%d",i);error=GRBsetcharattrelement(model,"VType",col,GRB_BINARY);if(error)gotoQUIT;error=GRBsetstrattrelement(model,"VarName",col,buffer);if(error)gotoQUIT;}for(i=0;i<NOBJ;i++){col=OBJ(i);sprintf(buffer,"Obj%d",i);error=GRBsetcharattrelement(model,"VType",col,GRB_BINARY);if(error)gotoQUIT;error=GRBsetstrattrelement(model,"VarName",col,buffer);if(error)gotoQUIT;error=GRBsetdblattrelement(model,"Obj",col,1.0);if(error)gotoQUIT;}/* Link Xi and notXi */for(i=0;i<NLITERALS;i++){sprintf(buffer,"CNSTR_X%d",i);cind[0]=LIT(i);cind[1]=NOTLIT(i);cval[0]=cval[1]=1;error=GRBaddconstr(model,2,cind,cval,GRB_EQUAL,1.0,buffer);if(error)gotoQUIT;}/* Link clauses and literals */for(i=0;i<NCLAUSES;i++){sprintf(buffer,"CNSTR_Clause%d",i);error=GRBaddgenconstrOr(model,buffer,CLA(i),3,Clauses[i]);if(error)gotoQUIT;}/* Link objs with clauses */for(i=0;i<NCLAUSES;i++){cind[i]=CLA(i);cval[i]=1;}error=GRBaddgenconstrMin(model,"CNSTR_Obj0",OBJ(0),NCLAUSES,cind,GRB_INFINITY);if(error)gotoQUIT;/* note that passing 4 instead of 4.0 will produce undefined behavior */error=GRBaddgenconstrIndicator(model,"CNSTR_Obj1",OBJ(1),1,NCLAUSES,cind,cval,GRB_GREATER_EQUAL,4.0);if(error)gotoQUIT;/* Set global objective sense */error=GRBsetintattr(model,GRB_INT_ATTR_MODELSENSE,GRB_MAXIMIZE);if(error)gotoQUIT;/* Save problem */error=GRBwrite(model,"genconstr_c.mps");if(error)gotoQUIT;error=GRBwrite(model,"genconstr_c.lp");if(error)gotoQUIT;/* Optimize */error=GRBoptimize(model);if(error)gotoQUIT;/* Status checking */error=GRBgetintattr(model,"Status",&status);if(error)gotoQUIT;if(status==GRB_INF_OR_UNBD||status==GRB_INFEASIBLE||status==GRB_UNBOUNDED){printf("The model cannot be solved ""because it is infeasible or unbounded\n");gotoQUIT;}if(status!=GRB_OPTIMAL){printf("Optimization was stopped with status %i\n",status);gotoQUIT;}/* Print result */error=GRBgetdblattr(model,GRB_DBL_ATTR_OBJVAL,&objval);if(error)gotoQUIT;if(objval>1.9)printf("Logical expression is satisfiable\n");elseif(objval>0.9)printf("At least four clauses can be satisfied\n");elseprintf("At most three clauses may be satisfied\n");QUIT:if(model!=NULL)GRBfreemodel(model);if(env!=NULL)GRBfreeenv(env);returnerror;}

/* 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. */#include"gurobi_c++.h"#include<sstream>#include<iomanip>usingnamespacestd;#define n         4#define NLITERALS 4// same as n#define NCLAUSES  8#define NOBJ      2intmain(void){GRBEnv*env=0;try{// Example data//   e.g. {0, n+1, 2} means clause (x0 or ~x1 or x2)constintClauses[][3]={{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}};inti,status;// Create environmentenv=newGRBEnv("genconstr_c++.log");// Create initial modelGRBModelmodel=GRBModel(*env);model.set(GRB_StringAttr_ModelName,"genconstr_c++");// Initialize decision variables and objectiveGRBVarLit[NLITERALS];GRBVarNotLit[NLITERALS];for(i=0;i<NLITERALS;i++){ostringstreamvname;vname<<"X"<<i;Lit[i]=model.addVar(0.0,1.0,0.0,GRB_BINARY,vname.str());vname.str("");vname<<"notX"<<i;NotLit[i]=model.addVar(0.0,1.0,0.0,GRB_BINARY,vname.str());}GRBVarCla[NCLAUSES];for(i=0;i<NCLAUSES;i++){ostringstreamvname;vname<<"Clause"<<i;Cla[i]=model.addVar(0.0,1.0,0.0,GRB_BINARY,vname.str());}GRBVarObj[NOBJ];for(i=0;i<NOBJ;i++){ostringstreamvname;vname<<"Obj"<<i;Obj[i]=model.addVar(0.0,1.0,1.0,GRB_BINARY,vname.str());}// Link Xi and notXiGRBLinExprlhs;for(i=0;i<NLITERALS;i++){ostringstreamcname;cname<<"CNSTR_X"<<i;lhs=0;lhs+=Lit[i];lhs+=NotLit[i];model.addConstr(lhs==1.0,cname.str());}// Link clauses and literalsGRBVarclause[3];for(i=0;i<NCLAUSES;i++){for(intj=0;j<3;j++){if(Clauses[i][j]>=n)clause[j]=NotLit[Clauses[i][j]-n];elseclause[j]=Lit[Clauses[i][j]];}ostringstreamcname;cname<<"CNSTR_Clause"<<i;model.addGenConstrOr(Cla[i],clause,3,cname.str());}// Link objs with clausesmodel.addGenConstrMin(Obj[0],Cla,NCLAUSES,GRB_INFINITY,"CNSTR_Obj0");lhs=0;for(i=0;i<NCLAUSES;i++){lhs+=Cla[i];}model.addGenConstrIndicator(Obj[1],1,lhs>=4.0,"CNSTR_Obj1");// Set global objective sensemodel.set(GRB_IntAttr_ModelSense,GRB_MAXIMIZE);// Save problemmodel.write("genconstr_c++.mps");model.write("genconstr_c++.lp");// Optimizemodel.optimize();// Status checkingstatus=model.get(GRB_IntAttr_Status);if(status==GRB_INF_OR_UNBD||status==GRB_INFEASIBLE||status==GRB_UNBOUNDED){cout<<"The model cannot be solved "<<"because it is infeasible or unbounded"<<endl;return1;}if(status!=GRB_OPTIMAL){cout<<"Optimization was stopped with status "<<status<<endl;return1;}// Print resultdoubleobjval=model.get(GRB_DoubleAttr_ObjVal);if(objval>1.9)cout<<"Logical expression is satisfiable"<<endl;elseif(objval>0.9)cout<<"At least four clauses can be satisfied"<<endl;elsecout<<"Not even three clauses can be satisfied"<<endl;}catch(GRBExceptione){cout<<"Error code = "<<e.getErrorCode()<<endl;cout<<e.getMessage()<<endl;}catch(...){cout<<"Exception during optimization"<<endl;}// Free environmentdeleteenv;return0;}

/* 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. */usingSystem;usingGurobi;classgenconstr_cs{publicconstintn=4;publicconstintNLITERALS=4;// same as npublicconstintNCLAUSES=8;publicconstintNOBJ=2;staticvoidMain(){try{// Example data://   e.g. {0, n+1, 2} means clause (x0 or ~x1 or x2)int[,]Clauses=newint[,]{{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}};inti,status;// Create environmentGRBEnvenv=newGRBEnv("genconstr_cs.log");// Create initial modelGRBModelmodel=newGRBModel(env);model.ModelName="genconstr_cs";// Initialize decision variables and objectiveGRBVar[]Lit=newGRBVar[NLITERALS];GRBVar[]NotLit=newGRBVar[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=newGRBVar[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=newGRBVar[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 notXiGRBLinExprlhs;for(i=0;i<NLITERALS;i++){lhs=newGRBLinExpr();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 literalsfor(i=0;i<NCLAUSES;i++){GRBVar[]clause=newGRBVar[3];for(intj=0;j<3;j++){if(Clauses[i,j]>=n)clause[j]=NotLit[Clauses[i,j]-n];elseclause[j]=Lit[Clauses[i,j]];}model.AddGenConstrOr(Cla[i],clause,string.Format("CNSTR_Clause{0}",i));}// Link objs with clausesmodel.AddGenConstrMin(Obj[0],Cla,GRB.INFINITY,"CNSTR_Obj0");lhs=newGRBLinExpr();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 sensemodel.ModelSense=GRB.MAXIMIZE;// Save problemmodel.Write("genconstr_cs.mps");model.Write("genconstr_cs.lp");// Optimizemodel.Optimize();// Status checkingstatus=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 resultdoubleobjval=model.ObjVal;if(objval>1.9)Console.WriteLine("Logical expression is satisfiable");elseif(objval>0.9)Console.WriteLine("At least four clauses can be satisfied");elseConsole.WriteLine("Not even three clauses can be satisfied");// Dispose of model and environmentmodel.Dispose();env.Dispose();}catch(GRBExceptione){Console.WriteLine("Error code: {0}. {1}",e.ErrorCode,e.Message);}}}

/* 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. */importcom.gurobi.gurobi.*;publicclassGenconstr{publicstaticfinalintn=4;publicstaticfinalintNLITERALS=4;// same as npublicstaticfinalintNCLAUSES=8;publicstaticfinalintNOBJ=2;publicstaticvoidmain(String[]args){try{// Example data://   e.g. {0, n+1, 2} means clause (x0 or ~x1 or x2)intClauses[][]=newint[][]{{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}};inti,status,nSolutions;// Create environmentGRBEnvenv=newGRBEnv("Genconstr.log");// Create initial modelGRBModelmodel=newGRBModel(env);model.set(GRB.StringAttr.ModelName,"Genconstr");// Initialize decision variables and objectiveGRBVar[]Lit=newGRBVar[NLITERALS];GRBVar[]NotLit=newGRBVar[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=newGRBVar[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=newGRBVar[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 notXiGRBLinExprlhs;for(i=0;i<NLITERALS;i++){lhs=newGRBLinExpr();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 literalsfor(i=0;i<NCLAUSES;i++){GRBVar[]clause=newGRBVar[3];for(intj=0;j<3;j++){if(Clauses[i][j]>=n)clause[j]=NotLit[Clauses[i][j]-n];elseclause[j]=Lit[Clauses[i][j]];}model.addGenConstrOr(Cla[i],clause,"CNSTR_Clause"+String.valueOf(i));}// Link objs with clausesmodel.addGenConstrMin(Obj[0],Cla,GRB.INFINITY,"CNSTR_Obj0");lhs=newGRBLinExpr();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 sensemodel.set(GRB.IntAttr.ModelSense,GRB.MAXIMIZE);// Save problemmodel.write("Genconstr.mps");model.write("Genconstr.lp");// Optimizemodel.optimize();// Status checkingstatus=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 resultdoubleobjval=model.get(GRB.DoubleAttr.ObjVal);if(objval>1.9)System.out.println("Logical expression is satisfiable");elseif(objval>0.9)System.out.println("At least four clauses can be satisfied");elseSystem.out.println("Not even three clauses can be satisfied");// Dispose of model and environmentmodel.dispose();env.dispose();}catch(GRBExceptione){System.out.println("Error code: "+e.getErrorCode()+". "+e.getMessage());}}}

functiongenconstr()% 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 = (x1 or ~x2 or x3)  and (x2 or ~x3 or x4)  and%     (x3 or ~x4 or x1)  and (x4 or ~x1 or x2)  and%     (~x1 or ~x2 or x3) and (~x2 or ~x3 or x4) and%     (~x3 or ~x4 or x1) and (~x4 or ~x1 or x2)%% 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 Obj1 + Obj2%%  Obj1 = MIN(Clause2, ... , Clause8)%  Obj2 = 2 -> Clause2 + ... + 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.%% define primitive datan=4;nLiterals=4;nClauses=8;nObj=2;nVars=2*nLiterals+nClauses+nObj;Clauses=[1,n+2,3;2,n+3,4;3,n+4,1;4,n+1,2;n+1,n+2,3;n+2,n+3,4;n+3,n+4,1;n+4,n+1,2];% Create modelmodel.modelname='genconstr';model.modelsense='max';% Set-up data for variables and constraintsmodel.vtype=repmat('B',nVars,1);model.ub=ones(nVars,1);model.obj=[zeros(2*nLiterals+nClauses,1);ones(nObj,1)];model.A=sparse(nLiterals,nVars);model.rhs=ones(nLiterals,1);model.sense=repmat('=',nLiterals,1);forj=1:nLiteralsmodel.varnames{j}=sprintf('X%d',j);model.varnames{nLiterals+j}=sprintf('notX%d',j);endforj=1:nClausesmodel.varnames{2*nLiterals+j}=sprintf('Clause%d',j);endforj=1:nObjmodel.varnames{2*nLiterals+nClauses+j}=sprintf('Obj%d',j);end% Link Xi and notXifori=1:nLiteralsmodel.A(i,i)=1;model.A(i,nLiterals+i)=1;model.constrnames{i}=sprintf('CNSTR_X%d',i);end% Link clauses and literalsfori=1:nClausesmodel.genconor(i).resvar=2*nLiterals+i;model.genconor(i).vars=Clauses(i:i,1:3);model.genconor(i).name=sprintf('CNSTR_Clause%d',i);end% Link objs with clausesmodel.genconmin.resvar=2*nLiterals+nClauses+1;fori=1:nClausesmodel.genconmin.vars(i)=2*nLiterals+i;endmodel.genconmin.name='CNSTR_Obj1';model.genconind.binvar=2*nLiterals+nClauses+2;model.genconind.binval=1;model.genconind.a=[zeros(2*nLiterals,1);ones(nClauses,1);zeros(nObj,1)];model.genconind.sense='>';model.genconind.rhs=4;model.genconind.name='CNSTR_Obj2';% Save modelgurobi_write(model,'genconstr_m.lp');% Optimizeparams.logfile='genconstr.log';result=gurobi(model,params);% Check optimization statusifstrcmp(result.status,'OPTIMAL')ifresult.objval>1.9fprintf('Logical expression is satisfiable\n');elseifresult.objval>0.9fprintf('At least four clauses are satisfiable\n');elsefprintf('At most three clauses may be satisfiable\n');endendelsefprintf('Optimization failed\n');end

#!/usr/bin/env python3# Copyright 2025, Gurobi Optimization, LLC# This example considers the following nonconvex nonlinear problem##  maximize    2 x    + y#  subject to  exp(x) + 4 sqrt(y) <= 9#              x, y >= 0##  We show you two approaches to solve this:##  1) Use a piecewise-linear approach to handle general function#     constraints (such as exp and sqrt).#     a) Add two variables#        u = exp(x)#        v = sqrt(y)#     b) Compute points (x, u) of u = exp(x) for some step length (e.g., x#        = 0, 1e-3, 2e-3, ..., xmax) and points (y, v) of v = sqrt(y) for#        some step length (e.g., y = 0, 1e-3, 2e-3, ..., ymax). We need to#        compute xmax and ymax (which is easy for this example, but this#        does not hold in general).#     c) Use the points to add two general constraints of type#        piecewise-linear.##  2) Use the Gurobis built-in general function constraints directly (EXP#     and POW). Here, we do not need to compute the points and the maximal#     possible values, which will be done internally by Gurobi.  In this#     approach, we show how to "zoom in" on the optimal solution and#     tighten tolerances to improve the solution quality.#importmathimportgurobipyasgpfromgurobipyimportGRBdefprintsol(m,x,y,u,v):print(f"x ={x.X}, u ={u.X}")print(f"y ={y.X}, v ={v.X}")print(f"Obj ={m.ObjVal}")# Calculate violation of exp(x) + 4 sqrt(y) <= 9vio=math.exp(x.X)+4*math.sqrt(y.X)-9ifvio<0:vio=0print(f"Vio ={vio}")try:# Create a new modelm=gp.Model()# Create variablesx=m.addVar(name="x")y=m.addVar(name="y")u=m.addVar(name="u")v=m.addVar(name="v")# Set objectivem.setObjective(2*x+y,GRB.MAXIMIZE)# Add constraintslc=m.addConstr(u+4*v<=9)# Approach 1) PWL constraint approachxpts=[]ypts=[]upts=[]vpts=[]intv=1e-3xmax=math.log(9)t=0.0whilet<xmax+intv:xpts.append(t)upts.append(math.exp(t))t+=intvymax=(9.0/4)*(9.0/4)t=0.0whilet<ymax+intv:ypts.append(t)vpts.append(math.sqrt(t))t+=intvgc1=m.addGenConstrPWL(x,u,xpts,upts,"gc1")gc2=m.addGenConstrPWL(y,v,ypts,vpts,"gc2")# Optimize the modelm.optimize()printsol(m,x,y,u,v)# Approach 2) General function constraint approach with auto PWL#             translation by Gurobi# restore unsolved state and get rid of PWL constraintsm.reset()m.remove(gc1)m.remove(gc2)m.update()# u = exp(x)gcf1=m.addGenConstrExp(x,u,name="gcf1")# v = y^(0.5)gcf2=m.addGenConstrPow(y,v,0.5,name="gcf2")# Use the equal piece length approach with the length = 1e-3m.Params.FuncPieces=1m.Params.FuncPieceLength=1e-3# Optimize the modelm.optimize()printsol(m,x,y,u,v)# Zoom in, use optimal solution to reduce the ranges and use a smaller# pclen=1-5 to solve itx.LB=max(x.LB,x.X-0.01)x.UB=min(x.UB,x.X+0.01)y.LB=max(y.LB,y.X-0.01)y.UB=min(y.UB,y.X+0.01)m.update()m.reset()m.Params.FuncPieceLength=1e-5# Optimize the modelm.optimize()printsol(m,x,y,u,v)exceptgp.GurobiErrorase:print(f"Error code{e.errno}:{e}")exceptAttributeError:print("Encountered an attribute error")

# 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.#library(Matrix)library(gurobi)# Set up parametersparams<-list()params$logfile<-'genconstr.log'# define primitive datanLiterals<-4nClauses<-8nObj<-2nVars<-2*nLiterals+nClauses+nObjLiteral<-function(n){n}NotLit<-function(n){n+nLiterals}Clause<-function(n){2*nLiterals+n}Obj<-function(n){2*nLiterals+nClauses+n}Clauses<-list(c(Literal(1),NotLit(2),Literal(3)),c(Literal(2),NotLit(3),Literal(4)),c(Literal(3),NotLit(4),Literal(1)),c(Literal(4),NotLit(1),Literal(2)),c(NotLit(1),NotLit(2),Literal(3)),c(NotLit(2),NotLit(3),Literal(4)),c(NotLit(3),NotLit(4),Literal(1)),c(NotLit(4),NotLit(1),Literal(2)))# Create modelmodel<-list()model$modelname<-'genconstr'model$modelsense<-'max'# Create objective function, variable names, and variable typesmodel$vtype<-rep('B',nVars)model$ub<-rep(1,nVars)model$varnames<-c(sprintf('X%d',seq(1,nLiterals)),sprintf('notX%d',seq(1,nLiterals)),sprintf('Clause%d',seq(1,nClauses)),sprintf('Obj%d',seq(1,nObj)))model$obj<-c(rep(0,2*nLiterals+nClauses),rep(1,nObj))# Create linear constraints linking literals and not literalsmodel$A<-spMatrix(nLiterals,nVars,i=c(seq(1,nLiterals),seq(1,nLiterals)),j=c(seq(1,nLiterals),seq(1+nLiterals,2*nLiterals)),x=rep(1,2*nLiterals))model$constrnames<-c(sprintf('CNSTR_X%d',seq(1,nLiterals)))model$rhs<-rep(1,nLiterals)model$sense<-rep('=',nLiterals)# Create OR general constraints linking clauses and literalsmodel$genconor<-lapply(1:nClauses,function(i)list(resvar=Clause(i),vars=Clauses[[i]],name=sprintf('CNSTR_Clause%d',i)))# Set up Obj1 = Min(Clause[1:nClauses])model$genconmin<-list(list(resvar=Obj(1),vars=c(seq(Clause(1),Clause(nClauses))),name='CNSTR_Obj1'))# the indicator constraint excepts the following vector types for the# linear sum:## - a dense vector, for example#   c(rep(0, 2*nLiterals), rep(1, nClauses), rep(0,nObj))# - a sparse vector, for example#   sparseVector( x = rep(1,nClauses), i = (2*nLiterals+1):(2*nLiterals+nClauses), length=nVars)# - In case all coefficients are the same, you can pass a vector of length#   one with the corresponding value which gets expanded to a dense vector#   with all values being the given one## We use a sparse vector in this examplea<-sparseVector(x=rep(1,nClauses),i=(2*nLiterals+1):(2*nLiterals+nClauses),length=nVars)# Set up Obj2 to signal if any clause is satisfied, i.e.# we use an indicator constraint of the form:#     (Obj2 = 1) -> sum(Clause[1:nClauses]) >= 4model$genconind<-list(list(binvar=Obj(2),binval=1,a=a,sense='>',rhs=4,name='CNSTR_Obj2'))# Save modelgurobi_write(model,'genconstr.lp',params)# Optimizeresult<-gurobi(model,params=params)# Check optimization statusif(result$status=='OPTIMAL'){if(result$objval>1.9){cat('Logical expression is satisfiable\n')}elseif(result$objval>0.9){cat('At least four clauses are satisfiable\n')}else{cat('At most three clauses may be satisfiable\n')}}else{cat('Optimization failed\n')}# Clear spacerm(model,result,params,Clauses)

' 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.'ImportsGurobiClassgenconstr_vbPublicConstnAsInteger=4PublicConstNLITERALSAsInteger=4'same as nPublicConstNCLAUSESAsInteger=8PublicConstNOBJAsInteger=2SharedSubMain()Try' Example data:' e.g. {0, n+1, 2} means clause (x0 or ~x1 or x2)DimClausesAsInteger(,)=NewInteger(,){_{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}}DimiAsInteger,statusAsInteger' Create environmentDimenvAsNewGRBEnv("genconstr_vb.log")' Create initial modelDimmodelAsNewGRBModel(env)model.ModelName="genconstr_vb"' Initialize decision variables and objectiveDimLitAsGRBVar()=NewGRBVar(NLITERALS-1){}DimNotLitAsGRBVar()=NewGRBVar(NLITERALS-1){}Fori=0ToNLITERALS-1Lit(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))NextDimClaAsGRBVar()=NewGRBVar(NCLAUSES-1){}Fori=0ToNCLAUSES-1Cla(i)=model.AddVar(0.0,1.0,0.0,GRB.BINARY,String.Format("Clause{0}",i))NextDimObjAsGRBVar()=NewGRBVar(NOBJ-1){}Fori=0ToNOBJ-1Obj(i)=model.AddVar(0.0,1.0,1.0,GRB.BINARY,String.Format("Obj{0}",i))Next' Link Xi and notXiDimlhsAsGRBLinExprFori=0ToNLITERALS-1lhs=NewGRBLinExpr()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))Next' Link clauses and literalsFori=0ToNCLAUSES-1DimclauseAsGRBVar()=NewGRBVar(2){}ForjAsInteger=0To2IfClauses(i,j)>=nThenclause(j)=NotLit(Clauses(i,j)-n)Elseclause(j)=Lit(Clauses(i,j))EndIfNextmodel.AddGenConstrOr(Cla(i),clause,String.Format("CNSTR_Clause{0}",i))Next' Link objs with clausesmodel.AddGenConstrMin(Obj(0),Cla,GRB.INFINITY,"CNSTR_Obj0")lhs=NewGRBLinExpr()Fori=0ToNCLAUSES-1lhs.AddTerm(1.0,Cla(i))Nextmodel.AddGenConstrIndicator(Obj(1),1,lhs,GRB.GREATER_EQUAL,4.0,"CNSTR_Obj1")' Set global objective sensemodel.ModelSense=GRB.MAXIMIZE' Save problemmodel.Write("genconstr_vb.mps")model.Write("genconstr_vb.lp")' Optimizemodel.Optimize()' Status checkingstatus=model.StatusIfstatus=GRB.Status.INF_OR_UNBDOrElse_status=GRB.Status.INFEASIBLEOrElse_status=GRB.Status.UNBOUNDEDThenConsole.WriteLine("The model cannot be solved "&_"because it is infeasible or unbounded")ReturnEndIfIfstatus<>GRB.Status.OPTIMALThenConsole.WriteLine("Optimization was stopped with status {0}",status)ReturnEndIf' Print resultDimobjvalAsDouble=model.ObjValIfobjval>1.9ThenConsole.WriteLine("Logical expression is satisfiable")ElseIfobjval>0.9ThenConsole.WriteLine("At least four clauses can be satisfied")ElseConsole.WriteLine("Not even three clauses can be satisfied")EndIf' Dispose of model and environmentmodel.Dispose()env.Dispose()CatcheAsGRBExceptionConsole.WriteLine("Error code: {0}. {1}",e.ErrorCode,e.Message)EndTryEndSubEndClass