[9] | 1 | /* SAT, Satisfiability Problem */ |
---|
| 2 | |
---|
| 3 | /* Written in GNU MathProg by Andrew Makhorin <mao@gnu.org> */ |
---|
| 4 | |
---|
| 5 | param m, integer, > 0; |
---|
| 6 | /* number of clauses */ |
---|
| 7 | |
---|
| 8 | param n, integer, > 0; |
---|
| 9 | /* number of variables */ |
---|
| 10 | |
---|
| 11 | set C{1..m}; |
---|
| 12 | /* clauses; each clause C[i], i = 1, ..., m, is disjunction of some |
---|
| 13 | variables or their negations; in the data section each clause is |
---|
| 14 | coded as a set of indices of corresponding variables, where negative |
---|
| 15 | indices mean negation; for example, the clause (x3 or not x7 or x11) |
---|
| 16 | is coded as the set { 3, -7, 11 } */ |
---|
| 17 | |
---|
| 18 | var x{1..n}, binary; |
---|
| 19 | /* main variables */ |
---|
| 20 | |
---|
| 21 | /* To solve the satisfiability problem means to determine all variables |
---|
| 22 | x[j] such that conjunction of all clauses C[1] and ... and C[m] takes |
---|
| 23 | on the value true, i.e. all clauses are satisfied. |
---|
| 24 | |
---|
| 25 | Let the clause C[i] be (t or t' or ... or t''), where t, t', ..., t'' |
---|
| 26 | are either variables or their negations. The condition of satisfying |
---|
| 27 | C[i] can be most naturally written as: |
---|
| 28 | |
---|
| 29 | t + t' + ... + t'' >= 1, (1) |
---|
| 30 | |
---|
| 31 | where t, t', t'' have to be replaced by either x[j] or (1 - x[j]). |
---|
| 32 | The formulation (1) leads to the mip problem with no objective, i.e. |
---|
| 33 | to a feasibility problem. |
---|
| 34 | |
---|
| 35 | Another, more practical way is to write the condition for C[i] as: |
---|
| 36 | |
---|
| 37 | t + t' + ... + t'' + y[i] >= 1, (2) |
---|
| 38 | |
---|
| 39 | where y[i] is an auxiliary binary variable, and minimize the sum of |
---|
| 40 | y[i]. If the sum is zero, all y[i] are also zero, and therefore all |
---|
| 41 | clauses are satisfied. If the sum is minimal but non-zero, its value |
---|
| 42 | shows the number of clauses which cannot be satisfied. */ |
---|
| 43 | |
---|
| 44 | var y{1..m}, binary, >= 0; |
---|
| 45 | /* auxiliary variables */ |
---|
| 46 | |
---|
| 47 | s.t. c{i in 1..m}: |
---|
| 48 | sum{j in C[i]} (if j > 0 then x[j] else (1 - x[-j])) + y[i] >= 1; |
---|
| 49 | /* the condition (2) */ |
---|
| 50 | |
---|
| 51 | minimize unsat: sum{i in 1..m} y[i]; |
---|
| 52 | /* number of unsatisfied clauses */ |
---|
| 53 | |
---|
| 54 | data; |
---|
| 55 | |
---|
| 56 | /* These data correspond to the instance hole6 (pigeon hole problem for |
---|
| 57 | 6 holes) from SATLIB, the Satisfiability Library, which is part of |
---|
| 58 | the collection at the Forschungsinstitut fuer anwendungsorientierte |
---|
| 59 | Wissensverarbeitung in Ulm Germany */ |
---|
| 60 | |
---|
| 61 | /* The optimal solution is 1 (one clause cannot be satisfied) */ |
---|
| 62 | |
---|
| 63 | param m := 133; |
---|
| 64 | |
---|
| 65 | param n := 42; |
---|
| 66 | |
---|
| 67 | set C[1] := -1 -7; |
---|
| 68 | set C[2] := -1 -13; |
---|
| 69 | set C[3] := -1 -19; |
---|
| 70 | set C[4] := -1 -25; |
---|
| 71 | set C[5] := -1 -31; |
---|
| 72 | set C[6] := -1 -37; |
---|
| 73 | set C[7] := -7 -13; |
---|
| 74 | set C[8] := -7 -19; |
---|
| 75 | set C[9] := -7 -25; |
---|
| 76 | set C[10] := -7 -31; |
---|
| 77 | set C[11] := -7 -37; |
---|
| 78 | set C[12] := -13 -19; |
---|
| 79 | set C[13] := -13 -25; |
---|
| 80 | set C[14] := -13 -31; |
---|
| 81 | set C[15] := -13 -37; |
---|
| 82 | set C[16] := -19 -25; |
---|
| 83 | set C[17] := -19 -31; |
---|
| 84 | set C[18] := -19 -37; |
---|
| 85 | set C[19] := -25 -31; |
---|
| 86 | set C[20] := -25 -37; |
---|
| 87 | set C[21] := -31 -37; |
---|
| 88 | set C[22] := -2 -8; |
---|
| 89 | set C[23] := -2 -14; |
---|
| 90 | set C[24] := -2 -20; |
---|
| 91 | set C[25] := -2 -26; |
---|
| 92 | set C[26] := -2 -32; |
---|
| 93 | set C[27] := -2 -38; |
---|
| 94 | set C[28] := -8 -14; |
---|
| 95 | set C[29] := -8 -20; |
---|
| 96 | set C[30] := -8 -26; |
---|
| 97 | set C[31] := -8 -32; |
---|
| 98 | set C[32] := -8 -38; |
---|
| 99 | set C[33] := -14 -20; |
---|
| 100 | set C[34] := -14 -26; |
---|
| 101 | set C[35] := -14 -32; |
---|
| 102 | set C[36] := -14 -38; |
---|
| 103 | set C[37] := -20 -26; |
---|
| 104 | set C[38] := -20 -32; |
---|
| 105 | set C[39] := -20 -38; |
---|
| 106 | set C[40] := -26 -32; |
---|
| 107 | set C[41] := -26 -38; |
---|
| 108 | set C[42] := -32 -38; |
---|
| 109 | set C[43] := -3 -9; |
---|
| 110 | set C[44] := -3 -15; |
---|
| 111 | set C[45] := -3 -21; |
---|
| 112 | set C[46] := -3 -27; |
---|
| 113 | set C[47] := -3 -33; |
---|
| 114 | set C[48] := -3 -39; |
---|
| 115 | set C[49] := -9 -15; |
---|
| 116 | set C[50] := -9 -21; |
---|
| 117 | set C[51] := -9 -27; |
---|
| 118 | set C[52] := -9 -33; |
---|
| 119 | set C[53] := -9 -39; |
---|
| 120 | set C[54] := -15 -21; |
---|
| 121 | set C[55] := -15 -27; |
---|
| 122 | set C[56] := -15 -33; |
---|
| 123 | set C[57] := -15 -39; |
---|
| 124 | set C[58] := -21 -27; |
---|
| 125 | set C[59] := -21 -33; |
---|
| 126 | set C[60] := -21 -39; |
---|
| 127 | set C[61] := -27 -33; |
---|
| 128 | set C[62] := -27 -39; |
---|
| 129 | set C[63] := -33 -39; |
---|
| 130 | set C[64] := -4 -10; |
---|
| 131 | set C[65] := -4 -16; |
---|
| 132 | set C[66] := -4 -22; |
---|
| 133 | set C[67] := -4 -28; |
---|
| 134 | set C[68] := -4 -34; |
---|
| 135 | set C[69] := -4 -40; |
---|
| 136 | set C[70] := -10 -16; |
---|
| 137 | set C[71] := -10 -22; |
---|
| 138 | set C[72] := -10 -28; |
---|
| 139 | set C[73] := -10 -34; |
---|
| 140 | set C[74] := -10 -40; |
---|
| 141 | set C[75] := -16 -22; |
---|
| 142 | set C[76] := -16 -28; |
---|
| 143 | set C[77] := -16 -34; |
---|
| 144 | set C[78] := -16 -40; |
---|
| 145 | set C[79] := -22 -28; |
---|
| 146 | set C[80] := -22 -34; |
---|
| 147 | set C[81] := -22 -40; |
---|
| 148 | set C[82] := -28 -34; |
---|
| 149 | set C[83] := -28 -40; |
---|
| 150 | set C[84] := -34 -40; |
---|
| 151 | set C[85] := -5 -11; |
---|
| 152 | set C[86] := -5 -17; |
---|
| 153 | set C[87] := -5 -23; |
---|
| 154 | set C[88] := -5 -29; |
---|
| 155 | set C[89] := -5 -35; |
---|
| 156 | set C[90] := -5 -41; |
---|
| 157 | set C[91] := -11 -17; |
---|
| 158 | set C[92] := -11 -23; |
---|
| 159 | set C[93] := -11 -29; |
---|
| 160 | set C[94] := -11 -35; |
---|
| 161 | set C[95] := -11 -41; |
---|
| 162 | set C[96] := -17 -23; |
---|
| 163 | set C[97] := -17 -29; |
---|
| 164 | set C[98] := -17 -35; |
---|
| 165 | set C[99] := -17 -41; |
---|
| 166 | set C[100] := -23 -29; |
---|
| 167 | set C[101] := -23 -35; |
---|
| 168 | set C[102] := -23 -41; |
---|
| 169 | set C[103] := -29 -35; |
---|
| 170 | set C[104] := -29 -41; |
---|
| 171 | set C[105] := -35 -41; |
---|
| 172 | set C[106] := -6 -12; |
---|
| 173 | set C[107] := -6 -18; |
---|
| 174 | set C[108] := -6 -24; |
---|
| 175 | set C[109] := -6 -30; |
---|
| 176 | set C[110] := -6 -36; |
---|
| 177 | set C[111] := -6 -42; |
---|
| 178 | set C[112] := -12 -18; |
---|
| 179 | set C[113] := -12 -24; |
---|
| 180 | set C[114] := -12 -30; |
---|
| 181 | set C[115] := -12 -36; |
---|
| 182 | set C[116] := -12 -42; |
---|
| 183 | set C[117] := -18 -24; |
---|
| 184 | set C[118] := -18 -30; |
---|
| 185 | set C[119] := -18 -36; |
---|
| 186 | set C[120] := -18 -42; |
---|
| 187 | set C[121] := -24 -30; |
---|
| 188 | set C[122] := -24 -36; |
---|
| 189 | set C[123] := -24 -42; |
---|
| 190 | set C[124] := -30 -36; |
---|
| 191 | set C[125] := -30 -42; |
---|
| 192 | set C[126] := -36 -42; |
---|
| 193 | set C[127] := 6 5 4 3 2 1; |
---|
| 194 | set C[128] := 12 11 10 9 8 7; |
---|
| 195 | set C[129] := 18 17 16 15 14 13; |
---|
| 196 | set C[130] := 24 23 22 21 20 19; |
---|
| 197 | set C[131] := 30 29 28 27 26 25; |
---|
| 198 | set C[132] := 36 35 34 33 32 31; |
---|
| 199 | set C[133] := 42 41 40 39 38 37; |
---|
| 200 | |
---|
| 201 | end; |
---|