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 int height(void) const {
00076 if (_size.value() == 0U)
00077 return static_cast<int>(_height.value());
00078 else
00079 return static_cast<int>(_size.value());
00080 }
00082 int width(void) const {
00083 if (_size.value() == 0U)
00084 return static_cast<int>(_width.value());
00085 else
00086 return static_cast<int>(_size.value());
00087 }
00089 int colors(void) const { return static_cast<int>(_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(int colors);
00119
00126 TupleSet same_or_0_tuple_set(int colors);
00127
00130 DFA distinct_except_0_dfa(int colors);
00131
00134 DFA no_monochrome_rectangle_dfa(int colors);
00135
00138 IntSetArgs distinct_except_0_counts(int colors, int size);
00139
00142 DFA not_all_equal_dfa(int colors);
00143
00145 }
00146
00164 class ColoredMatrix : public IntMinimizeScript {
00165 protected:
00169 const ColoredMatrixOptions& opt;
00170 const int height;
00171 const int width;
00172 const 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 int length = v1.size();
00289 switch (opt.no_monochrome_rectangle()) {
00290 case NO_MONOCHROME_DECOMPOSITION: {
00291 IntVarArgs z(length);
00292 for (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 (int c1 = 0; c1 < width; ++c1) {
00373 for (int c2 = c1+1; c2 < width; ++c2) {
00374 for (int r1 = 0; r1 < height; ++r1) {
00375 for (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 (int r1 = 0; r1 < height; ++r1) {
00388 for (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 (int c1 = 0; c1 < width; ++c1) {
00395 for (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 (int r = 0; r < height-1; ++r) {
00406 rel(*this, m.row(r), IRT_LE, m.row(r+1));
00407 }
00408 for (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 (int r = 0; r < height; ++r) {
00432 os << "\t";
00433 for (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(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 =
00569 new DFA::Transition[static_cast<size_t>(n_transitions)];
00570 int current_transition = 0;
00571
00572
00573 for (int color = 1; color <= colors; ++color) {
00574 trans[current_transition++] =
00575 DFA::Transition(start_state, color, color);
00576 }
00577
00578
00579
00580 for (int state = 1; state <= colors; ++state) {
00581 for (int color = 1; color <= colors; ++color) {
00582 if (color == state) {
00583 trans[current_transition++] =
00584 DFA::Transition(state, color, colors+state);
00585 } else {
00586 trans[current_transition++] =
00587 DFA::Transition(state, color, not_equal_state);
00588 }
00589 }
00590 }
00591
00592
00593
00594 for (int color = 1; color <= colors; ++color) {
00595 trans[current_transition++] =
00596 DFA::Transition(colors+color, color, final_state);
00597 }
00598
00599
00600 trans[current_transition++] =
00601 DFA::Transition(not_equal_state, 0, final_state);
00602
00603
00604 trans[current_transition++] =
00605 DFA::Transition(-1, 0, -1);
00606
00607 int final_states[] = {final_state, -1};
00608
00609 DFA result(start_state, trans, final_states, true);
00610
00611 delete[] trans;
00612
00613 return result;
00614 }
00615
00616 TupleSet same_or_0_tuple_set(int colors) {
00617 TupleSet result(3);
00618 for (int i = 1; i <= colors; ++i) {
00619 for (int j = 1; j <= colors; ++j) {
00620 if (i == j) {
00621 result.add({i, j, i});
00622 } else {
00623 result.add({i, j, 0});
00624 }
00625 }
00626 }
00627 result.finalize();
00628 return result;
00629 }
00630
00631 DFA distinct_except_0_dfa(int colors)
00632 {
00633
00634
00635
00636
00637
00638
00639
00640
00641
00642 const int nstates = 1 << colors;
00643 const int start_state = nstates-1;
00644
00645 DFA::Transition* trans =
00646 new DFA::Transition[static_cast<size_t>(nstates*colors + 1)];
00647 int current_transition = 0;
00648
00649 for (int state = nstates; state--; ) {
00650 trans[current_transition++] = DFA::Transition(state, 0, state);
00651
00652 for (int color = 1; color <= colors; ++color) {
00653 const int color_bit = (1 << (color-1));
00654 if (state & color_bit) {
00655 trans[current_transition++] =
00656 DFA::Transition(state, color, state & ~color_bit);
00657 }
00658 }
00659 }
00660 trans[current_transition++] = DFA::Transition(-1, 0, -1);
00661
00662 int* final_states = new int[nstates+1];
00663 final_states[nstates] = -1;
00664 for (int i = nstates; i--; ) {
00665 final_states[i] = i;
00666 }
00667
00668 DFA result(start_state, trans, final_states);
00669
00670 delete[] trans;
00671 delete[] final_states;
00672
00673 return result;
00674 }
00675
00676 DFA no_monochrome_rectangle_dfa(int colors)
00677 {
00678
00679
00680
00681
00682
00683
00684
00685
00686
00687
00688
00689
00690
00691
00692 const int base_states = 1 << colors;
00693 const int start_state = base_states-1;
00694 const int nstates = base_states + colors*base_states;
00695
00696 DFA::Transition* trans = new DFA::Transition[nstates*colors + 1];
00697 int current_transition = 0;
00698
00699 for (int state = base_states; state--; ) {
00700 for (int color = 1; color <= colors; ++color) {
00701 const int color_bit = (1 << (color-1));
00702 const int color_remembered_state = state + color*base_states;
00703
00704 trans[current_transition++] =
00705 DFA::Transition(state, color, color_remembered_state);
00706
00707 for (int next_color = 1; next_color <= colors; ++next_color) {
00708 if (next_color == color) {
00709
00710 if (state & color_bit) {
00711 trans[current_transition++] =
00712 DFA::Transition(color_remembered_state, color, state & ~color_bit);
00713 }
00714 } else {
00715 trans[current_transition++] =
00716 DFA::Transition(color_remembered_state, next_color, state);
00717 }
00718 }
00719 }
00720 }
00721 trans[current_transition++] = DFA::Transition(-1, 0, -1);
00722 assert(current_transition <= nstates*colors+1);
00723
00724 int* final_states = new int[base_states+1];
00725 final_states[base_states] = -1;
00726 for (int i = base_states; i--; ) {
00727 final_states[i] = i;
00728 }
00729
00730 DFA result(start_state, trans, final_states);
00731
00732 delete[] trans;
00733 delete[] final_states;
00734
00735 return result;
00736 }
00737
00738 IntSetArgs distinct_except_0_counts(int colors, int size)
00739 {
00740 IntSetArgs result(colors+1);
00741
00742 result[0] = IntSet(0, size);
00743
00744 for (int i = 1; i <= colors; ++i) {
00745 result[i] = IntSet(0, 1);
00746 }
00747
00748 return result;
00749 }
00750
00751
00752 DFA not_all_equal_dfa(int colors)
00753 {
00754
00755
00756
00757
00758
00759
00760
00761
00762 const int nstates = 1 + colors + 1;
00763 const int start_state = 0;
00764 const int final_state = nstates-1;
00765
00766 DFA::Transition* trans = new DFA::Transition[2*colors + colors*colors + 1];
00767 int current_transition = 0;
00768
00769
00770 for (int color = 1; color <= colors; ++color) {
00771 trans[current_transition++] = DFA::Transition(start_state, color, color);
00772 }
00773
00774
00775 for (int state = 1; state <= colors; ++state) {
00776 for (int color = 1; color <= colors; ++color) {
00777 if (state == color) {
00778 trans[current_transition++] = DFA::Transition(state, color, state);
00779 } else {
00780 trans[current_transition++] = DFA::Transition(state, color, final_state);
00781 }
00782 }
00783 }
00784
00785
00786 for (int color = 1; color <= colors; ++color) {
00787 trans[current_transition++] = DFA::Transition(final_state, color, final_state);
00788 }
00789
00790 trans[current_transition++] = DFA::Transition(-1, 0, -1);
00791
00792 int final_states[] = {final_state, -1};
00793
00794 DFA result(start_state, trans, final_states);
00795
00796 delete[] trans;
00797
00798 return result;
00799 }
00800
00801 }
00802
00803
00804