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.ipl());
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.ipl());
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 : IntMinimizeScript(opt0),
00365 opt(opt0), height(opt.height()), width(opt.width()), colors(opt.colors()),
00366 x(*this, height*width, 1, colors),
00367 max_color(*this, 1, colors)
00368 {
00369
00370 max(*this, x, max_color);
00371
00372 Matrix<IntVarArray> m(x, width, height);
00373
00374
00375 if (opt.model() & MODEL_CORNERS) {
00376 for (unsigned int c1 = 0; c1 < width; ++c1) {
00377 for (unsigned int c2 = c1+1; c2 < width; ++c2) {
00378 for (unsigned int r1 = 0; r1 < height; ++r1) {
00379 for (unsigned int r2 = r1+1; r2 < height; ++r2) {
00380 not_all_equal(IntVarArgs() << m(c1,r1) << m(c1,r2) << m(c2,r1) << m(c2,r2));
00381 }
00382 }
00383 }
00384 }
00385 }
00386
00387
00388
00389
00390 if (opt.model() & MODEL_ROWS) {
00391 for (unsigned int r1 = 0; r1 < height; ++r1) {
00392 for (unsigned int r2 = r1+1; r2 < height; ++r2) {
00393 no_monochrome_rectangle(m.row(r1), m.row(r2));
00394 }
00395 }
00396 }
00397 if (opt.model() & MODEL_COLUMNS) {
00398 for (unsigned int c1 = 0; c1 < width; ++c1) {
00399 for (unsigned int c2 = c1+1; c2 < width; ++c2) {
00400 no_monochrome_rectangle(m.col(c1), m.col(c2));
00401 }
00402 }
00403 }
00404
00405
00406 {
00407
00408 if (opt.symmetry() & SYMMETRY_MATRIX) {
00409 for (unsigned int r = 0; r < height-1; ++r) {
00410 rel(*this, m.row(r), IRT_LE, m.row(r+1));
00411 }
00412 for (unsigned int c = 0; c < width-1; ++c) {
00413 rel(*this, m.col(c), IRT_LE, m.col(c+1));
00414 }
00415 }
00416
00417
00418 if (opt.symmetry() & SYMMETRY_VALUES) {
00419 precede(*this, x, IntArgs::create(colors, 1));
00420 }
00421 }
00422
00423 branch(*this, x, tiebreak(INT_VAR_MIN_MIN(), INT_VAR_SIZE_MIN()), INT_VAL_MIN());
00424 }
00425
00427 virtual IntVar cost(void) const {
00428 return max_color;
00429 }
00430
00432 virtual void
00433 print(std::ostream& os) const {
00434 Matrix<IntVarArray> m(x, width, height);
00435 for (unsigned int r = 0; r < height; ++r) {
00436 os << "\t";
00437 for (unsigned int c = 0; c < width; ++c) {
00438 os << m(c, r) << " ";
00439 }
00440 os << std::endl;
00441 }
00442 os << std::endl;
00443 os << "\tmax color: " << max_color << std::endl;
00444 os << std::endl;
00445 }
00446
00448 ColoredMatrix(bool share, ColoredMatrix& s)
00449 : IntMinimizeScript(share,s), opt(s.opt),
00450 height(s.height), width(s.width), colors(s.colors) {
00451 x.update(*this, share, s.x);
00452 max_color.update(*this, share, s.max_color);
00453 }
00455 virtual Space*
00456 copy(bool share) {
00457 return new ColoredMatrix(share,*this);
00458 }
00459 };
00460
00461 ColoredMatrixOptions::ColoredMatrixOptions(const char* n)
00462 : Options(n),
00463 _height("-height", "Height of matrix", 8),
00464 _width("-width", "Width of matrix", 8),
00465 _size("-size", "If different from 0, used as both width and height", 0),
00466 _colors("-colors", "Maximum number of colors", 4),
00467 _not_all_equal("-not-all-equal", "How to implement the not all equals constraint (used in corners model)",
00468 ColoredMatrix::NOT_ALL_EQUAL_NQ),
00469 _same_or_0("-same-or-0", "How to implement the same or 0 constraint (used in the decomposed no monochrome rectangle constraint)",
00470 ColoredMatrix::SAME_OR_0_DFA),
00471 _distinct_except_0("-distinct-except-0", "How to implement the distinct except 0 constraint (used in the decomposed no monochrome rectangle constraint)",
00472 ColoredMatrix::DISTINCT_EXCEPT_0_DFA),
00473 _no_monochrome_rectangle("-no-monochrome-rectangle", "How to implement no monochrome rectangle (used in the rows model)",
00474 ColoredMatrix::NO_MONOCHROME_DFA)
00475 {
00476 add(_height);
00477 add(_width);
00478 add(_size);
00479 add(_colors);
00480 add(_not_all_equal);
00481 add(_same_or_0);
00482 add(_distinct_except_0);
00483 add(_no_monochrome_rectangle);
00484
00485
00486 _search.add(ColoredMatrix::SEARCH_DFS, "dfs", "Find a solution.");
00487 _search.add(ColoredMatrix::SEARCH_BAB, "bab", "Find an optimal solution.");
00488 _search.value(ColoredMatrix::SEARCH_DFS);
00489
00490
00491 _symmetry.add(ColoredMatrix::SYMMETRY_NONE, "none", "Don't use symmetry breaking.");
00492 _symmetry.add(ColoredMatrix::SYMMETRY_MATRIX, "matrix", "Order matrix rows and columns");
00493 _symmetry.add(ColoredMatrix::SYMMETRY_VALUES, "values", "Order values");
00494 _symmetry.add(ColoredMatrix::SYMMETRY_MATRIX | ColoredMatrix::SYMMETRY_VALUES,
00495 "both", "Order both rows/columns and values");
00496 _symmetry.value(ColoredMatrix::SYMMETRY_MATRIX);
00497
00498
00499 _model.add(ColoredMatrix::MODEL_CORNERS, "corner", "Use direct corners model with not-all-equal constraints.");
00500 _model.add(ColoredMatrix::MODEL_ROWS, "rows", "Use model on pairs of rows (same_or_0 and distinct_except_0 constraints).");
00501 _model.add(ColoredMatrix::MODEL_ROWS | ColoredMatrix::MODEL_CORNERS,
00502 "both", "Use both rows and corners model");
00503 _model.add(ColoredMatrix::MODEL_COLUMNS, "columns", "Use model on pairs of columns (same_or_0 and distinct_except_0 constraints).");
00504 _model.add(ColoredMatrix::MODEL_ROWS | ColoredMatrix::MODEL_COLUMNS,
00505 "matrix", "Use both rows and columns model");
00506 _model.value(ColoredMatrix::MODEL_CORNERS);
00507
00508
00509 _not_all_equal.add(ColoredMatrix::NOT_ALL_EQUAL_NQ, "nq", "Use nq constraint.");
00510 _not_all_equal.add(ColoredMatrix::NOT_ALL_EQUAL_NAIVE, "naive", "Use naive reified decomposition.");
00511 _not_all_equal.add(ColoredMatrix::NOT_ALL_EQUAL_REIFIED, "reified", "Use reified decomposition.");
00512 _not_all_equal.add(ColoredMatrix::NOT_ALL_EQUAL_NVALUES, "nvalues", "Use nvalues.");
00513 _not_all_equal.add(ColoredMatrix::NOT_ALL_EQUAL_COUNT, "count", "Use count.");
00514 _not_all_equal.add(ColoredMatrix::NOT_ALL_EQUAL_DFA, "dfa", "Use dfa.");
00515
00516
00517 _same_or_0.add(ColoredMatrix::SAME_OR_0_REIFIED, "reified", "Use reified decomposition.");
00518 _same_or_0.add(ColoredMatrix::SAME_OR_0_TUPLE_SET, "tuple-set", "Use tuple set representation.");
00519 _same_or_0.add(ColoredMatrix::SAME_OR_0_DFA, "dfa", "Use dfa representation.");
00520
00521
00522 _distinct_except_0.add(ColoredMatrix::DISTINCT_EXCEPT_0_REIFIED, "reified", "Use reified decomposition.");
00523 _distinct_except_0.add(ColoredMatrix::DISTINCT_EXCEPT_0_DFA, "dfa", "Use dfa decomposition.");
00524 _distinct_except_0.add(ColoredMatrix::DISTINCT_EXCEPT_0_COUNT, "count", "Use global cardinality.");
00525
00526
00527 _no_monochrome_rectangle.add(ColoredMatrix::NO_MONOCHROME_DECOMPOSITION,
00528 "decompositions",
00529 "Use decompositions into same_or_0 and distinct_except_0.");
00530 _no_monochrome_rectangle.add(ColoredMatrix::NO_MONOCHROME_DFA,
00531 "dfa",
00532 "Use DFA as direct implementation.");
00533 }
00534
00538 int
00539 main(int argc, char* argv[]) {
00540 ColoredMatrixOptions opt("Colored matrix");
00541 opt.parse(argc,argv);
00542 if (opt.search() == ColoredMatrix::SEARCH_DFS) {
00543 Script::run<ColoredMatrix,DFS,ColoredMatrixOptions>(opt);
00544 } else {
00545 Script::run<ColoredMatrix,BAB,ColoredMatrixOptions>(opt);
00546 }
00547 return 0;
00548 }
00549
00550
00551 namespace {
00552 DFA same_or_0_dfa(unsigned int colors)
00553 {
00554
00555
00556
00557
00558
00559
00560
00561
00562
00563
00564
00565
00566
00567 const int start_state = 0;
00568 const int not_equal_state = 2*colors+1;
00569 const int final_state = 2*colors+2;
00570
00571 int n_transitions = colors*colors + 2*colors + 2;
00572 DFA::Transition* trans = new DFA::Transition[n_transitions];
00573 int current_transition = 0;
00574
00575
00576 for (unsigned int color = 1; color <= colors; ++color) {
00577 trans[current_transition++] =
00578 DFA::Transition(start_state, color, color);
00579 }
00580
00581
00582
00583 for (unsigned int state = 1; state <= colors; ++state) {
00584 for (unsigned int color = 1; color <= colors; ++color) {
00585 if (color == state) {
00586 trans[current_transition++] =
00587 DFA::Transition(state, color, colors+state);
00588 } else {
00589 trans[current_transition++] =
00590 DFA::Transition(state, color, not_equal_state);
00591 }
00592 }
00593 }
00594
00595
00596
00597 for (unsigned int color = 1; color <= colors; ++color) {
00598 trans[current_transition++] =
00599 DFA::Transition(colors+color, color, final_state);
00600 }
00601
00602
00603 trans[current_transition++] =
00604 DFA::Transition(not_equal_state, 0, final_state);
00605
00606
00607 trans[current_transition++] =
00608 DFA::Transition(-1, 0, -1);
00609
00610 int final_states[] = {final_state, -1};
00611
00612 DFA result(start_state, trans, final_states, true);
00613
00614 delete[] trans;
00615
00616 return result;
00617 }
00618
00619 TupleSet same_or_0_tuple_set(unsigned int colors)
00620 {
00621 TupleSet result;
00622 for (unsigned int i = 1; i <= colors; ++i) {
00623 for (unsigned int j = 1; j <= colors; ++j) {
00624 if (i == j) {
00625 result.add(IntArgs(3, i, j, i));
00626 } else {
00627 result.add(IntArgs(3, i, j, 0));
00628 }
00629 }
00630 }
00631 result.finalize();
00632 return result;
00633 }
00634
00635 DFA distinct_except_0_dfa(unsigned int colors)
00636 {
00637
00638
00639
00640
00641
00642
00643
00644
00645
00646 const int nstates = 1 << colors;
00647 const int start_state = nstates-1;
00648
00649 DFA::Transition* trans = new DFA::Transition[nstates*colors + 1];
00650 int current_transition = 0;
00651
00652 for (int state = nstates; state--; ) {
00653 trans[current_transition++] = DFA::Transition(state, 0, state);
00654
00655 for (unsigned int color = 1; color <= colors; ++color) {
00656 const unsigned int color_bit = (1 << (color-1));
00657 if (state & color_bit) {
00658 trans[current_transition++] =
00659 DFA::Transition(state, color, state & ~color_bit);
00660 }
00661 }
00662 }
00663 trans[current_transition++] = DFA::Transition(-1, 0, -1);
00664
00665 int* final_states = new int[nstates+1];
00666 final_states[nstates] = -1;
00667 for (int i = nstates; i--; ) {
00668 final_states[i] = i;
00669 }
00670
00671 DFA result(start_state, trans, final_states);
00672
00673 delete[] trans;
00674 delete[] final_states;
00675
00676 return result;
00677 }
00678
00679 DFA no_monochrome_rectangle_dfa(unsigned int colors)
00680 {
00681
00682
00683
00684
00685
00686
00687
00688
00689
00690
00691
00692
00693
00694
00695 const int base_states = 1 << colors;
00696 const int start_state = base_states-1;
00697 const int nstates = base_states + colors*base_states;
00698
00699 DFA::Transition* trans = new DFA::Transition[nstates*colors + 1];
00700 int current_transition = 0;
00701
00702 for (int state = base_states; state--; ) {
00703 for (unsigned int color = 1; color <= colors; ++color) {
00704 const unsigned int color_bit = (1 << (color-1));
00705 const int color_remembered_state = state + color*base_states;
00706
00707 trans[current_transition++] =
00708 DFA::Transition(state, color, color_remembered_state);
00709
00710 for (unsigned int next_color = 1; next_color <= colors; ++next_color) {
00711 if (next_color == color) {
00712
00713 if (state & color_bit) {
00714 trans[current_transition++] =
00715 DFA::Transition(color_remembered_state, color, state & ~color_bit);
00716 }
00717 } else {
00718 trans[current_transition++] =
00719 DFA::Transition(color_remembered_state, next_color, state);
00720 }
00721 }
00722 }
00723 }
00724 trans[current_transition++] = DFA::Transition(-1, 0, -1);
00725 assert(current_transition <= nstates*colors+1);
00726
00727 int* final_states = new int[base_states+1];
00728 final_states[base_states] = -1;
00729 for (int i = base_states; i--; ) {
00730 final_states[i] = i;
00731 }
00732
00733 DFA result(start_state, trans, final_states);
00734
00735 delete[] trans;
00736 delete[] final_states;
00737
00738 return result;
00739 }
00740
00741 IntSetArgs distinct_except_0_counts(unsigned int colors, unsigned int size)
00742 {
00743 IntSetArgs result(colors+1);
00744
00745 result[0] = IntSet(0, size);
00746
00747 for (unsigned int i = 1; i <= colors; ++i) {
00748 result[i] = IntSet(0, 1);
00749 }
00750
00751 return result;
00752 }
00753
00754
00755 DFA not_all_equal_dfa(unsigned int colors)
00756 {
00757
00758
00759
00760
00761
00762
00763
00764
00765 const int nstates = 1 + colors + 1;
00766 const int start_state = 0;
00767 const int final_state = nstates-1;
00768
00769 DFA::Transition* trans = new DFA::Transition[2*colors + colors*colors + 1];
00770 int current_transition = 0;
00771
00772
00773 for (unsigned int color = 1; color <= colors; ++color) {
00774 trans[current_transition++] = DFA::Transition(start_state, color, color);
00775 }
00776
00777
00778 for (unsigned int state = 1; state <= colors; ++state) {
00779 for (unsigned int color = 1; color <= colors; ++color) {
00780 if (state == color) {
00781 trans[current_transition++] = DFA::Transition(state, color, state);
00782 } else {
00783 trans[current_transition++] = DFA::Transition(state, color, final_state);
00784 }
00785 }
00786 }
00787
00788
00789 for (unsigned int color = 1; color <= colors; ++color) {
00790 trans[current_transition++] = DFA::Transition(final_state, color, final_state);
00791 }
00792
00793 trans[current_transition++] = DFA::Transition(-1, 0, -1);
00794
00795 int final_states[] = {final_state, -1};
00796
00797 DFA result(start_state, trans, final_states);
00798
00799 delete[] trans;
00800
00801 return result;
00802 }
00803
00804 }
00805
00806
00807