Generated on Thu Apr 11 13:58:52 2019 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   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       // 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 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     // For each pair of columns and rows, the intersections may not be equal.
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     // 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 (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     // Symmetry breaking constraints.
00402     {
00403       // Lexical order for all columns and rows (all are interchangable)
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       // 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 (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   // 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(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 = 
00569       new DFA::Transition[static_cast<size_t>(n_transitions)];
00570     int current_transition = 0;
00571 
00572     // From start state
00573     for (int color = 1; color <= colors; ++color) {
00574       trans[current_transition++] =
00575         DFA::Transition(start_state, color, color);
00576     }
00577 
00578     // From first level states (indices [1..color])
00579     // To second-level if same color, otherwise to not_equal_state
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     // From second level states (indices [colors+1..colors+colors])
00593     // To final state with the same color
00594     for (int color = 1; color <= colors; ++color) {
00595       trans[current_transition++] =
00596         DFA::Transition(colors+color, color, final_state);
00597     }
00598 
00599     // From not equal state to final state
00600     trans[current_transition++] =
00601       DFA::Transition(not_equal_state, 0, final_state);
00602 
00603     // End sentinel
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     /* DFA for a sequence that may use each color only once (and all
00634      * others are zero).
00635      *
00636      * For n colors, 2^n nodes are used. For each node, if bit b is one, then
00637      * that color has not been used yet. All nodes have self-loops for zero, and
00638      * edges for still usable colors to the node with the corresponding bit un-set.
00639      * All nodes are final nodes.
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     /* DFA for a sequence of pairs, where each monochromatic pair may
00679      * only appear once.
00680      *
00681      * For n colors, there are 2^n base states representing which
00682      * monochromatic pairs are still available. For each base state s,
00683      * the color seen goes to a new intermediate state. A different
00684      * color will go back to state s. Seeing the same color will move
00685      * to the next base state with that color combination removed (if
00686      * it is still allowed).
00687      *
00688      * In essence, this DFA represents the combination of same_or_0
00689      * and distinct_except_0 as a single constraint.
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             // Two equal adjacent, only transition if color still allowed
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     /* DFA for not all equal.
00755      *
00756      * From the start state, there is a transition for each color to
00757      * that colors state.  As long as the same color is seen, the
00758      * automaton stays in that state. If a different color is seen,
00759      * then it goes to the accepting state.
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     // Each color to its own state
00770     for (int color = 1; color <= colors; ++color) {
00771       trans[current_transition++] = DFA::Transition(start_state, color, color);
00772     }
00773 
00774     // Each colors state loops on itself, and goes to final on all others
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     // Loop on all colors in final state
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 // STATISTICS: example-any