genconstr.m
function genconstr()
% 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 = (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 data
n = 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 model
model.modelname = 'genconstr';
model.modelsense = 'max';
% Set-up data for variables and constraints
model.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);
for j = 1:nLiterals
model.varnames{j} = sprintf('X%d', j);
model.varnames{nLiterals+j} = sprintf('notX%d', j);
end
for j = 1:nClauses
model.varnames{2*nLiterals+j} = sprintf('Clause%d', j);
end
for j = 1:nObj
model.varnames{2*nLiterals+nClauses+j} = sprintf('Obj%d', j);
end
% Link Xi and notXi
for i = 1:nLiterals
model.A(i, i) = 1;
model.A(i, nLiterals+i) = 1;
model.constrnames{i} = sprintf('CNSTR_X%d', i);
end
% Link clauses and literals
for i = 1:nClauses
model.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 clauses
model.genconmin.resvar = 2 * nLiterals + nClauses + 1;
for i = 1:nClauses
model.genconmin.vars(i) = 2 * nLiterals + i;
end
model.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 model
gurobi_write(model, 'genconstr_m.lp');
% Optimize
params.logfile = 'genconstr.log';
result = gurobi(model, params);
% Check optimization status
if strcmp(result.status, 'OPTIMAL')
if result.objval > 1.9
fprintf('Logical expression is satisfiable\n');
else
if result.objval > 0.9
fprintf('At least four clauses are satisfiable\n');
else
fprintf('At most three clauses may be satisfiable\n');
end
end
else
fprintf('Optimization failed\n');
end
