1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/examples/sat.mod Mon Dec 06 13:09:21 2010 +0100
1.3 @@ -0,0 +1,201 @@
1.4 +/* SAT, Satisfiability Problem */
1.5 +
1.6 +/* Written in GNU MathProg by Andrew Makhorin <mao@gnu.org> */
1.7 +
1.8 +param m, integer, > 0;
1.9 +/* number of clauses */
1.10 +
1.11 +param n, integer, > 0;
1.12 +/* number of variables */
1.13 +
1.14 +set C{1..m};
1.15 +/* clauses; each clause C[i], i = 1, ..., m, is disjunction of some
1.16 + variables or their negations; in the data section each clause is
1.17 + coded as a set of indices of corresponding variables, where negative
1.18 + indices mean negation; for example, the clause (x3 or not x7 or x11)
1.19 + is coded as the set { 3, -7, 11 } */
1.20 +
1.21 +var x{1..n}, binary;
1.22 +/* main variables */
1.23 +
1.24 +/* To solve the satisfiability problem means to determine all variables
1.25 + x[j] such that conjunction of all clauses C[1] and ... and C[m] takes
1.26 + on the value true, i.e. all clauses are satisfied.
1.27 +
1.28 + Let the clause C[i] be (t or t' or ... or t''), where t, t', ..., t''
1.29 + are either variables or their negations. The condition of satisfying
1.30 + C[i] can be most naturally written as:
1.31 +
1.32 + t + t' + ... + t'' >= 1, (1)
1.33 +
1.34 + where t, t', t'' have to be replaced by either x[j] or (1 - x[j]).
1.35 + The formulation (1) leads to the mip problem with no objective, i.e.
1.36 + to a feasibility problem.
1.37 +
1.38 + Another, more practical way is to write the condition for C[i] as:
1.39 +
1.40 + t + t' + ... + t'' + y[i] >= 1, (2)
1.41 +
1.42 + where y[i] is an auxiliary binary variable, and minimize the sum of
1.43 + y[i]. If the sum is zero, all y[i] are also zero, and therefore all
1.44 + clauses are satisfied. If the sum is minimal but non-zero, its value
1.45 + shows the number of clauses which cannot be satisfied. */
1.46 +
1.47 +var y{1..m}, binary, >= 0;
1.48 +/* auxiliary variables */
1.49 +
1.50 +s.t. c{i in 1..m}:
1.51 + sum{j in C[i]} (if j > 0 then x[j] else (1 - x[-j])) + y[i] >= 1;
1.52 +/* the condition (2) */
1.53 +
1.54 +minimize unsat: sum{i in 1..m} y[i];
1.55 +/* number of unsatisfied clauses */
1.56 +
1.57 +data;
1.58 +
1.59 +/* These data correspond to the instance hole6 (pigeon hole problem for
1.60 + 6 holes) from SATLIB, the Satisfiability Library, which is part of
1.61 + the collection at the Forschungsinstitut fuer anwendungsorientierte
1.62 + Wissensverarbeitung in Ulm Germany */
1.63 +
1.64 +/* The optimal solution is 1 (one clause cannot be satisfied) */
1.65 +
1.66 +param m := 133;
1.67 +
1.68 +param n := 42;
1.69 +
1.70 +set C[1] := -1 -7;
1.71 +set C[2] := -1 -13;
1.72 +set C[3] := -1 -19;
1.73 +set C[4] := -1 -25;
1.74 +set C[5] := -1 -31;
1.75 +set C[6] := -1 -37;
1.76 +set C[7] := -7 -13;
1.77 +set C[8] := -7 -19;
1.78 +set C[9] := -7 -25;
1.79 +set C[10] := -7 -31;
1.80 +set C[11] := -7 -37;
1.81 +set C[12] := -13 -19;
1.82 +set C[13] := -13 -25;
1.83 +set C[14] := -13 -31;
1.84 +set C[15] := -13 -37;
1.85 +set C[16] := -19 -25;
1.86 +set C[17] := -19 -31;
1.87 +set C[18] := -19 -37;
1.88 +set C[19] := -25 -31;
1.89 +set C[20] := -25 -37;
1.90 +set C[21] := -31 -37;
1.91 +set C[22] := -2 -8;
1.92 +set C[23] := -2 -14;
1.93 +set C[24] := -2 -20;
1.94 +set C[25] := -2 -26;
1.95 +set C[26] := -2 -32;
1.96 +set C[27] := -2 -38;
1.97 +set C[28] := -8 -14;
1.98 +set C[29] := -8 -20;
1.99 +set C[30] := -8 -26;
1.100 +set C[31] := -8 -32;
1.101 +set C[32] := -8 -38;
1.102 +set C[33] := -14 -20;
1.103 +set C[34] := -14 -26;
1.104 +set C[35] := -14 -32;
1.105 +set C[36] := -14 -38;
1.106 +set C[37] := -20 -26;
1.107 +set C[38] := -20 -32;
1.108 +set C[39] := -20 -38;
1.109 +set C[40] := -26 -32;
1.110 +set C[41] := -26 -38;
1.111 +set C[42] := -32 -38;
1.112 +set C[43] := -3 -9;
1.113 +set C[44] := -3 -15;
1.114 +set C[45] := -3 -21;
1.115 +set C[46] := -3 -27;
1.116 +set C[47] := -3 -33;
1.117 +set C[48] := -3 -39;
1.118 +set C[49] := -9 -15;
1.119 +set C[50] := -9 -21;
1.120 +set C[51] := -9 -27;
1.121 +set C[52] := -9 -33;
1.122 +set C[53] := -9 -39;
1.123 +set C[54] := -15 -21;
1.124 +set C[55] := -15 -27;
1.125 +set C[56] := -15 -33;
1.126 +set C[57] := -15 -39;
1.127 +set C[58] := -21 -27;
1.128 +set C[59] := -21 -33;
1.129 +set C[60] := -21 -39;
1.130 +set C[61] := -27 -33;
1.131 +set C[62] := -27 -39;
1.132 +set C[63] := -33 -39;
1.133 +set C[64] := -4 -10;
1.134 +set C[65] := -4 -16;
1.135 +set C[66] := -4 -22;
1.136 +set C[67] := -4 -28;
1.137 +set C[68] := -4 -34;
1.138 +set C[69] := -4 -40;
1.139 +set C[70] := -10 -16;
1.140 +set C[71] := -10 -22;
1.141 +set C[72] := -10 -28;
1.142 +set C[73] := -10 -34;
1.143 +set C[74] := -10 -40;
1.144 +set C[75] := -16 -22;
1.145 +set C[76] := -16 -28;
1.146 +set C[77] := -16 -34;
1.147 +set C[78] := -16 -40;
1.148 +set C[79] := -22 -28;
1.149 +set C[80] := -22 -34;
1.150 +set C[81] := -22 -40;
1.151 +set C[82] := -28 -34;
1.152 +set C[83] := -28 -40;
1.153 +set C[84] := -34 -40;
1.154 +set C[85] := -5 -11;
1.155 +set C[86] := -5 -17;
1.156 +set C[87] := -5 -23;
1.157 +set C[88] := -5 -29;
1.158 +set C[89] := -5 -35;
1.159 +set C[90] := -5 -41;
1.160 +set C[91] := -11 -17;
1.161 +set C[92] := -11 -23;
1.162 +set C[93] := -11 -29;
1.163 +set C[94] := -11 -35;
1.164 +set C[95] := -11 -41;
1.165 +set C[96] := -17 -23;
1.166 +set C[97] := -17 -29;
1.167 +set C[98] := -17 -35;
1.168 +set C[99] := -17 -41;
1.169 +set C[100] := -23 -29;
1.170 +set C[101] := -23 -35;
1.171 +set C[102] := -23 -41;
1.172 +set C[103] := -29 -35;
1.173 +set C[104] := -29 -41;
1.174 +set C[105] := -35 -41;
1.175 +set C[106] := -6 -12;
1.176 +set C[107] := -6 -18;
1.177 +set C[108] := -6 -24;
1.178 +set C[109] := -6 -30;
1.179 +set C[110] := -6 -36;
1.180 +set C[111] := -6 -42;
1.181 +set C[112] := -12 -18;
1.182 +set C[113] := -12 -24;
1.183 +set C[114] := -12 -30;
1.184 +set C[115] := -12 -36;
1.185 +set C[116] := -12 -42;
1.186 +set C[117] := -18 -24;
1.187 +set C[118] := -18 -30;
1.188 +set C[119] := -18 -36;
1.189 +set C[120] := -18 -42;
1.190 +set C[121] := -24 -30;
1.191 +set C[122] := -24 -36;
1.192 +set C[123] := -24 -42;
1.193 +set C[124] := -30 -36;
1.194 +set C[125] := -30 -42;
1.195 +set C[126] := -36 -42;
1.196 +set C[127] := 6 5 4 3 2 1;
1.197 +set C[128] := 12 11 10 9 8 7;
1.198 +set C[129] := 18 17 16 15 14 13;
1.199 +set C[130] := 24 23 22 21 20 19;
1.200 +set C[131] := 30 29 28 27 26 25;
1.201 +set C[132] := 36 35 34 33 32 31;
1.202 +set C[133] := 42 41 40 39 38 37;
1.203 +
1.204 +end;