\$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'; );