00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024
00025
00026
00027
00028
00029
00030
00031
00032
00033
00034 #include <gecode/driver.hh>
00035 #include <gecode/int.hh>
00036 #include <gecode/minimodel.hh>
00037
00038 #include <fstream>
00039
00040 using namespace Gecode;
00041
00046 class ColoredMatrixOptions : public Options {
00047 private:
00049 Driver::UnsignedIntOption _height;
00051 Driver::UnsignedIntOption _width;
00053 Driver::UnsignedIntOption _size;
00055 Driver::UnsignedIntOption _colors;
00057 Driver::StringOption _not_all_equal;
00059 Driver::StringOption _same_or_0;
00061 Driver::StringOption _distinct_except_0;
00063 Driver::StringOption _no_monochrome_rectangle;
00064
00065 public:
00067 ColoredMatrixOptions(const char* n);
00068
00070 void parse(int& argc, char* argv[]) {
00071 Options::parse(argc,argv);
00072 }
00073
00075 unsigned int height(void) const {
00076 if (_size.value() == 0)
00077 return _height.value();
00078 else
00079 return _size.value();
00080 }
00082 unsigned int width(void) const {
00083 if (_size.value() == 0)
00084 return _width.value();
00085 else
00086 return _size.value();
00087 }
00089 unsigned int colors(void) const { return _colors.value(); }
00091 int not_all_equal(void) const { return _not_all_equal.value(); }
00093 int same_or_0(void) const { return _same_or_0.value(); }
00095 int distinct_except_0(void) const { return _distinct_except_0.value(); }
00097 int no_monochrome_rectangle(void) const {
00098 return _no_monochrome_rectangle.value();
00099 }
00100 };
00101
00102 namespace {
00111
00118 DFA same_or_0_dfa(unsigned int colors);
00119
00126 TupleSet same_or_0_tuple_set(unsigned int colors);
00127
00130 DFA distinct_except_0_dfa(unsigned int colors);
00131
00134 DFA no_monochrome_rectangle_dfa(unsigned int colors);
00135
00138 IntSetArgs distinct_except_0_counts(unsigned int colors, unsigned int size);
00139
00142 DFA not_all_equal_dfa(unsigned int colors);
00143
00145 }
00146
00164 class ColoredMatrix : public IntMinimizeScript {
00165 protected:
00169 const ColoredMatrixOptions& opt;
00170 const unsigned int height;
00171 const unsigned int width;
00172 const unsigned int colors;
00173
00174
00178
00179 IntVarArray x;
00181 IntVar max_color;
00183
00186 IntVar same_or_0(const IntVar& a, const IntVar& b)
00187 {
00188 switch (opt.same_or_0()) {
00189 case SAME_OR_0_REIFIED: {
00190 IntVar result(*this, 0, colors);
00191 BoolVar same = expr(*this, (a == b));
00192 rel(*this, result, IRT_EQ, a, same);
00193
00194 rel(*this, result, IRT_NQ, 0, same);
00195 return result;
00196 }
00197 case SAME_OR_0_TUPLE_SET: {
00198 static TupleSet table = same_or_0_tuple_set(colors);
00199 IntVar result(*this, 0, colors);
00200 extensional(*this, IntVarArgs() << a << b << result, table);
00201 return result;
00202 }
00203 case SAME_OR_0_DFA: {
00204 static const DFA automaton = same_or_0_dfa(colors);
00205 IntVar result(*this, 0, colors);
00206 extensional(*this, IntVarArgs() << a << b << result, automaton);
00207 return result;
00208 }
00209 default:
00210 GECODE_NEVER;
00211 return IntVar(*this, 0, 0);
00212 }
00213 }
00214
00217 void distinct_except_0(const IntVarArgs& v)
00218 {
00219 switch (opt.distinct_except_0()) {
00220 case DISTINCT_EXCEPT_0_REIFIED:
00221 for (int i = v.size(); i--; ) {
00222 BoolVar viIsZero = expr(*this, v[i] == 0);
00223 for (int j = i; j--; ) {
00224 rel(*this, viIsZero || (v[i] != v[j]));
00225 }
00226 }
00227 break;
00228 case DISTINCT_EXCEPT_0_DFA: {
00229 static const DFA automaton = distinct_except_0_dfa(colors);
00230 extensional(*this, v, automaton);
00231 break;
00232 }
00233 case DISTINCT_EXCEPT_0_COUNT: {
00234 static const IntSetArgs counts = distinct_except_0_counts(colors, std::max(width, height));
00235 count(*this, v, counts, opt.ipl());
00236 break;
00237 }
00238 }
00239 }
00240
00243 void not_all_equal(const IntVarArgs& v)
00244 {
00245 switch (opt.not_all_equal()) {
00246 case NOT_ALL_EQUAL_NQ: {
00247 rel(*this, v, IRT_NQ);
00248 break;
00249 }
00250 case NOT_ALL_EQUAL_NAIVE: {
00251
00252
00253 BoolVarArgs disequalities;
00254 for (int i = v.size(); i--; )
00255 for (int j = i; j--; )
00256 disequalities << expr(*this, v[i] != v[j]);
00257 rel(*this, BOT_OR, disequalities, 1);
00258 break;
00259 }
00260 case NOT_ALL_EQUAL_REIFIED: {
00261
00262 BoolVarArgs equalities;
00263 for (int i = 0; i < v.size()-1; ++i)
00264 equalities << expr(*this, v[i] == v[i+1]);
00265 rel(*this, BOT_AND, equalities, 0);
00266 break;
00267 }
00268 case NOT_ALL_EQUAL_NVALUES:
00269
00270 nvalues(*this, v, IRT_GR, 1);
00271 break;
00272 case NOT_ALL_EQUAL_COUNT:
00273
00274 count(*this, v, IntSet(0, v.size()-1), IntArgs::create(colors, 1), opt.ipl());
00275 break;
00276 case NOT_ALL_EQUAL_DFA: {
00277 static const DFA automaton = not_all_equal_dfa(colors);
00278 extensional(*this, v, automaton);
00279 break;
00280 }
00281 }
00282 }
00283
00287 void no_monochrome_rectangle(IntVarArgs v1, IntVarArgs v2) {
00288 const unsigned int length = v1.size();
00289 switch (opt.no_monochrome_rectangle()) {
00290 case NO_MONOCHROME_DECOMPOSITION: {
00291 IntVarArgs z(length);
00292 for (unsigned int i = 0; i < length; ++i) {
00293 z[i] = same_or_0(v1[i], v2[i]);
00294 }
00295 distinct_except_0(z);
00296 break;
00297 }
00298 case NO_MONOCHROME_DFA: {
00299 static const DFA automaton = no_monochrome_rectangle_dfa(colors);
00300 IntVarArgs z(2*length);
00301 for (int i = length; i--; ) {
00302 z[2*i + 0] = v1[i];
00303 z[2*i + 1] = v2[i];
00304 }
00305 extensional(*this, z, automaton);
00306 break;
00307 }
00308 }
00309 }
00310
00311
00312 public:
00314 enum {
00315 SEARCH_DFS,
00316 SEARCH_BAB,
00317 };
00319 enum {
00320 SYMMETRY_NONE = 0,
00321 SYMMETRY_MATRIX = 1,
00322 SYMMETRY_VALUES = 2,
00323 };
00325 enum {
00326 MODEL_CORNERS = 1,
00327 MODEL_ROWS = 2,
00328 MODEL_COLUMNS = 4,
00329 };
00331 enum {
00332 NOT_ALL_EQUAL_NQ,
00333 NOT_ALL_EQUAL_NAIVE,
00334 NOT_ALL_EQUAL_REIFIED,
00335 NOT_ALL_EQUAL_NVALUES,
00336 NOT_ALL_EQUAL_COUNT,
00337 NOT_ALL_EQUAL_DFA,
00338 };
00340 enum {
00341 SAME_OR_0_REIFIED,
00342 SAME_OR_0_DFA,
00343 SAME_OR_0_TUPLE_SET,
00344 };
00346 enum {
00347 DISTINCT_EXCEPT_0_REIFIED,
00348 DISTINCT_EXCEPT_0_DFA,
00349 DISTINCT_EXCEPT_0_COUNT,
00350 };
00352 enum {
00353 NO_MONOCHROME_DECOMPOSITION,
00354 NO_MONOCHROME_DFA,
00355 };
00356
00357
00359 ColoredMatrix(const ColoredMatrixOptions& opt0)
00360 : IntMinimizeScript(opt0),
00361 opt(opt0), height(opt.height()), width(opt.width()), colors(opt.colors()),
00362 x(*this, height*width, 1, colors),
00363 max_color(*this, 1, colors)
00364 {
00365
00366 max(*this, x, max_color);
00367
00368 Matrix<IntVarArray> m(x, width, height);
00369
00370
00371 if (opt.model() & MODEL_CORNERS) {
00372 for (unsigned int c1 = 0; c1 < width; ++c1) {
00373 for (unsigned int c2 = c1+1; c2 < width; ++c2) {
00374 for (unsigned int r1 = 0; r1 < height; ++r1) {
00375 for (unsigned int r2 = r1+1; r2 < height; ++r2) {
00376 not_all_equal(IntVarArgs() << m(c1,r1) << m(c1,r2) << m(c2,r1) << m(c2,r2));
00377 }
00378 }
00379 }
00380 }
00381 }
00382
00383
00384
00385
00386 if (opt.model() & MODEL_ROWS) {
00387 for (unsigned int r1 = 0; r1 < height; ++r1) {
00388 for (unsigned int r2 = r1+1; r2 < height; ++r2) {
00389 no_monochrome_rectangle(m.row(r1), m.row(r2));
00390 }
00391 }
00392 }
00393 if (opt.model() & MODEL_COLUMNS) {
00394 for (unsigned int c1 = 0; c1 < width; ++c1) {
00395 for (unsigned int c2 = c1+1; c2 < width; ++c2) {
00396 no_monochrome_rectangle(m.col(c1), m.col(c2));
00397 }
00398 }
00399 }
00400
00401
00402 {
00403
00404 if (opt.symmetry() & SYMMETRY_MATRIX) {
00405 for (unsigned int r = 0; r < height-1; ++r) {
00406 rel(*this, m.row(r), IRT_LE, m.row(r+1));
00407 }
00408 for (unsigned int c = 0; c < width-1; ++c) {
00409 rel(*this, m.col(c), IRT_LE, m.col(c+1));
00410 }
00411 }
00412
00413
00414 if (opt.symmetry() & SYMMETRY_VALUES) {
00415 precede(*this, x, IntArgs::create(colors, 1));
00416 }
00417 }
00418
00419 branch(*this, x, tiebreak(INT_VAR_MIN_MIN(), INT_VAR_SIZE_MIN()), INT_VAL_MIN());
00420 }
00421
00423 virtual IntVar cost(void) const {
00424 return max_color;
00425 }
00426
00428 virtual void
00429 print(std::ostream& os) const {
00430 Matrix<IntVarArray> m(x, width, height);
00431 for (unsigned int r = 0; r < height; ++r) {
00432 os << "\t";
00433 for (unsigned int c = 0; c < width; ++c) {
00434 os << m(c, r) << " ";
00435 }
00436 os << std::endl;
00437 }
00438 os << std::endl;
00439 os << "\tmax color: " << max_color << std::endl;
00440 os << std::endl;
00441 }
00442
00444 ColoredMatrix(ColoredMatrix& s)
00445 : IntMinimizeScript(s), opt(s.opt),
00446 height(s.height), width(s.width), colors(s.colors) {
00447 x.update(*this, s.x);
00448 max_color.update(*this, s.max_color);
00449 }
00451 virtual Space*
00452 copy(void) {
00453 return new ColoredMatrix(*this);
00454 }
00455 };
00456
00457 ColoredMatrixOptions::ColoredMatrixOptions(const char* n)
00458 : Options(n),
00459 _height("height", "Height of matrix", 8),
00460 _width("width", "Width of matrix", 8),
00461 _size("size", "If different from 0, used as both width and height", 0),
00462 _colors("colors", "Maximum number of colors", 4),
00463 _not_all_equal("not-all-equal", "How to implement the not all equals constraint (used in corners model)",
00464 ColoredMatrix::NOT_ALL_EQUAL_NQ),
00465 _same_or_0("same-or-0", "How to implement the same or 0 constraint (used in the decomposed no monochrome rectangle constraint)",
00466 ColoredMatrix::SAME_OR_0_DFA),
00467 _distinct_except_0("distinct-except-0", "How to implement the distinct except 0 constraint (used in the decomposed no monochrome rectangle constraint)",
00468 ColoredMatrix::DISTINCT_EXCEPT_0_DFA),
00469 _no_monochrome_rectangle("no-monochrome-rectangle", "How to implement no monochrome rectangle (used in the rows model)",
00470 ColoredMatrix::NO_MONOCHROME_DFA)
00471 {
00472 add(_height);
00473 add(_width);
00474 add(_size);
00475 add(_colors);
00476 add(_not_all_equal);
00477 add(_same_or_0);
00478 add(_distinct_except_0);
00479 add(_no_monochrome_rectangle);
00480
00481
00482 _search.add(ColoredMatrix::SEARCH_DFS, "dfs", "Find a solution.");
00483 _search.add(ColoredMatrix::SEARCH_BAB, "bab", "Find an optimal solution.");
00484 _search.value(ColoredMatrix::SEARCH_DFS);
00485
00486
00487 _symmetry.add(ColoredMatrix::SYMMETRY_NONE, "none", "Don't use symmetry breaking.");
00488 _symmetry.add(ColoredMatrix::SYMMETRY_MATRIX, "matrix", "Order matrix rows and columns");
00489 _symmetry.add(ColoredMatrix::SYMMETRY_VALUES, "values", "Order values");
00490 _symmetry.add(ColoredMatrix::SYMMETRY_MATRIX | ColoredMatrix::SYMMETRY_VALUES,
00491 "both", "Order both rows/columns and values");
00492 _symmetry.value(ColoredMatrix::SYMMETRY_MATRIX);
00493
00494
00495 _model.add(ColoredMatrix::MODEL_CORNERS, "corner", "Use direct corners model with not-all-equal constraints.");
00496 _model.add(ColoredMatrix::MODEL_ROWS, "rows", "Use model on pairs of rows (same_or_0 and distinct_except_0 constraints).");
00497 _model.add(ColoredMatrix::MODEL_ROWS | ColoredMatrix::MODEL_CORNERS,
00498 "both", "Use both rows and corners model");
00499 _model.add(ColoredMatrix::MODEL_COLUMNS, "columns", "Use model on pairs of columns (same_or_0 and distinct_except_0 constraints).");
00500 _model.add(ColoredMatrix::MODEL_ROWS | ColoredMatrix::MODEL_COLUMNS,
00501 "matrix", "Use both rows and columns model");
00502 _model.value(ColoredMatrix::MODEL_CORNERS);
00503
00504
00505 _not_all_equal.add(ColoredMatrix::NOT_ALL_EQUAL_NQ, "nq", "Use nq constraint.");
00506 _not_all_equal.add(ColoredMatrix::NOT_ALL_EQUAL_NAIVE, "naive", "Use naive reified decomposition.");
00507 _not_all_equal.add(ColoredMatrix::NOT_ALL_EQUAL_REIFIED, "reified", "Use reified decomposition.");
00508 _not_all_equal.add(ColoredMatrix::NOT_ALL_EQUAL_NVALUES, "nvalues", "Use nvalues.");
00509 _not_all_equal.add(ColoredMatrix::NOT_ALL_EQUAL_COUNT, "count", "Use count.");
00510 _not_all_equal.add(ColoredMatrix::NOT_ALL_EQUAL_DFA, "dfa", "Use dfa.");
00511
00512
00513 _same_or_0.add(ColoredMatrix::SAME_OR_0_REIFIED, "reified", "Use reified decomposition.");
00514 _same_or_0.add(ColoredMatrix::SAME_OR_0_TUPLE_SET, "tuple-set", "Use tuple set representation.");
00515 _same_or_0.add(ColoredMatrix::SAME_OR_0_DFA, "dfa", "Use dfa representation.");
00516
00517
00518 _distinct_except_0.add(ColoredMatrix::DISTINCT_EXCEPT_0_REIFIED, "reified", "Use reified decomposition.");
00519 _distinct_except_0.add(ColoredMatrix::DISTINCT_EXCEPT_0_DFA, "dfa", "Use dfa decomposition.");
00520 _distinct_except_0.add(ColoredMatrix::DISTINCT_EXCEPT_0_COUNT, "count", "Use global cardinality.");
00521
00522
00523 _no_monochrome_rectangle.add(ColoredMatrix::NO_MONOCHROME_DECOMPOSITION,
00524 "decompositions",
00525 "Use decompositions into same_or_0 and distinct_except_0.");
00526 _no_monochrome_rectangle.add(ColoredMatrix::NO_MONOCHROME_DFA,
00527 "dfa",
00528 "Use DFA as direct implementation.");
00529 }
00530
00534 int
00535 main(int argc, char* argv[]) {
00536 ColoredMatrixOptions opt("Colored matrix");
00537 opt.parse(argc,argv);
00538 if (opt.search() == ColoredMatrix::SEARCH_DFS) {
00539 Script::run<ColoredMatrix,DFS,ColoredMatrixOptions>(opt);
00540 } else {
00541 Script::run<ColoredMatrix,BAB,ColoredMatrixOptions>(opt);
00542 }
00543 return 0;
00544 }
00545
00546
00547 namespace {
00548 DFA same_or_0_dfa(unsigned int colors)
00549 {
00550
00551
00552
00553
00554
00555
00556
00557
00558
00559
00560
00561
00562
00563 const int start_state = 0;
00564 const int not_equal_state = 2*colors+1;
00565 const int final_state = 2*colors+2;
00566
00567 int n_transitions = colors*colors + 2*colors + 2;
00568 DFA::Transition* trans = new DFA::Transition[n_transitions];
00569 int current_transition = 0;
00570
00571
00572 for (unsigned int color = 1; color <= colors; ++color) {
00573 trans[current_transition++] =
00574 DFA::Transition(start_state, color, color);
00575 }
00576
00577
00578
00579 for (unsigned int state = 1; state <= colors; ++state) {
00580 for (unsigned int color = 1; color <= colors; ++color) {
00581 if (color == state) {
00582 trans[current_transition++] =
00583 DFA::Transition(state, color, colors+state);
00584 } else {
00585 trans[current_transition++] =
00586 DFA::Transition(state, color, not_equal_state);
00587 }
00588 }
00589 }
00590
00591
00592
00593 for (unsigned int color = 1; color <= colors; ++color) {
00594 trans[current_transition++] =
00595 DFA::Transition(colors+color, color, final_state);
00596 }
00597
00598
00599 trans[current_transition++] =
00600 DFA::Transition(not_equal_state, 0, final_state);
00601
00602
00603 trans[current_transition++] =
00604 DFA::Transition(-1, 0, -1);
00605
00606 int final_states[] = {final_state, -1};
00607
00608 DFA result(start_state, trans, final_states, true);
00609
00610 delete[] trans;
00611
00612 return result;
00613 }
00614
00615 TupleSet same_or_0_tuple_set(unsigned int colors) {
00616 TupleSet result(3);
00617 for (unsigned int i = 1; i <= colors; ++i) {
00618 for (unsigned int j = 1; j <= colors; ++j) {
00619 if (i == j) {
00620 result.add(i, j, i);
00621 } else {
00622 result.add(i, j, 0);
00623 }
00624 }
00625 }
00626 result.finalize();
00627 return result;
00628 }
00629
00630 DFA distinct_except_0_dfa(unsigned int colors)
00631 {
00632
00633
00634
00635
00636
00637
00638
00639
00640
00641 const int nstates = 1 << colors;
00642 const int start_state = nstates-1;
00643
00644 DFA::Transition* trans = new DFA::Transition[nstates*colors + 1];
00645 int current_transition = 0;
00646
00647 for (int state = nstates; state--; ) {
00648 trans[current_transition++] = DFA::Transition(state, 0, state);
00649
00650 for (unsigned int color = 1; color <= colors; ++color) {
00651 const unsigned int color_bit = (1 << (color-1));
00652 if (state & color_bit) {
00653 trans[current_transition++] =
00654 DFA::Transition(state, color, state & ~color_bit);
00655 }
00656 }
00657 }
00658 trans[current_transition++] = DFA::Transition(-1, 0, -1);
00659
00660 int* final_states = new int[nstates+1];
00661 final_states[nstates] = -1;
00662 for (int i = nstates; i--; ) {
00663 final_states[i] = i;
00664 }
00665
00666 DFA result(start_state, trans, final_states);
00667
00668 delete[] trans;
00669 delete[] final_states;
00670
00671 return result;
00672 }
00673
00674 DFA no_monochrome_rectangle_dfa(unsigned int colors)
00675 {
00676
00677
00678
00679
00680
00681
00682
00683
00684
00685
00686
00687
00688
00689
00690 const int base_states = 1 << colors;
00691 const int start_state = base_states-1;
00692 const int nstates = base_states + colors*base_states;
00693
00694 DFA::Transition* trans = new DFA::Transition[nstates*colors + 1];
00695 int current_transition = 0;
00696
00697 for (int state = base_states; state--; ) {
00698 for (unsigned int color = 1; color <= colors; ++color) {
00699 const unsigned int color_bit = (1 << (color-1));
00700 const int color_remembered_state = state + color*base_states;
00701
00702 trans[current_transition++] =
00703 DFA::Transition(state, color, color_remembered_state);
00704
00705 for (unsigned int next_color = 1; next_color <= colors; ++next_color) {
00706 if (next_color == color) {
00707
00708 if (state & color_bit) {
00709 trans[current_transition++] =
00710 DFA::Transition(color_remembered_state, color, state & ~color_bit);
00711 }
00712 } else {
00713 trans[current_transition++] =
00714 DFA::Transition(color_remembered_state, next_color, state);
00715 }
00716 }
00717 }
00718 }
00719 trans[current_transition++] = DFA::Transition(-1, 0, -1);
00720 assert(current_transition <= nstates*colors+1);
00721
00722 int* final_states = new int[base_states+1];
00723 final_states[base_states] = -1;
00724 for (int i = base_states; i--; ) {
00725 final_states[i] = i;
00726 }
00727
00728 DFA result(start_state, trans, final_states);
00729
00730 delete[] trans;
00731 delete[] final_states;
00732
00733 return result;
00734 }
00735
00736 IntSetArgs distinct_except_0_counts(unsigned int colors, unsigned int size)
00737 {
00738 IntSetArgs result(colors+1);
00739
00740 result[0] = IntSet(0, size);
00741
00742 for (unsigned int i = 1; i <= colors; ++i) {
00743 result[i] = IntSet(0, 1);
00744 }
00745
00746 return result;
00747 }
00748
00749
00750 DFA not_all_equal_dfa(unsigned int colors)
00751 {
00752
00753
00754
00755
00756
00757
00758
00759
00760 const int nstates = 1 + colors + 1;
00761 const int start_state = 0;
00762 const int final_state = nstates-1;
00763
00764 DFA::Transition* trans = new DFA::Transition[2*colors + colors*colors + 1];
00765 int current_transition = 0;
00766
00767
00768 for (unsigned int color = 1; color <= colors; ++color) {
00769 trans[current_transition++] = DFA::Transition(start_state, color, color);
00770 }
00771
00772
00773 for (unsigned int state = 1; state <= colors; ++state) {
00774 for (unsigned int color = 1; color <= colors; ++color) {
00775 if (state == color) {
00776 trans[current_transition++] = DFA::Transition(state, color, state);
00777 } else {
00778 trans[current_transition++] = DFA::Transition(state, color, final_state);
00779 }
00780 }
00781 }
00782
00783
00784 for (unsigned int color = 1; color <= colors; ++color) {
00785 trans[current_transition++] = DFA::Transition(final_state, color, final_state);
00786 }
00787
00788 trans[current_transition++] = DFA::Transition(-1, 0, -1);
00789
00790 int final_states[] = {final_state, -1};
00791
00792 DFA result(start_state, trans, final_states);
00793
00794 delete[] trans;
00795
00796 return result;
00797 }
00798
00799 }
00800
00801
00802