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