Description

Contributor: Michael Bussieck

Large Model of Type : GAMS

Category : GAMS Test library

Main file : gurobi03.gms

$TITLE 'GUROBI test suite - general constraints and,or' (GUROBI03,SEQ=710)
$ontext
Contributor: Michael Bussieck
$offtext

$set   genconstrAnd    4
$set   genconstrOr     5

Set l literals / 1*20 /, c clauses / c1*c100 /;
parameter cnf(c,l) 1 means x -1 menas not x, r1, r2, r3;

loop(c,
   r1 = uniformInt(-20,20);
   r2 = uniformInt(-20,20);
   r3 = uniformInt(-20,20);
   cnf(c,l)$(ord(l)=abs(r1)) = -1$(r1<0) + 1$(r1>0);
   cnf(c,l)$(ord(l)=abs(r2)) = -1$(r2<0) + 1$(r2>0);
   cnf(c,l)$(ord(l)=abs(r3)) = -1$(r3<0) + 1$(r3>0);
);

* MIP Max3-SAT model
binary variable x(l), f(c);
variable obj;
equation defcnf, defobj;
$macro xbar(i) (1-x(i))

defobj..    obj =e= sum(c, f(c));
defcnf(c).. sum(l$(cnf(c,l)<0), xbar(l))  + sum(l$(cnf(c,l)>0), x(l)) =g= f(c);

model max3satmip / defobj, defcnf /;
option optcr=0, solver=gurobi;

solve max3satmip max obj using mip;

set cc(c) set of satisfiable clauses;
cc(c) = f.l(c) > 0.5;

* General contraints 3-SAT model
binary variable xb(l) not x(l), r;
equation defxb(l), defOr(c), defAnd, defobj2;

defxb(l)..  xb(l) =e= 1-x(l);
defOr(cc).. f(cc) =e= sum(l$(cnf(cc,l)<0), xb(l))  + sum(l$(cnf(cc,l)>0), x(l));
defAnd..    r =e= sum(cc, f(cc));
defobj2..   obj =e= r;

model satGurobi / defxb, defOr, defAnd, defobj2 /;
$onecho > gurobi.opt
defOr.genconstrtype %genconstrOr%
defAnd.genconstrtype %genconstrAnd%
writeprob x.lp
$offecho

satGurobi.optfile = 1;
solve satGurobi max obj us mip;
abort$(abs(obj.l-1)>1e-6) 'expect a statisfyable SAT problem';

* If we took some clauses out, we can run with all clauses and see
* that the problem is not satisfyable anymore
if (card(cc)<>card(c),
  cc(c) = yes;
  solve satGurobi max obj us mip;
  abort$(abs(obj.l-0)>1e-6) 'expect a not-statisfyable SAT problem';
);