Post a distinct-linear constraint on variables \a x with sum \a c
| 489 | } |
| 490 | /// Post a distinct-linear constraint on variables \a x with sum \a c |
| 491 | void distinctlinear(Cache& dc, const IntVarArgs& x, int c, |
| 492 | const SizeOptions& opt) { |
| 493 | int n=x.size(); |
| 494 | if (opt.model() == MODEL_DECOMPOSE) { |
| 495 | if (n < 8) |
| 496 | linear(*this, x, IRT_EQ, c, opt.ipl()); |
| 497 | else if (n == 8) |
| 498 | rel(*this, x, IRT_NQ, 9*(9+1)/2 - c); |
| 499 | distinct(*this, x, opt.ipl()); |
| 500 | } else { |
| 501 | switch (n) { |
| 502 | case 0: |
| 503 | return; |
| 504 | case 1: |
| 505 | rel(*this, x[0], IRT_EQ, c); |
| 506 | return; |
| 507 | case 8: |
| 508 | // Prune the single missing digit |
| 509 | rel(*this, x, IRT_NQ, 9*(9+1)/2 - c); |
| 510 | break; |
| 511 | case 9: |
| 512 | break; |
| 513 | default: |
| 514 | if (c == n*(n+1)/2) { |
| 515 | // sum has unique decomposition: 1 + ... + n |
| 516 | rel(*this, x, IRT_LQ, n); |
| 517 | } else if (c == n*(n+1)/2 + 1) { |
| 518 | // sum has unique decomposition: 1 + ... + n-1 + n+1 |
| 519 | rel(*this, x, IRT_LQ, n+1); |
| 520 | rel(*this, x, IRT_NQ, n); |
| 521 | } else if (c == 9*(9+1)/2 - (9-n)*(9-n+1)/2) { |
| 522 | // sum has unique decomposition: (9-n+1) + (9-n+2) + ... + 9 |
| 523 | rel(*this, x, IRT_GQ, 9-n+1); |
| 524 | } else if (c == 9*(9+1)/2 - (9-n)*(9-n+1)/2 + 1) { |
| 525 | // sum has unique decomposition: (9-n) + (9-n+2) + ... + 9 |
| 526 | rel(*this, x, IRT_GQ, 9-n); |
| 527 | rel(*this, x, IRT_NQ, 9-n+1); |
| 528 | } else { |
| 529 | extensional(*this, x, dc.get(n,c)); |
| 530 | return; |
| 531 | } |
| 532 | } |
| 533 | distinct(*this, x, opt.ipl()); |
| 534 | } |
| 535 | } |
| 536 | /// The actual problem |
| 537 | Kakuro(const SizeOptions& opt) |
| 538 | : Script(opt), |