Try our new documentation site (beta).

Filter Content By
Version

### genconstr_c.c

/* 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 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)

int
main(void)
{
GRBenv   *env   = NULL;
GRBmodel *model = NULL;
int       error = 0;
int       cind[NVARS];
double    cval[NVARS];
char      buffer[MAXSTR];
int col, i, status;
double objval;

/* Example data */
const int Clauses[][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 */
if (error) goto QUIT;

/* Create initial model */
error = GRBnewmodel(env, &model, "genconstr_c", NVARS, NULL,
NULL, NULL, NULL, NULL);
if (error) goto QUIT;

/* 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) goto QUIT;

error = GRBsetstrattrelement(model, "VarName", col, buffer);
if (error) goto QUIT;

col = NOTLIT(i);
sprintf(buffer, "notX%d", i);
error = GRBsetcharattrelement(model, "VType", col, GRB_BINARY);
if (error) goto QUIT;

error = GRBsetstrattrelement(model, "VarName", col, buffer);
if (error) goto QUIT;
}

for (i = 0; i < NCLAUSES; i++) {
col = CLA(i);
sprintf(buffer, "Clause%d", i);
error = GRBsetcharattrelement(model, "VType", col, GRB_BINARY);
if (error) goto QUIT;

error = GRBsetstrattrelement(model, "VarName", col, buffer);
if (error) goto QUIT;
}

for (i = 0; i < NOBJ; i++) {
col = OBJ(i);
sprintf(buffer, "Obj%d", i);
error = GRBsetcharattrelement(model, "VType", col, GRB_BINARY);
if (error) goto QUIT;

error = GRBsetstrattrelement(model, "VarName", col, buffer);
if (error) goto QUIT;

error = GRBsetdblattrelement(model, "Obj", col, 1.0);
if (error) goto QUIT;
}

/* 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) goto QUIT;
}

/* 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) goto QUIT;
}

/* 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) goto QUIT;

/* note that passing 4 instead of 4.0 will produce undefined behavior */
OBJ(1), 1, NCLAUSES, cind, cval,
GRB_GREATER_EQUAL, 4.0);
if (error) goto QUIT;

/* Set global objective sense */
error = GRBsetintattr(model, GRB_INT_ATTR_MODELSENSE, GRB_MAXIMIZE);
if (error) goto QUIT;

/* Save problem */
error = GRBwrite(model, "genconstr_c.mps");
if (error) goto QUIT;

error = GRBwrite(model, "genconstr_c.lp");
if (error) goto QUIT;

/* Optimize */
error = GRBoptimize(model);
if (error) goto QUIT;

/* Status checking */
error = GRBgetintattr(model, "Status", &status);
if (error) goto QUIT;

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");
goto QUIT;
}
if (status != GRB_OPTIMAL) {
printf("Optimization was stopped with status %i\n", status);
goto QUIT;
}

/* Print result */
error = GRBgetdblattr(model, GRB_DBL_ATTR_OBJVAL, &objval);
if (error) goto QUIT;

if (objval > 1.9)
printf("Logical expression is satisfiable\n");
else if (objval > 0.9)
printf("At least four clauses can be satisfied\n");
else
printf("At most three clauses may be satisfied\n");

QUIT:

if (model != NULL) GRBfreemodel(model);
if (env != NULL)   GRBfreeenv(env);

return error;
}


Choose the evaluation license that fits you best, and start working with our Expert Team for technical guidance and support.

Get a free, full-featured license of the Gurobi Optimizer to experience the performance, support, benchmarking and tuning services we provide as part of our product offering.
Gurobi supports the teaching and use of optimization within academic institutions. We offer free, full-featured copies of Gurobi for use in class, and for research.
##### Cloud Trial

Request free trial hours, so you can see how quickly and easily a model can be solved on the cloud.