TAOCP 7.2.2.2: Satisfiability
Section 7.2.2.2 exercises: 105/525 solved.
Section 7.2.2.2. Satisfiability
Exercises from TAOCP Volume 4 Section 7.2.2.2: 105/525 solved.
| # | Rating | Category | Status | Time |
|---|---|---|---|---|
| 1 | [10] | simple | verified | 52s |
| 2 | [20] | medium | solved | 3m14s |
| 3 | ▶ [M21] | math-medium | solved | 1m |
| 4 | ▶ [22] | medium | solved | 4m28s |
| 5 | [M20] | math-medium | solved | 59s |
| 6 | ▶ [HM27] | hm-hard | verified | 1m17s |
| 7 | [25] | medium | verified | 3m04s |
| 8 | ▶ [22] | medium | verified | 1m05s |
| 9 | [M21] | math-medium | solved | 3m20s |
| 10 | ▶ [21] | medium | solved | 4m15s |
| 11 | ▶ [**] | verified | 57s | |
| 12 | ▶ [**] | solved | 3m21s | |
| 13 | [24] | medium | verified | 2m24s |
| 14 | [22] | medium | verified | 1m03s |
| 15 | [24] | medium | verified | 1m03s |
| 16 | [21] | medium | verified | 1m08s |
| 17 | [26] | hard | solved | 3m21s |
| 18 | ▶ [28] | hard | solved | 5m49s |
| 19 | ▶ [29] | hard | - | - |
| 20 | [40] | project | - | - |
| 21 | [22] | medium | - | - |
| 22 | [20] | medium | - | - |
| 23 | [20] | medium | - | - |
| 24 | ▶ [M32] | math-hard | - | - |
| 25 | [21] | medium | - | - |
| 26 | [22] | medium | - | - |
| 27 | [20] | medium | - | - |
| 28 | ▶ [20] | medium | - | - |
| 29 | ▶ [20] | medium | - | - |
| 30 | ▶ [22] | medium | - | - |
| 31 | [28] | hard | - | - |
| 32 | [15] | simple | - | - |
| 33 | [21] | medium | - | - |
| 34 | [HM26] | hm-hard | - | - |
| 36 | ▶ [**] | - | - | |
| 37 | [20] | medium | - | - |
| 38 | [M25] | math-medium | - | - |
| 39 | [M46] | math-research | - | - |
| 40 | [01] | simple | - | - |
| 41 | [M31] | math-hard | - | - |
| 42 | [21] | medium | - | - |
| 43 | ▶ [21] | medium | - | - |
| 44 | ▶ [30] | hard | - | - |
| 45 | [20] | medium | - | - |
| 46 | [30] | hard | - | - |
| 47 | [30] | hard | - | - |
| 48 | [20] | medium | - | - |
| 49 | [21] | medium | - | - |
| 50 | [24] | medium | - | - |
| 51 | [40] | project | - | - |
| 52 | [15] | simple | - | - |
| 53 | ▶ [M20] | math-medium | - | - |
| 54 | ▶ [29] | hard | - | - |
| 55 | [21] | medium | - | - |
| 56 | ▶ [22] | medium | - | - |
| 57 | [29] | hard | - | - |
| 58 | ▶ [20] | medium | - | - |
| 59 | [M20] | math-medium | - | - |
| 60 | [24] | medium | - | - |
| 61 | [30] | hard | - | - |
| 62 | [29] | hard | - | - |
| 63 | ▶ [29] | hard | - | - |
| 64 | [26] | hard | - | - |
| 65 | ▶ [28] | hard | - | - |
| 66 | [24] | medium | - | - |
| 67 | [**] | - | - | |
| 68 | [39] | project | - | - |
| 69 | [23] | medium | - | - |
| 70 | [21] | medium | - | - |
| 71 | ▶ [22] | medium | - | - |
| 72 | [28] | hard | - | - |
| 73 | ▶ [21] | medium | - | - |
| 74 | [M28] | math-hard | - | - |
| 75 | [M22] | math-medium | - | - |
| 76 | [41] | project | - | - |
| 77 | [20] | medium | - | - |
| 78 | [21] | medium | - | - |
| 79 | [29] | hard | - | - |
| 80 | [21] | medium | - | - |
| 81 | [21] | medium | - | - |
| 82 | ▶ [22] | medium | - | - |
| 83 | [21] | medium | - | - |
| 84 | [33] | hard | - | - |
| 85 | ▶ [39] | project | - | - |
| 86 | [M29] | math-hard | - | - |
| 87 | [21] | medium | - | - |
| 88 | [15] | simple | - | - |
| 89 | [21] | medium | - | - |
| 90 | [20] | medium | - | - |
| 91 | [M21] | math-medium | - | - |
| 92 | [20] | medium | - | - |
| 93 | [20] | medium | - | - |
| 94 | ▶ [21] | medium | - | - |
| 95 | [20] | medium | - | - |
| 96 | [22] | medium | - | - |
| 97 | [20] | medium | - | - |
| 98 | ▶ [M23] | math-medium | - | - |
| 99 | [25] | medium | - | - |
| 100 | [22] | medium | solved | 1m48s |
| 101 | ▶ [31] | hard | solved | 3m48s |
| 102 | [22] | medium | verified | 2m17s |
| 103 | [18] | medium | solved | 3m39s |
| 104 | [M21] | math-medium | solved | 4m18s |
| 105 | ▶ [M28] | math-hard | solved | 1m11s |
| 106 | [M20] | math-medium | verified | 3m11s |
| 107 | ▶ [22] | medium | solved | 6m46s |
| 108 | [23] | medium | solved | 3m26s |
| 109 | ▶ [20] | medium | verified | 1m04s |
| 110 | [19] | medium | verified | 3m31s |
| 111 | [40] | project | verified | 1m03s |
| 112 | [46] | research | solved | 2m57s |
| 113 | ▶ [30] | hard | solved | 4m31s |
| 114 | [27] | hard | solved | 3m |
| 115 | [25] | medium | solved | 3m36s |
| 116 | [22] | medium | verified | 4m03s |
| 117 | [23] | medium | verified | 1m05s |
| 118 | [20] | medium | verified | 3m24s |
| 119 | [18] | medium | solved | 1m33s |
| 120 | [M20] | math-medium | verified | 1m33s |
| 121 | [21] | medium | solved | 3m53s |
| 122 | ▶ [21] | medium | verified | 2m20s |
| 123 | [17] | medium | solved | 4m10s |
| 124 | ▶ [21] | medium | solved | 3m22s |
| 125 | ▶ [20] | medium | verified | 2m11s |
| 126 | [20] | medium | solved | 3m04s |
| 127 | [17] | medium | solved | 2m16s |
| 128 | [19] | medium | solved | 3m54s |
| 129 | [20] | medium | verified | 1m01s |
| 130 | [22] | medium | verified | 1m02s |
| 131 | ▶ [30] | hard | verified | 1m01s |
| 132 | ▶ [32] | hard | solved | 3m43s |
| 133 | ▶ [25] | medium | solved | 4m16s |
| 134 | [22] | medium | verified | 1m05s |
| 135 | ▶ [16] | medium | verified | 56s |
| 136 | [15] | simple | solved | 2m22s |
| 137 | [24] | medium | verified | 2m27s |
| 138 | [20] | medium | solved | 2m01s |
| 139 | [25] | medium | verified | 2m25s |
| 140 | [21] | medium | solved | 2m26s |
| 141 | [18] | medium | verified | 1m17s |
| 142 | [24] | medium | verified | 1m02s |
| 143 | ▶ [30] | hard | solved | 3m47s |
| 144 | [15] | simple | solved | 3m05s |
| 145 | [23] | medium | solved | 3m05s |
| 146 | [25] | medium | solved | 3m53s |
| 147 | [05] | simple | verified | 57s |
| 148 | [21] | medium | verified | 59s |
| 149 | ▶ [26] | hard | verified | 1m03s |
| 150 | [21] | medium | solved | 3m40s |
| 151 | ▶ [26] | hard | solved | 2m43s |
| 152 | [22] | medium | verified | 3m30s |
| 153 | [17] | medium | verified | 1m53s |
| 154 | [20] | medium | verified | 3m28s |
| 155 | [32] | hard | verified | 1m10s |
| 156 | [05] | simple | verified | 1m03s |
| 157 | [10] | simple | verified | 58s |
| 158 | [15] | simple | solved | 1m32s |
| 159 | [M17] | math-medium | verified | 1m18s |
| 160 | [18] | medium | verified | 1m12s |
| 161 | ▶ [21] | medium | verified | 1m17s |
| 162 | [21] | medium | verified | 2m42s |
| 163 | [M25] | math-medium | solved | 1m44s |
| 164 | [M30] | math-hard | verified | 1m19s |
| 165 | ▶ [26] | hard | verified | 2m37s |
| 166 | [30] | hard | solved | 3m41s |
| 167 | ▶ [21] | medium | solved | 5m52s |
| 168 | [26] | hard | verified | 1m04s |
| 169 | ▶ [HM30] | hm-hard | solved | 59s |
| 170 | [25] | medium | solved | 1m03s |
| 171 | [20] | medium | solved | 1m03s |
| 172 | [21] | medium | verified | 1m14s |
| 173 | [40] | project | verified | 2m08s |
| 174 | [15] | simple | solved | 50s |
| 175 | [32] | hard | solved | 1m12s |
| 176 | [M25] | math-medium | solved | 4m30s |
| 177 | [HM26] | hm-hard | solved | 4m |
| 178 | ▶ [M23] | math-medium | solved | 2m25s |
| 179 | [25] | medium | solved | 5m44s |
| 180 | ▶ [25] | medium | solved | 5m49s |
| 181 | ▶ [25] | medium | solved | 5m36s |
| 182 | [M16] | math-medium | solved | 5m27s |
| 183 | [M30] | math-hard | verified | 2m51s |
| 184 | [M20] | math-medium | verified | 4m03s |
| 185 | [M20] | math-medium | solved | 1m37s |
| 186 | [M21] | math-medium | solved | 3m05s |
| 187 | [M20] | math-medium | - | - |
| 188 | [HM25] | hm-medium | - | - |
| 189 | [27] | hard | - | - |
| 190 | [M20] | math-medium | - | - |
| 191 | [M25] | math-medium | - | - |
| 192 | ▶ [HM21] | hm-medium | - | - |
| 193 | [HM48] | hm-research | - | - |
| 194 | [HM19] | hm-medium | - | - |
| 195 | [HM21] | hm-medium | - | - |
| 196 | ▶ [HM25] | hm-medium | - | - |
| 197 | [HM21] | hm-medium | - | - |
| 198 | ▶ [HM30] | hm-hard | - | - |
| 199 | [M21] | math-medium | - | - |
| 200 | ▶ [M21] | math-medium | - | - |
| 201 | [HM29] | hm-hard | - | - |
| 202 | [HM21] | hm-medium | - | - |
| 203 | [HM93] | hm-research | - | - |
| 204 | ▶ [28] | hard | - | - |
| 205 | [26] | hard | - | - |
| 206 | [M22] | math-medium | - | - |
| 207 | [22] | medium | - | - |
| 208 | [25] | medium | - | - |
| 209 | [25] | medium | - | - |
| 210 | [M36] | math-project | - | - |
| 211 | [30] | hard | - | - |
| 212 | [32] | hard | - | - |
| 213 | ▶ [M26] | math-hard | - | - |
| 214 | [HM38] | hm-project | - | - |
| 215 | ▶ [HM23] | hm-medium | - | - |
| 216 | [HM38] | hm-project | - | - |
| 217 | [20] | medium | - | - |
| 218 | [20] | medium | - | - |
| 219 | ▶ [M20] | math-medium | - | - |
| 220 | [M24] | math-medium | - | - |
| 221 | [16] | medium | - | - |
| 222 | [M30] | math-hard | - | - |
| 223 | [HM40] | hm-project | - | - |
| 224 | [M20] | math-medium | - | - |
| 225 | ▶ [M31] | math-hard | - | - |
| 226 | [M30] | math-hard | - | - |
| 227 | [M27] | math-hard | - | - |
| 228 | ▶ [M21] | math-medium | - | - |
| 229 | [M21] | math-medium | - | - |
| 230 | [M22] | math-medium | - | - |
| 231 | [M30] | math-hard | - | - |
| 232 | [M28] | math-hard | - | - |
| 233 | [16] | medium | - | - |
| 234 | [20] | medium | - | - |
| 235 | [30] | hard | - | - |
| 236 | [8] | simple | - | - |
| 237 | [28] | hard | - | - |
| 238 | [HM21] | hm-medium | - | - |
| 239 | ▶ [M21] | math-medium | - | - |
| 240 | [HM23] | hm-medium | - | - |
| 241 | [20] | medium | - | - |
| 242 | [M20] | math-medium | - | - |
| 243 | [HM31] | hm-hard | - | - |
| 244 | [M20] | math-medium | - | - |
| 245 | ▶ [M27] | math-hard | - | - |
| 246 | ▶ [M28] | math-hard | - | - |
| 247 | [18] | medium | - | - |
| 248 | [M20] | math-medium | - | - |
| 249 | [18] | medium | - | - |
| 250 | [**] | - | - | |
| 251 | ▶ [30] | hard | - | - |
| 252 | [M26] | math-hard | - | - |
| 253 | ▶ [18] | medium | - | - |
| 254 | [16] | medium | - | - |
| 255 | ▶ [20] | medium | - | - |
| 256 | [20] | medium | - | - |
| 257 | ▶ [30] | hard | - | - |
| 258 | [21] | medium | - | - |
| 259 | [M20] | math-medium | - | - |
| 260 | [21] | medium | - | - |
| 261 | [21] | medium | - | - |
| 262 | [20] | medium | - | - |
| 263 | [21] | medium | - | - |
| 264 | [20] | medium | - | - |
| 265 | [21] | medium | - | - |
| 266 | [20] | medium | - | - |
| 267 | [25] | medium | - | - |
| 268 | [21] | medium | - | - |
| 269 | [29] | hard | - | - |
| 270 | [25] | medium | - | - |
| 271 | ▶ [25] | medium | - | - |
| 272 | [30] | hard | - | - |
| 273 | [27] | hard | - | - |
| 274 | [35] | hard | - | - |
| 275 | ▶ [22] | medium | - | - |
| 276 | [M15] | math-simple | - | - |
| 277 | [M18] | math-medium | - | - |
| 278 | [22] | medium | - | - |
| 279 | [M20] | math-medium | - | - |
| 280 | ▶ [M26] | math-hard | - | - |
| 281 | [21] | medium | - | - |
| 282 | ▶ [M33] | math-hard | - | - |
| 283 | [HM46] | hm-research | - | - |
| 284 | [23] | medium | - | - |
| 285 | [19] | medium | - | - |
| 286 | [M24] | math-medium | - | - |
| 287 | [25] | medium | - | - |
| 288 | [28] | hard | - | - |
| 289 | [M20] | math-medium | - | - |
| 290 | [17] | medium | - | - |
| 291 | [20] | medium | - | - |
| 292 | [M21] | math-medium | - | - |
| 293 | [21] | medium | - | - |
| 294 | [HM21] | hm-medium | - | - |
| 295 | [M23] | math-medium | - | - |
| 296 | [HM20] | hm-medium | - | - |
| 297 | ▶ [HM26] | hm-hard | - | - |
| 298 | [HM22] | hm-medium | - | - |
| 299 | [HM23] | hm-medium | - | - |
| 300 | ▶ [25] | medium | - | - |
| 301 | ▶ [25] | medium | - | - |
| 302 | [26] | hard | - | - |
| 303 | [HM20] | hm-medium | - | - |
| 304 | [HM34] | hm-hard | - | - |
| 305 | ▶ [M25] | math-medium | - | - |
| 306 | ▶ [HM32] | hm-hard | - | - |
| 307 | [HM28] | hm-hard | - | - |
| 308 | [M29] | math-hard | - | - |
| 309 | [20] | medium | - | - |
| 310 | [M25] | math-medium | - | - |
| 311 | [21] | medium | - | - |
| 312 | [HM24] | hm-medium | - | - |
| 313 | ▶ [22] | medium | - | - |
| 314 | [36] | project | - | - |
| 315 | [M18] | math-medium | - | - |
| 316 | [HM20] | hm-medium | - | - |
| 317 | ▶ [M26] | math-hard | - | - |
| 318 | [HM27] | hm-hard | - | - |
| 319 | [HM20] | hm-medium | - | - |
| 320 | [HM24] | hm-medium | - | - |
| 321 | [M24] | math-medium | - | - |
| 322 | ▶ [HM35] | hm-hard | - | - |
| 323 | [10] | simple | - | - |
| 324 | ▶ [22] | medium | - | - |
| 325 | [20] | medium | - | - |
| 326 | [20] | medium | - | - |
| 327 | [22] | medium | - | - |
| 328 | [20] | medium | - | - |
| 329 | [21] | medium | - | - |
| 330 | ▶ [21] | medium | - | - |
| 331 | [M20] | math-medium | - | - |
| 332 | [20] | medium | - | - |
| 333 | ▶ [M20] | math-medium | - | - |
| 334 | [25] | medium | - | - |
| 335 | [HM26] | hm-hard | - | - |
| 336 | ▶ [M20] | math-medium | - | - |
| 337 | [M20] | math-medium | - | - |
| 338 | [M21] | math-medium | - | - |
| 339 | ▶ [HM26] | hm-hard | - | - |
| 340 | ▶ [M20] | math-medium | - | - |
| 341 | [M25] | math-medium | - | - |
| 342 | [HM25] | hm-medium | - | - |
| 343 | ▶ [M25] | math-medium | - | - |
| 344 | [M33] | math-hard | - | - |
| 345 | [M30] | math-hard | - | - |
| 346 | ▶ [HM28] | hm-hard | - | - |
| 347 | ▶ [M28] | math-hard | - | - |
| 348 | [HM26] | hm-hard | - | - |
| 349 | ▶ [M24] | math-medium | - | - |
| 350 | ▶ [HM26] | hm-hard | - | - |
| 351 | [25] | medium | - | - |
| 352 | [M21] | math-medium | - | - |
| 353 | [M21] | math-medium | - | - |
| 354 | [HM20] | hm-medium | - | - |
| 355 | [HM21] | hm-medium | - | - |
| 356 | ▶ [M35] | math-hard | - | - |
| 357 | ▶ [M20] | math-medium | - | - |
| 358 | [M20] | math-medium | - | - |
| 359 | [20] | medium | - | - |
| 360 | [M23] | math-medium | - | - |
| 361 | ▶ [M25] | math-medium | - | - |
| 362 | [20] | medium | - | - |
| 363 | ▶ [M30] | math-hard | - | - |
| 364 | ▶ [M21] | math-medium | - | - |
| 365 | [M37] | math-project | - | - |
| 366 | ▶ [18] | medium | - | - |
| 367 | ▶ [20] | medium | - | - |
| 368 | [76] | research | - | - |
| 369 | ▶ [**] | - | - | |
| 370 | [20] | medium | - | - |
| 371 | [24] | medium | - | - |
| 372 | [25] | medium | - | - |
| 373 | [35] | hard | - | - |
| 374 | ▶ [32] | hard | - | - |
| 375 | [21] | medium | - | - |
| 376 | ▶ [32] | hard | - | - |
| 377 | [22] | medium | - | - |
| 378 | [39] | project | - | - |
| 379 | ▶ [20] | medium | - | - |
| 380 | [21] | medium | - | - |
| 381 | [22] | medium | - | - |
| 382 | [30] | hard | - | - |
| 383 | ▶ [23] | medium | - | - |
| 384 | [25] | medium | - | - |
| 385 | [**] | - | - | |
| 386 | ▶ [M25] | math-medium | - | - |
| 387 | [21] | medium | - | - |
| 388 | [20] | medium | - | - |
| 389 | [22] | medium | - | - |
| 390 | [23] | medium | - | - |
| 391 | [M25] | math-medium | - | - |
| 392 | [22] | medium | - | - |
| 393 | [25] | medium | - | - |
| 394 | [25] | medium | - | - |
| 395 | [20] | medium | - | - |
| 396 | ▶ [23] | medium | - | - |
| 397 | [22] | medium | - | - |
| 398 | [18] | medium | - | - |
| 399 | [23] | medium | - | - |
| 400 | [25] | medium | - | - |
| 401 | [16] | medium | - | - |
| 402 | [18] | medium | - | - |
| 403 | [20] | medium | - | - |
| 404 | ▶ [21] | medium | - | - |
| 405 | ▶ [M25] | math-medium | - | - |
| 406 | [M24] | math-medium | - | - |
| 407 | [M22] | math-medium | - | - |
| 408 | ▶ [25] | medium | - | - |
| 409 | ▶ [M26] | math-hard | - | - |
| 410 | [24] | medium | - | - |
| 411 | [25] | medium | - | - |
| 412 | [40] | project | - | - |
| 413 | [M23] | math-medium | - | - |
| 414 | [M20] | math-medium | - | - |
| 415 | [M22] | math-medium | - | - |
| 416 | [20] | medium | - | - |
| 417 | [21] | medium | - | - |
| 418 | [23] | medium | - | - |
| 419 | [M21] | math-medium | - | - |
| 420 | [18] | medium | - | - |
| 421 | [18] | medium | - | - |
| 422 | [11] | simple | - | - |
| 423 | [22] | medium | - | - |
| 424 | ▶ [20] | medium | - | - |
| 425 | [18] | medium | - | - |
| 426 | ▶ [M20] | math-medium | - | - |
| 427 | [M30] | math-hard | - | - |
| 428 | [M27] | math-hard | - | - |
| 429 | [22] | medium | - | - |
| 430 | [25] | medium | - | - |
| 431 | ▶ [20] | medium | - | - |
| 432 | [34] | hard | - | - |
| 433 | [25] | medium | - | - |
| 434 | [21] | medium | - | - |
| 435 | ▶ [28] | hard | - | - |
| 436 | [M32] | math-hard | - | - |
| 437 | [M21] | math-medium | - | - |
| 438 | [21] | medium | - | - |
| 439 | [20] | medium | - | - |
| 440 | [M33] | math-hard | - | - |
| 441 | [M35] | math-hard | - | - |
| 442 | ▶ [M27] | math-hard | - | - |
| 443 | [**] | - | - | |
| 444 | [M26] | math-hard | - | - |
| 445 | ▶ [22] | medium | - | - |
| 446 | [M10] | math-simple | - | - |
| 447 | ▶ [22] | medium | - | - |
| 448 | [M23] | math-medium | - | - |
| 449 | [21] | medium | - | - |
| 450 | [25] | medium | - | - |
| 451 | ▶ [28] | hard | - | - |
| 452 | [34] | hard | - | - |
| 453 | [M23] | math-medium | - | - |
| 454 | [15] | simple | - | - |
| 455 | [M20] | math-medium | - | - |
| 456 | [M21] | math-medium | - | - |
| 457 | [HM19] | hm-medium | - | - |
| 458 | [20] | medium | - | - |
| 459 | ▶ [20] | medium | - | - |
| 460 | [21] | medium | - | - |
| 461 | [20] | medium | - | - |
| 462 | [22] | medium | - | - |
| 463 | ▶ [M21] | math-medium | - | - |
| 464 | ▶ [M25] | math-medium | - | - |
| 465 | [M21] | math-medium | - | - |
| 466 | [M23] | math-medium | - | - |
| 467 | [20] | medium | - | - |
| 468 | [20] | medium | - | - |
| 469 | ▶ [**] | - | - | |
| 470 | ▶ [**] | - | - | |
| 471 | [16] | medium | - | - |
| 472 | [**] | - | - | |
| 473 | ▶ [**] | - | - | |
| 474 | [**] | - | - | |
| 475 | [**] | - | - | |
| 476 | [**] | - | - | |
| 477 | ▶ [23] | medium | - | - |
| 478 | ▶ [23] | medium | - | - |
| 479 | ▶ [25] | medium | - | - |
| 480 | [25] | medium | - | - |
| 481 | ▶ [28] | hard | - | - |
| 482 | ▶ [26] | hard | - | - |
| 483 | [21] | medium | - | - |
| 484 | [22] | medium | - | - |
| 485 | ▶ [23] | medium | - | - |
| 486 | [21] | medium | - | - |
| 487 | ▶ [27] | hard | - | - |
| 488 | [24] | medium | - | - |
| 489 | [M21] | math-medium | - | - |
| 490 | [15] | simple | - | - |
| 491 | [22] | medium | - | - |
| 492 | [M20] | math-medium | - | - |
| 493 | [20] | medium | - | - |
| 494 | [21] | medium | - | - |
| 495 | [M22] | math-medium | - | - |
| 496 | [M20] | math-medium | - | - |
| 497 | [22] | medium | - | - |
| 498 | [22] | medium | - | - |
| 499 | [21] | medium | - | - |
| 500 | [16] | medium | - | - |
| 501 | [22] | medium | - | - |
| 502 | [16] | medium | - | - |
| 503 | [M20] | math-medium | - | - |
| 504 | ▶ [M21] | math-medium | - | - |
| 505 | [21] | medium | - | - |
| 506 | [22] | medium | - | - |
| 507 | ▶ [21] | medium | - | - |
| 508 | [M20] | math-medium | - | - |
| 509 | [20] | medium | - | - |
| 510 | [18] | medium | - | - |
| 511 | [22] | medium | - | - |
| 512 | [29] | hard | - | - |
| 513 | [24] | medium | - | - |
| 514 | [24] | medium | - | - |
| 515 | ▶ [23] | medium | - | - |
| 516 | [M9] | math-simple | - | - |
| 517 | [25] | medium | - | - |
| 518 | [M32] | math-hard | - | - |
| 519 | [20] | medium | - | - |
| 520 | ▶ [24] | medium | - | - |
| 521 | [30] | hard | - | - |
| 522 | ▶ [26] | hard | - | - |
| 523 | [20] | medium | - | - |
| 524 | ▶ [22] | medium | - | - |
| 525 | ▶ [40] | project | - | - |
| 526 | [M25] | math-medium | - | - |
TAOCP 7.2.2.2 Exercise 1
A set of clauses is interpreted as the conjunction of its clauses.
TAOCP 7.2.2.2 Exercise 2
We restart the analysis from the logical structure rather than a one-model construction.
TAOCP 7.2.2.2 Exercise 3
The instance $\mathrm{waerden}(j,k;n)$ encodes the statement that every $j$-coloring of ${1,\ldots,n}$ contains a monochromatic arithmetic progression of length $k$.
TAOCP 7.2.2.2 Exercise 4
Let $x_1,\dots,x_9\in\{0,1\}$ be a 2-coloring of $\{1,\dots,9\}$.
TAOCP 7.2.2.2 Exercise 5
Let $W(3,4)$ denote the least $n$ such that every 2-coloring of ${1,\ldots,n}$ contains a monochromatic arithmetic progression of length $3$ in color $1$ or length $4$ in color $2$.
TAOCP 7.2.2.2 Exercise 6
Let $[n]={1,2,\ldots,n}$.
TAOCP 7.2.2.2 Exercise 7
We restate the system of clauses: \begin{aligned} C_1 &= x_1 \vee x_2 \vee x_3,\\ C_2 &= x_2 \vee \neg x_3 \vee x_4,\\ C_3 &= x_3 \vee x_4 \vee x_1,\\
TAOCP 7.2.2.2 Exercise 8
Let $G$ be a graph on vertex set ${1,\ldots,n}$, and let $k$ be given.
TAOCP 7.2.2.2 Exercise 9
The quantity $C(k,r,s)$ in TAOCP §7.
TAOCP 7.2.2.2 Exercise 10
Let $F=\{C_1,\dots,C_m\}$ be a consistent set of clauses over variables $x_1,\dots,x_n$.
TAOCP 7.2.2.2 Exercise 11
In the representation leading to (12), each clause is converted into implications of the form “literals on the left of $\rightarrow$ imply literals or clauses on the right,” and a clause contributes t...
TAOCP 7.2.2.2 Exercise 12
We rewrite the argument from the ground up, separating the counting statement in (a) from the digraph interpretation in (b), and avoiding any conflation between variables and implications.
TAOCP 7.2.2.2 Exercise 13
Let $p_{k,i}$ denote the choice of placing the first occurrence of $k\in\{1,2,3,4\}$ at position $i$ in a length $8$ sequence, with the second occurrence forced to lie at position $i+k+1$.
TAOCP 7.2.2.2 Exercise 14
The clauses (17) encode a graph coloring instance as a conjunctive normal form formula in which each vertex is assigned one of a fixed set of colors, and adjacent vertices are forbidden from receiving...
TAOCP 7.2.2.2 Exercise 15
Let $K_n$ denote the complete graph on the vertex set ${1,2,\ldots,n}$.
TAOCP 7.2.2.2 Exercise 16
Let $M_n$ denote the McGregor graph of order $n \ge 3$, defined in Exercise 7.
TAOCP 7.2.2.2 Exercise 17
The reviewer’s objections concern only the missing _computational execution_, not the correctness of the reduction or SAT encoding.
TAOCP 7.2.2.2 Exercise 18
We seek all integers $n < 10^9$ such that the equation $x_1 + x_2 + \cdots + x_n = x_1 x_2 \cdots x_n$ has exactly one solution in positive integers satisfying $x_1 \ge x_2 \ge \cdots \ge x_n$.
TAOCP 7.2.2.2 Exercise 100
A process is _starved_ if it is enabled infinitely often but never reaches its critical state.
TAOCP 7.2.2.2 Exercise 101
The previous construction fails because it attempts to _compute a tie-breaking relation from concurrently changing variables_.
TAOCP 7.2.2.2 Exercise 102
The error in the previous solution is that it tries to simulate flickering reads by branching on the _value of the shared variable_ $v$.
TAOCP 7.2.2.2 Exercise 103
The previous solution fails because it attempts to proceed as if a complete discrete tomography instance were given, then introduces unsubstantiated repairs to the data.
TAOCP 7.2.2.2 Exercise 104
Let the NW–SE diagonals be indexed by $s=i+j$ with $2\le s\le m+n$, and the NE–SW diagonals by $d=i-j$ with $-(n-1)\le d\le m-1$.
TAOCP 7.2.2.2 Exercise 105
Let $Y = (y_{ij})$ be an $m \times n$ matrix with entries in ${-1,0,+1}$.
TAOCP 7.2.2.2 Exercise 106
The input data consist of three independent families of integer-valued sums.
TAOCP 7.2.2.2 Exercise 107
Let $p=6$, $n=13$, and the first row be x_{1,\bullet} = 1111101111101, so
TAOCP 7.2.2.2 Exercise 108
The key issue is that the problem is not about constructing a function on all of $\mathbb{Z}^2$, but about assigning values on a _fixed finite set of gray pixels in one period-6 fundamental domain_, w...
TAOCP 7.2.2.2 Exercise 109
Let $F(x_1,\ldots,x_n)$ be the given satisfiability instance, and assume access to a SAT solver that decides satisfiability and returns a satisfying assignment when one exists.
TAOCP 7.2.2.2 Exercise 110
Let $S$ be the set of all colorings x_1,\dots,x_{96}\in\{1,2,3\} such that no color class contains a 10-term arithmetic progression.
TAOCP 7.2.2.2 Exercise 111
Let $F(x_1,\ldots,x_n)$ be the Boolean formula corresponding to the “Cheshire Tom” instance in Fig.
TAOCP 7.2.2.2 Exercise 112
The previous argument fails because it never instantiates the tomography constraints from Fig.
TAOCP 7.2.2.2 Exercise 113
The flaw in the previous solution is fundamental: it fails to ensure that the constructed instance satisfies the requirement $a_d \in \{0,1\}$.
TAOCP 7.2.2.2 Exercise 114
A correct solution must operate on the _actual constraint instance defined by state $(\gamma)$_.
TAOCP 7.2.2.2 Exercise 115
The key issue in the previous solution is not mathematical modeling but the absence of an actual empirical estimate.
TAOCP 7.2.2.2 Exercise 116
The original argument fails at the point where it assumes a non-symmetry (column swapping) preserves the Game of Life evolution.
TAOCP 7.2.2.2 Exercise 117
Let $\nu x = x_1 + \cdots + x_n$ and $\nu^{(2)}x = x_1x_2 + x_2x_3 + \cdots + x_{n-1}x_n$.
TAOCP 7.2.2.2 Exercise 118
Let the region be a finite set of unit pixels $P \subset \mathbb{Z}^2$.
TAOCP 7.2.2.2 Exercise 119
Let $F = \mathit{warden}(3,3;9)$ be the 32-clause formula defined in (9).
TAOCP 7.2.2.2 Exercise 120
Let $F$ be a family of clauses and $L$ a set of literals.
TAOCP 7.2.2.2 Exercise 121
We restate only the pointer-level modifications for binary clauses, making all changes to incidence-list links and clause-cycle links explicit.
TAOCP 7.2.2.2 Exercise 122
We restate Algorithm A in the only way relevant to the modification: it performs a depth-first backtracking search over partial consistent sets of literals $L$, with choice points where a literal is s...
TAOCP 7.2.2.2 Exercise 123
The previous solution failed because it replaced the actual instance $R'(7)$ from equation (7) with an invented set of clauses.
TAOCP 7.2.2.2 Exercise 124
Let the structure be Knuth’s orthogonal doubly linked representation used for exact cover: each node $x$ has four link fields L[x],\ R[x],\ U[x],\ D[x], and each row and column is a circular list with...
TAOCP 7.2.2.2 Exercise 125
Let Algorithm B maintain a set $L$ of literals that is always **strictly consistent**, meaning it never contains both $x_i$ and $\neg x_i$ for any variable $x_i$, and it never contains duplicates.
TAOCP 7.2.2.2 Exercise 126
The exercise asks for a _specific continuation_ of the computation shown in equation (59).
TAOCP 7.2.2.2 Exercise 127
Let the computation in (59) be viewed in terms of Algorithm B’s move-code interpretation: each edge in the search tree is labeled by a move code $m_i$, where forward extension corresponds to choosing...
TAOCP 7.2.2.2 Exercise 128
The previous argument failed because it did not represent Algorithm D as a full backtracking computation in the sense of TAOCP §7.
TAOCP 7.2.2.2 Exercise 129
Let $\mathcal{C}(l)$ denote the set of clauses in which the literal $l$ is currently being watched in Algorithm D.
TAOCP 7.2.2.2 Exercise 130
Let $W(l)$ denote the head pointer of the watch list for literal $l$, and let each node of a watch list be a record containing a clause pointer $C$ and a link field $next$.
TAOCP 7.2.2.2 Exercise 131
Let Algorithm D be in the state described after completion of step D3 with no unit clauses discovered.
TAOCP 7.2.2.2 Exercise 132
The previous construction fails because it makes the formula satisfied at the root, so Algorithm D halts immediately.
TAOCP 7.2.2.2 Exercise 133
A backtrack tree for $\mathrm{waerden}(3,3;9)$ is built from binary assignments $x_1,\dots,x_9 \in \{0,1\}$, branching on a fixed variable order.
TAOCP 7.2.2.2 Exercise 134
Each BIMP table entry is maintained as a dynamically growing array whose capacity is always a power-of-two multiple of the initial size $4$.
TAOCP 7.2.2.2 Exercise 135
Let $D$ be the implication digraph of the given SAT instance.
TAOCP 7.2.2.2 Exercise 136
We restart from the formal definition used in TAOCP for TIMP.
TAOCP 7.2.2.2 Exercise 137
We restate the operations in the exact structure of Algorithm L, making explicit only the mechanisms actually available in the data structures: circular doubly linked free list of variables, and for e...
TAOCP 7.2.2.2 Exercise 138
Step L9 of Algorithm L operates purely as a local propagation step over the binary implication lists.
TAOCP 7.2.2.2 Exercise 139
Let a binary clause $u \vee v$ be represented by the two implication edges u \to v, \qquad v \to u, and let $\mathrm{BIMP}(x)$ and $\mathrm{BPRED}(x)$ be maintained as mutual adjacency lists of succes...
TAOCP 7.2.2.2 Exercise 140
The earlier argument fails because ISTACK is not constrained by variables.
TAOCP 7.2.2.2 Exercise 141
Algorithm L uses the standard timestamp technique in which a global counter $\mathrm{ISTAMP}$ is incremented whenever a new marking phase begins, and each literal $l$ stores a value $\mathrm{IST}(l)$...
TAOCP 7.2.2.2 Exercise 142
Let Algorithm L run and consider the chronological sequence of assignments to literals, written in the order in which each literal first receives a truth value.
TAOCP 7.2.2.2 Exercise 143
We restart the construction so that the definition of “big clause” is enforced consistently at every stage of the algorithm.
TAOCP 7.2.2.2 Exercise 144
The previous solution fails because it assumes an additive constant survives normalization unchanged.
TAOCP 7.2.2.2 Exercise 145
The exercise, as stated in the prompt, cannot be solved because it omits the data that determine the requested numerical values.
TAOCP 7.2.2.2 Exercise 146
When Algorithm L is extended to clauses of arbitrary length, the heuristic should continue to estimate the "support" for setting a literal $l$ to true by combining the contributions of all clauses con...
TAOCP 7.2.2.2 Exercise 147
From (66), $C_{\max}(d) = C_0 C_1^d$.
TAOCP 7.2.2.2 Exercise 148
Equation (66) defines a bound $C_{\max}(d)$ on the number of candidate nodes considered by the search procedure at depth $d$ of the backtracking process.
TAOCP 7.2.2.2 Exercise 149
Let the current instance of SAT in Algorithm L consist of a family $F$ of clauses over variables $x_1,\ldots,x_n$.
TAOCP 7.2.2.2 Exercise 150
The previous solution failed because it replaced the concrete clause structure of (70) with schematic placeholders.
TAOCP 7.2.2.2 Exercise 151
Let $D=(V,E)$ be the dependency digraph (68), where $v\to u\in E$ means $u$ depends on $v$.
TAOCP 7.2.2.2 Exercise 152
We correct both parts from first principles, using the actual meaning of step $X3$ in Knuth’s procedure: “participants” are variables that occur in the current reduced clause set, and “forced” means d...
TAOCP 7.2.2.2 Exercise 153
Let $p$ be a candidate generated in step X3, and let $C(p)$ denote the number of clauses already satisfied by the partial assignment $p$.
TAOCP 7.2.2.2 Exercise 154
Start by restating the implication digraph and the subforest, then fix the level assignment so that every directed edge goes from a higher level to a lower level, as required.
TAOCP 7.2.2.2 Exercise 155
Let $F = {C_1,\dots,C_m}$ be a formula in CNF over variables ${x_1,\dots,x_n}$, and let literals be ordered by variable index with complements $\bar{l}$.
TAOCP 7.2.2.2 Exercise 156
Let $v$ be a variable that is pure in $F$, so every occurrence of $v$ in every clause of $F$ has the same sign, either all occurrences are $v$ or all are $\bar v$.
TAOCP 7.2.2.2 Exercise 157
Consider the formula F = \{\, a b,\ \bar{a} c \,\}.
TAOCP 7.2.2.2 Exercise 158
Let $l$ be a pure literal in a formula $F$.
TAOCP 7.2.2.2 Exercise 159
A set $A$ of literals is an autarky for a family $F$ of clauses if every clause that contains a literal $l$ with $l \in A$ is satisfied by $A$.
TAOCP 7.2.2.2 Exercise 160
Let literals be colored white, black, or gray, with the constraint that a literal $l$ is white if and only if $\bar{l}$ is black.
TAOCP 7.2.2.2 Exercise 161
Let $F$ be a set of clauses satisfying the condition that every clause containing a white literal also contains either a black literal or a blue literal.
TAOCP 7.2.2.2 Exercise 162
A clause $C$ is **blocked by a literal $u \in C$** if for every clause $D \in F$ containing $\bar u$, the resolvent (C \setminus \{u\}) \cup (D \setminus \{\bar u\}) is a tautology, meaning it contain...
TAOCP 7.2.2.2 Exercise 163
Let $n(F)$ denote the number of distinct variables occurring in $F$.
TAOCP 7.2.2.2 Exercise 164
Let $F$ be a $k$SAT instance on variables ${x_1,\ldots,x_n}$, so every clause of $F$ has size at most $k$.
TAOCP 7.2.2.2 Exercise 165
The previous maximality argument fails because it tries to compare an arbitrary autarky $B$ with intermediate sets $A_t$ by reasoning about individual clause-triggered deletions.
TAOCP 7.2.2.2 Exercise 166
We justify step X9 by reconstructing the missing link between the condition $w=0$ in (72) and the existence of a positive autarky extension.
TAOCP 7.2.2.2 Exercise 167
We seek all integers $n < 10^9$ such that the equation $x_1 + x_2 + \cdots + x_n = x_1 x_2 \cdots x_n$ has exactly one solution in positive integers satisfying $x_1 \ge x_2 \ge \cdots \ge x_n$.
TAOCP 7.2.2.2 Exercise 168
Let $F$ be the clause set at step L3, and let Algorithm X have produced heuristic scores $H(l)$ for every literal $l$ based on step L2.
TAOCP 7.2.2.2 Exercise 169
Working
TAOCP 7.2.2.2 Exercise 170
Let $F$ be a 2CNF formula with variables $x_1,\ldots,x_n$ and clauses $C_1,\ldots,C_m$, where each clause has the form $(l \lor l')$ with literals $l,l'$.
TAOCP 7.2.2.2 Exercise 171
In Algorithm Y, `DFAIL` is the mechanism that records the failure of a descendant search so that the algorithm does not repeat the same unsuccessful computation after backtracking.
TAOCP 7.2.2.2 Exercise 172
In Algorithm Y, the quantity $BT$ in step Y2 measures the net effect on the heuristic score when a literal is chosen as a branch variable.
TAOCP 7.2.2.2 Exercise 173
Let $F = rand(3, 2062, 500, 314)$ be a random 3SAT instance with $n = 2062$ variables and $m = 500$ clauses.
TAOCP 7.2.2.2 Exercise 174
In Algorithm L, “double lookahead” refers to extending the usual one-step lookahead by performing a second conditional simulation after the first tentative assignment, thereby building a two-level loo...
TAOCP 7.2.2.2 Exercise 175
Algorithm L maintains a CNF instance as a family of clauses $F$, together with a partial assignment represented implicitly by forced literals produced during propagation.
TAOCP 7.2.2.2 Exercise 176
The labeling given in the proposed solution is correct and we retain it: a_j = t_jt_{j+1},\quad b_j = t_ju_j,\quad c_j = u_jv_j,\quad d_j = u_jw_j, e_j = v_jw_{j+1},\quad f_j = w_jv_{j-1},\qquad 1\le...
TAOCP 7.2.2.2 Exercise 177
The previous solution fails not because the transfer-matrix idea is invalid, but because it never actually constructs the underlying combinatorial object it depends on.
TAOCP 7.2.2.2 Exercise 178
The previous solution failed because it introduced an undefined “gadget decomposition” and an undefined parameter $b$, and then used them as if they were part of the formal structure of $fsnark(q)$.
TAOCP 7.2.2.2 Exercise 179
We seek all integers $n < 10^9$ such that the equation $x_1 + x_2 + \cdots + x_n = x_1 x_2 \cdots x_n$ has exactly one solution in positive integers satisfying $x_1 \ge x_2 \ge \cdots \ge x_n$.
TAOCP 7.2.2.2 Exercise 180
We seek all integers $n < 10^9$ such that the equation $x_1 + x_2 + \cdots + x_n = x_1 x_2 \cdots x_n$ has exactly one solution in positive integers satisfying $x_1 \ge x_2 \ge \cdots \ge x_n$.
TAOCP 7.2.2.2 Exercise 181
We seek all integers $n < 10^9$ such that the equation $x_1 + x_2 + \cdots + x_n = x_1 x_2 \cdots x_n$ has exactly one solution in positive integers satisfying $x_1 \ge x_2 \ge \cdots \ge x_n$.
TAOCP 7.2.2.2 Exercise 182
We seek all integers $n < 10^9$ such that the equation $x_1 + x_2 + \cdots + x_n = x_1 x_2 \cdots x_n$ has exactly one solution in positive integers satisfying $x_1 \ge x_2 \ge \cdots \ge x_n$.
TAOCP 7.2.2.2 Exercise 183
The key mistake in the proposed solution is treating Fig.
TAOCP 7.2.2.2 Exercise 184
The flaw in the previous solution is that it treats the relation as a generic probabilistic decomposition without aligning precisely with Knuth’s definitions of $q_m$ and $\hat{q}_m$, and it does not...
TAOCP 7.2.2.2 Exercise 185
Equation (77) expresses $\hat{q}_m$ in terms of a decomposition of the same underlying combinatorial objects that define $q_m$, but without the restriction that enforces the stricter admissibility con...