Generated on Fri Oct 19 11:24:48 2018 for Gecode by doxygen 1.6.3

colored-matrix.cpp

Go to the documentation of this file.
00001 /* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
00002 /*
00003  *  Main authors:
00004  *     Mikael Lagerkvist <lagerkvist@gecode.org>
00005  *
00006  *  Copyright:
00007  *     Mikael Lagerkvist, 2012
00008  *
00009  *  This file is part of Gecode, the generic constraint
00010  *  development environment:
00011  *     http://www.gecode.org
00012  *
00013  *  Permission is hereby granted, free of charge, to any person obtaining
00014  *  a copy of this software and associated documentation files (the
00015  *  "Software"), to deal in the Software without restriction, including
00016  *  without limitation the rights to use, copy, modify, merge, publish,
00017  *  distribute, sublicense, and/or sell copies of the Software, and to
00018  *  permit persons to whom the Software is furnished to do so, subject to
00019  *  the following conditions:
00020  *
00021  *  The above copyright notice and this permission notice shall be
00022  *  included in all copies or substantial portions of the Software.
00023  *
00024  *  THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
00025  *  EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
00026  *  MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
00027  *  NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
00028  *  LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
00029  *  OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
00030  *  WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
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       // Redundant (implied by previous), but improves efficiency
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       // At least one pair must be different.
00252       // Bad decomposition since too many disjuncts are created.
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       // It must not be the case that all are equal
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       // More than one number
00270       nvalues(*this, v, IRT_GR, 1);
00271       break;
00272     case NOT_ALL_EQUAL_COUNT:
00273       // No number in all positions
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     // For each pair of columns and rows, the intersections may not be equal.
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     // Given two rows/columns, construct variables representing if
00383     // the corresponding places are equal (and if so, what value).
00384     // For the new values, no non-zero value may appear more than
00385     // once.
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     // Symmetry breaking constraints.
00402     {
00403       // Lexical order for all columns and rows (all are interchangable)
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       // Value precedence. Compatible with row/column ordering
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   // Add search options
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   // Add symmetry options
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   // Add model options
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   // Add not all equal variants
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   // Add same or 0 variants
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   // Add distinct except 0 variants
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   // Add no monochrome rectangle variants
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     /* DFA over variable sequences (x,y,z) where z equals x/y if x and
00551      * y are equal, and z equals 0 otherwise.
00552      *
00553      * DFA is constructed to contain paths
00554      *   start -- c --> node -- c --> node' -- c --> end
00555      * for all colors c representing the case when x and y
00556      * are equal.
00557      *
00558      * For the cases where x and y are non-equal (c and c'), paths
00559      *   start -- c --> node -- c' --> not-equal -- 0 --> end
00560      * are added.
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     // From start state
00572     for (unsigned int color = 1; color <= colors; ++color) {
00573       trans[current_transition++] =
00574         DFA::Transition(start_state, color, color);
00575     }
00576 
00577     // From first level states (indices [1..color])
00578     // To second-level if same color, otherwise to not_equal_state
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     // From second level states (indices [colors+1..colors+colors])
00592     // To final state with the same color
00593     for (unsigned int color = 1; color <= colors; ++color) {
00594       trans[current_transition++] =
00595         DFA::Transition(colors+color, color, final_state);
00596     }
00597 
00598     // From not equal state to final state
00599     trans[current_transition++] =
00600       DFA::Transition(not_equal_state, 0, final_state);
00601 
00602     // End sentinel
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 (int i = 1; i <= colors; ++i) {
00618       for (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     /* DFA for a sequence that may use each color only once (and all
00633      * others are zero).
00634      *
00635      * For n colors, 2^n nodes are used. For each node, if bit b is one, then
00636      * that color has not been used yet. All nodes have self-loops for zero, and
00637      * edges for still usable colors to the node with the corresponding bit un-set.
00638      * All nodes are final nodes.
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     /* DFA for a sequence of pairs, where each monochromatic pair may
00677      * only appear once.
00678      *
00679      * For n colors, there are 2^n base states representing which
00680      * monochromatic pairs are still available. For each base state s,
00681      * the color seen goes to a new intermediate state. A different
00682      * color will go back to state s. Seeing the same color will move
00683      * to the next base state with that color combination removed (if
00684      * it is still allowed).
00685      *
00686      * In essence, this DFA represents the combination of same_or_0
00687      * and distinct_except_0 as a single constraint.
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             // Two equal adjacent, only transition if color still allowed
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     /* DFA for not all equal.
00753      *
00754      * From the start state, there is a transition for each color to
00755      * that colors state.  As long as the same color is seen, the
00756      * automaton stays in that state. If a different color is seen,
00757      * then it goes to the accepting state.
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     // Each color to its own state
00768     for (unsigned int color = 1; color <= colors; ++color) {
00769       trans[current_transition++] = DFA::Transition(start_state, color, color);
00770     }
00771 
00772     // Each colors state loops on itself, and goes to final on all others
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     // Loop on all colors in final state
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 // STATISTICS: example-any