1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/deps/glpk/examples/sat.mod	Sun Nov 06 20:59:10 2011 +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;