Generated on Wed Nov 5 2014 05:18:15 for Gecode by doxygen 1.7.6.1
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  *  Last modified:
00010  *     $Date: 2013-07-08 14:22:40 +0200 (Mon, 08 Jul 2013) $ by $Author: schulte $
00011  *     $Revision: 13820 $
00012  *
00013  *  This file is part of Gecode, the generic constraint
00014  *  development environment:
00015  *     http://www.gecode.org
00016  *
00017  *  Permission is hereby granted, free of charge, to any person obtaining
00018  *  a copy of this software and associated documentation files (the
00019  *  "Software"), to deal in the Software without restriction, including
00020  *  without limitation the rights to use, copy, modify, merge, publish,
00021  *  distribute, sublicense, and/or sell copies of the Software, and to
00022  *  permit persons to whom the Software is furnished to do so, subject to
00023  *  the following conditions:
00024  *
00025  *  The above copyright notice and this permission notice shall be
00026  *  included in all copies or substantial portions of the Software.
00027  *
00028  *  THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
00029  *  EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
00030  *  MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
00031  *  NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
00032  *  LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
00033  *  OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
00034  *  WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
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       // Redundant (implied by previous), but improves efficiency
00198       rel(*this, result, IRT_NQ, 0, same);      
00199       return result;
00200     }
00201     case SAME_OR_0_TUPLE_SET: {
00202       static TupleSet table = same_or_0_tuple_set(colors);
00203       IntVar result(*this, 0, colors);
00204       extensional(*this, IntVarArgs() << a << b << result, table);
00205       return result;
00206     }
00207     case SAME_OR_0_DFA: {
00208       static const DFA automaton = same_or_0_dfa(colors);
00209       IntVar result(*this, 0, colors);
00210       extensional(*this, IntVarArgs() << a << b << result, automaton);
00211       return result;
00212     }
00213     default:
00214       GECODE_NEVER;
00215       return IntVar(*this, 0, 0);
00216     }
00217   }
00218 
00221   void distinct_except_0(const IntVarArgs& v)
00222   {
00223     switch (opt.distinct_except_0()) {
00224     case DISTINCT_EXCEPT_0_REIFIED:
00225       for (int i = v.size(); i--; ) {
00226         BoolVar viIsZero = expr(*this, v[i] == 0);
00227         for (int j = i; j--; ) {
00228           rel(*this, viIsZero || (v[i] != v[j]));
00229         }
00230       }
00231       break;
00232     case DISTINCT_EXCEPT_0_DFA: {
00233       static const DFA automaton = distinct_except_0_dfa(colors);
00234       extensional(*this, v, automaton);
00235       break;
00236     }
00237     case DISTINCT_EXCEPT_0_COUNT: {
00238       static const IntSetArgs counts = distinct_except_0_counts(colors, std::max(width, height)); 
00239       count(*this, v, counts, opt.icl());
00240       break;
00241     }
00242     }
00243   }
00244 
00247   void not_all_equal(const IntVarArgs& v)
00248   {
00249     switch (opt.not_all_equal()) {
00250     case NOT_ALL_EQUAL_NQ: {
00251       rel(*this, v, IRT_NQ);
00252       break;
00253     }
00254     case NOT_ALL_EQUAL_NAIVE: {
00255       // At least one pair must be different.
00256       // Bad decomposition since too many disjuncts are created.
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       // It must not be the case that all are equal
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       // More than one number
00274       nvalues(*this, v, IRT_GR, 1);
00275       break;
00276     case NOT_ALL_EQUAL_COUNT:
00277       // No number in all positions
00278       count(*this, v, IntSet(0, v.size()-1), IntArgs::create(colors, 1), opt.icl());
00279       break;
00280     case NOT_ALL_EQUAL_DFA: {
00281       static const DFA automaton = not_all_equal_dfa(colors);
00282       extensional(*this, v, automaton);
00283       break;
00284     }
00285     }
00286   }
00287 
00291   void no_monochrome_rectangle(IntVarArgs v1, IntVarArgs v2) {
00292     const unsigned int length = v1.size();
00293     switch (opt.no_monochrome_rectangle()) {
00294     case NO_MONOCHROME_DECOMPOSITION: {
00295       IntVarArgs z(length);
00296       for (unsigned int i = 0; i < length; ++i) {
00297         z[i] = same_or_0(v1[i], v2[i]);
00298       }
00299       distinct_except_0(z);
00300       break;
00301     }
00302     case NO_MONOCHROME_DFA: {
00303       static const DFA automaton = no_monochrome_rectangle_dfa(colors);
00304       IntVarArgs z(2*length);
00305       for (int i = length; i--; ) {
00306         z[2*i + 0] = v1[i];
00307         z[2*i + 1] = v2[i];
00308       }
00309       extensional(*this, z, automaton);
00310       break;
00311     }
00312     }
00313   }
00314 
00315 
00316 public:
00318   enum {
00319     SEARCH_DFS, 
00320     SEARCH_BAB, 
00321   };
00323   enum {
00324     SYMMETRY_NONE   = 0,   
00325     SYMMETRY_MATRIX = 1, 
00326     SYMMETRY_VALUES = 2, 
00327   };
00329   enum {
00330     MODEL_CORNERS = 1,   
00331     MODEL_ROWS    = 2,      
00332     MODEL_COLUMNS = 4,   
00333   };
00335   enum {
00336     NOT_ALL_EQUAL_NQ,      
00337     NOT_ALL_EQUAL_NAIVE,   
00338     NOT_ALL_EQUAL_REIFIED, 
00339     NOT_ALL_EQUAL_NVALUES, 
00340     NOT_ALL_EQUAL_COUNT,   
00341     NOT_ALL_EQUAL_DFA,     
00342   };
00344   enum {
00345     SAME_OR_0_REIFIED,   
00346     SAME_OR_0_DFA,       
00347     SAME_OR_0_TUPLE_SET, 
00348   };
00350   enum {
00351     DISTINCT_EXCEPT_0_REIFIED, 
00352     DISTINCT_EXCEPT_0_DFA,     
00353     DISTINCT_EXCEPT_0_COUNT,   
00354   };
00356   enum {
00357     NO_MONOCHROME_DECOMPOSITION, 
00358     NO_MONOCHROME_DFA,           
00359   };
00360 
00361 
00363   ColoredMatrix(const ColoredMatrixOptions& opt0)
00364     : opt(opt0), height(opt.height()), width(opt.width()), colors(opt.colors()),
00365       x(*this, height*width, 1, colors),
00366       max_color(*this, 1, colors)
00367   {
00368 
00369     max(*this, x, max_color);
00370 
00371     Matrix<IntVarArray> m(x, width, height);
00372     
00373     // For each pair of columns and rows, the intersections may not be equal.
00374     if (opt.model() & MODEL_CORNERS) {
00375       for (unsigned int c1 = 0; c1 < width; ++c1) {
00376         for (unsigned int c2 = c1+1; c2 < width; ++c2) {
00377           for (unsigned int r1 = 0; r1 < height; ++r1) {
00378             for (unsigned int r2 = r1+1; r2 < height; ++r2) {
00379               not_all_equal(IntVarArgs() << m(c1,r1) << m(c1,r2) << m(c2,r1) << m(c2,r2));
00380             }
00381           }
00382         }
00383       }
00384     }
00385     // Given two rows/columns, construct variables representing if
00386     // the corresponding places are equal (and if so, what value).
00387     // For the new values, no non-zero value may appear more than
00388     // once.
00389     if (opt.model() & MODEL_ROWS) {
00390       for (unsigned int r1 = 0; r1 < height; ++r1) {
00391         for (unsigned int r2 = r1+1; r2 < height; ++r2) {
00392           no_monochrome_rectangle(m.row(r1), m.row(r2));
00393         }
00394       }
00395     }
00396     if (opt.model() & MODEL_COLUMNS) {
00397       for (unsigned int c1 = 0; c1 < width; ++c1) {
00398         for (unsigned int c2 = c1+1; c2 < width; ++c2) {
00399           no_monochrome_rectangle(m.col(c1), m.col(c2));
00400         }
00401       }
00402     }
00403 
00404     // Symmetry breaking constraints.
00405     {
00406       // Lexical order for all columns and rows (all are interchangable)
00407       if (opt.symmetry() & SYMMETRY_MATRIX) {
00408         for (unsigned int r = 0; r < height-1; ++r) {
00409           rel(*this, m.row(r), IRT_LE, m.row(r+1));
00410         }
00411         for (unsigned int c = 0; c < width-1; ++c) {
00412           rel(*this, m.col(c), IRT_LE, m.col(c+1));
00413         }
00414       }
00415 
00416       // Value precedence. Compatible with row/column ordering
00417       if (opt.symmetry() & SYMMETRY_VALUES) {
00418         precede(*this, x, IntArgs::create(colors, 1));
00419       }      
00420     }
00421 
00422     branch(*this, x, tiebreak(INT_VAR_MIN_MIN(), INT_VAR_SIZE_MIN()), INT_VAL_MIN());
00423   }
00424 
00426   virtual IntVar cost(void) const {
00427     return max_color;
00428   }
00429 
00431   virtual void
00432   print(std::ostream& os) const {
00433     Matrix<IntVarArray> m(x, width, height);
00434     for (unsigned int r = 0; r < height; ++r) {
00435       os << "\t";
00436       for (unsigned int c = 0; c < width; ++c) {
00437         os << m(c, r) << " ";
00438       }
00439       os << std::endl;
00440     }    
00441     os << std::endl;
00442     os << "\tmax color: " << max_color << std::endl;
00443     os << std::endl;
00444   }
00445 
00447   ColoredMatrix(bool share, ColoredMatrix& s)
00448     : IntMinimizeScript(share,s), opt(s.opt),
00449       height(s.height), width(s.width), colors(s.colors) {
00450     x.update(*this, share, s.x);
00451     max_color.update(*this, share, s.max_color);
00452   }
00454   virtual Space*
00455   copy(bool share) {
00456     return new ColoredMatrix(share,*this);
00457   }
00458 };
00459 
00460 ColoredMatrixOptions::ColoredMatrixOptions(const char* n)
00461   : Options(n),
00462     _height("-height", "Height of matrix", 8),
00463     _width("-width", "Width of matrix", 8),
00464     _size("-size", "If different from 0, used as both width and height", 0),
00465     _colors("-colors", "Maximum number of colors", 4),
00466     _not_all_equal("-not-all-equal", "How to implement the not all equals constraint (used in corners model)", 
00467                    ColoredMatrix::NOT_ALL_EQUAL_NQ),
00468     _same_or_0("-same-or-0", "How to implement the same or 0 constraint (used in the decomposed no monochrome rectangle constraint)", 
00469                ColoredMatrix::SAME_OR_0_DFA),
00470     _distinct_except_0("-distinct-except-0", "How to implement the distinct except 0 constraint (used in the decomposed no monochrome rectangle constraint)", 
00471                        ColoredMatrix::DISTINCT_EXCEPT_0_DFA),
00472     _no_monochrome_rectangle("-no-monochrome-rectangle", "How to implement no monochrome rectangle (used in the rows model)", 
00473                              ColoredMatrix::NO_MONOCHROME_DFA)
00474 {
00475   add(_height);
00476   add(_width);
00477   add(_size);
00478   add(_colors);
00479   add(_not_all_equal);
00480   add(_same_or_0);
00481   add(_distinct_except_0);
00482   add(_no_monochrome_rectangle);
00483 
00484   // Add search options
00485   _search.add(ColoredMatrix::SEARCH_DFS,  "dfs", "Find a solution.");
00486   _search.add(ColoredMatrix::SEARCH_BAB,  "bab", "Find an optimal solution.");
00487   _search.value(ColoredMatrix::SEARCH_DFS);
00488   
00489   // Add symmetry options
00490   _symmetry.add(ColoredMatrix::SYMMETRY_NONE,  "none", "Don't use symmetry breaking.");
00491   _symmetry.add(ColoredMatrix::SYMMETRY_MATRIX,  "matrix", "Order matrix rows and columns");
00492   _symmetry.add(ColoredMatrix::SYMMETRY_VALUES,  "values", "Order values");
00493   _symmetry.add(ColoredMatrix::SYMMETRY_MATRIX | ColoredMatrix::SYMMETRY_VALUES,
00494                 "both", "Order both rows/columns and values");
00495   _symmetry.value(ColoredMatrix::SYMMETRY_MATRIX);
00496 
00497   // Add model options
00498   _model.add(ColoredMatrix::MODEL_CORNERS,  "corner", "Use direct corners model with not-all-equal constraints.");
00499   _model.add(ColoredMatrix::MODEL_ROWS,  "rows", "Use model on pairs of rows (same_or_0 and distinct_except_0 constraints).");
00500   _model.add(ColoredMatrix::MODEL_ROWS | ColoredMatrix::MODEL_CORNERS,
00501              "both", "Use both rows and corners model");
00502   _model.add(ColoredMatrix::MODEL_COLUMNS,  "columns", "Use model on pairs of columns (same_or_0 and distinct_except_0 constraints).");
00503   _model.add(ColoredMatrix::MODEL_ROWS | ColoredMatrix::MODEL_COLUMNS,
00504              "matrix", "Use both rows and columns model");
00505   _model.value(ColoredMatrix::MODEL_CORNERS);
00506 
00507   // Add not all equal variants
00508   _not_all_equal.add(ColoredMatrix::NOT_ALL_EQUAL_NQ, "nq", "Use nq constraint.");
00509   _not_all_equal.add(ColoredMatrix::NOT_ALL_EQUAL_NAIVE, "naive", "Use naive reified decomposition.");
00510   _not_all_equal.add(ColoredMatrix::NOT_ALL_EQUAL_REIFIED, "reified", "Use reified decomposition.");
00511   _not_all_equal.add(ColoredMatrix::NOT_ALL_EQUAL_NVALUES, "nvalues", "Use nvalues.");
00512   _not_all_equal.add(ColoredMatrix::NOT_ALL_EQUAL_COUNT, "count", "Use count.");
00513   _not_all_equal.add(ColoredMatrix::NOT_ALL_EQUAL_DFA, "dfa", "Use dfa.");
00514 
00515   // Add same or 0 variants
00516   _same_or_0.add(ColoredMatrix::SAME_OR_0_REIFIED, "reified", "Use reified decomposition.");
00517   _same_or_0.add(ColoredMatrix::SAME_OR_0_TUPLE_SET, "tuple-set", "Use tuple set representation.");
00518   _same_or_0.add(ColoredMatrix::SAME_OR_0_DFA, "dfa", "Use dfa representation.");
00519 
00520   // Add distinct except 0 variants
00521   _distinct_except_0.add(ColoredMatrix::DISTINCT_EXCEPT_0_REIFIED, "reified", "Use reified decomposition.");
00522   _distinct_except_0.add(ColoredMatrix::DISTINCT_EXCEPT_0_DFA, "dfa", "Use dfa decomposition.");
00523   _distinct_except_0.add(ColoredMatrix::DISTINCT_EXCEPT_0_COUNT, "count", "Use global cardinality.");
00524 
00525   // Add no monochrome rectangle variants
00526   _no_monochrome_rectangle.add(ColoredMatrix::NO_MONOCHROME_DECOMPOSITION, 
00527                                "decompositions", 
00528                                "Use decompositions into same_or_0 and distinct_except_0.");
00529   _no_monochrome_rectangle.add(ColoredMatrix::NO_MONOCHROME_DFA, 
00530                                "dfa", 
00531                                "Use DFA as direct implementation.");
00532 }
00533 
00537 int
00538 main(int argc, char* argv[]) {
00539   ColoredMatrixOptions opt("Colored matrix");
00540   opt.parse(argc,argv);
00541   if (opt.search() == ColoredMatrix::SEARCH_DFS) {
00542     Script::run<ColoredMatrix,DFS,ColoredMatrixOptions>(opt);
00543   } else {
00544     Script::run<ColoredMatrix,BAB,ColoredMatrixOptions>(opt);
00545   }
00546   return 0;
00547 }
00548 
00549 
00550 namespace {
00551   DFA same_or_0_dfa(unsigned int colors)
00552   {
00553     /* DFA over variable sequences (x,y,z) where z equals x/y if x and
00554      * y are equal, and z equals 0 otherwise.
00555      * 
00556      * DFA is constructed to contain paths 
00557      *   start -- c --> node -- c --> node' -- c --> end
00558      * for all colors c representing the case when x and y 
00559      * are equal.
00560      *
00561      * For the cases where x and y are non-equal (c and c'), paths
00562      *   start -- c --> node -- c' --> not-equal -- 0 --> end
00563      * are added.
00564      */
00565 
00566     const int start_state = 0;
00567     const int not_equal_state = 2*colors+1;
00568     const int final_state = 2*colors+2;
00569 
00570     int n_transitions = colors*colors + 2*colors + 2;
00571     DFA::Transition* trans = new DFA::Transition[n_transitions];
00572     int current_transition = 0;
00573     
00574     // From start state
00575     for (unsigned int color = 1; color <= colors; ++color) {
00576       trans[current_transition++] =
00577         DFA::Transition(start_state, color, color);
00578     }
00579 
00580     // From first level states (indices [1..color])
00581     // To second-level if same color, otherwise to not_equal_state
00582     for (unsigned int state = 1; state <= colors; ++state) {
00583       for (unsigned int color = 1; color <= colors; ++color) {
00584         if (color == state) {
00585           trans[current_transition++] =
00586             DFA::Transition(state, color, colors+state);
00587         } else {          
00588           trans[current_transition++] =
00589             DFA::Transition(state, color, not_equal_state);
00590         }
00591       }
00592     }
00593 
00594     // From second level states (indices [colors+1..colors+colors])
00595     // To final state with the same color
00596     for (unsigned int color = 1; color <= colors; ++color) {
00597       trans[current_transition++] =
00598         DFA::Transition(colors+color, color, final_state);
00599     }
00600 
00601     // From not equal state to final state
00602     trans[current_transition++] =
00603       DFA::Transition(not_equal_state, 0, final_state);
00604     
00605     // End sentinel
00606     trans[current_transition++] =
00607       DFA::Transition(-1, 0, -1);
00608     
00609     int final_states[] = {final_state, -1};
00610     
00611     DFA result(start_state, trans, final_states, true);
00612 
00613     delete[] trans;
00614 
00615     return result;
00616   }
00617   
00618   TupleSet same_or_0_tuple_set(unsigned int colors)
00619   {
00620     TupleSet result;
00621     for (unsigned int i = 1; i <= colors; ++i) {
00622       for (unsigned int j = 1; j <= colors; ++j) {
00623         if (i == j) {
00624           result.add(IntArgs(3, i, j, i));
00625         } else {
00626           result.add(IntArgs(3, i, j, 0));
00627         }
00628       }
00629     }
00630     result.finalize();
00631     return result;
00632   }  
00633 
00634   DFA distinct_except_0_dfa(unsigned int colors)
00635   {
00636     /* DFA for a sequence that may use each color only once (and all
00637      * others are zero).
00638      * 
00639      * For n colors, 2^n nodes are used. For each node, if bit b is one, then 
00640      * that color has not been used yet. All nodes have self-loops for zero, and 
00641      * edges for still usable colors to the node with the corresponding bit un-set. 
00642      * All nodes are final nodes.
00643      */
00644 
00645     const int nstates = 1 << colors;
00646     const int start_state = nstates-1;
00647 
00648     DFA::Transition* trans = new DFA::Transition[nstates*colors + 1];
00649     int current_transition = 0;
00650 
00651     for (int state = nstates; state--; ) {
00652       trans[current_transition++] = DFA::Transition(state, 0, state);
00653 
00654       for (unsigned int color = 1; color <= colors; ++color) {
00655         const unsigned int color_bit = (1 << (color-1));
00656         if (state & color_bit) {
00657           trans[current_transition++] = 
00658             DFA::Transition(state, color, state & ~color_bit);
00659         }
00660       }
00661     }
00662     trans[current_transition++] = DFA::Transition(-1, 0, -1);
00663 
00664     int* final_states = new int[nstates+1];
00665     final_states[nstates] = -1;
00666     for (int i = nstates; i--; ) {
00667       final_states[i] = i;
00668     }
00669 
00670     DFA result(start_state, trans, final_states);
00671 
00672     delete[] trans;
00673     delete[] final_states;
00674 
00675     return result;
00676   }
00677 
00678   DFA no_monochrome_rectangle_dfa(unsigned int colors)
00679   {
00680     /* DFA for a sequence of pairs, where each monochromatic pair may
00681      * only appear once.
00682      * 
00683      * For n colors, there are 2^n base states representing which
00684      * monochromatic pairs are still available. For each base state s,
00685      * the color seen goes to a new intermediate state. A different
00686      * color will go back to state s. Seeing the same color will move
00687      * to the next base state with that color combination removed (if
00688      * it is still allowed).
00689      *
00690      * In essence, this DFA represents the combination of same_or_0
00691      * and distinct_except_0 as a single constraint.
00692      */
00693 
00694     const int base_states = 1 << colors;
00695     const int start_state = base_states-1;
00696     const int nstates = base_states + colors*base_states;
00697 
00698     DFA::Transition* trans = new DFA::Transition[nstates*colors + 1];
00699     int current_transition = 0;
00700 
00701     for (int state = base_states; state--; ) {
00702       for (unsigned int color = 1; color <= colors; ++color) {
00703         const unsigned int color_bit = (1 << (color-1));
00704         const int color_remembered_state = state + color*base_states;
00705         
00706         trans[current_transition++] = 
00707           DFA::Transition(state, color, color_remembered_state);
00708         
00709         for (unsigned int next_color = 1; next_color <= colors; ++next_color) {
00710           if (next_color == color) {
00711             // Two equal adjacent, only transition if color still allowed
00712             if (state & color_bit) {
00713               trans[current_transition++] = 
00714                 DFA::Transition(color_remembered_state, color, state & ~color_bit);
00715             }
00716           } else {
00717             trans[current_transition++] = 
00718               DFA::Transition(color_remembered_state, next_color, state);
00719           }
00720         }
00721       }
00722     }
00723     trans[current_transition++] = DFA::Transition(-1, 0, -1);
00724     assert(current_transition <= nstates*colors+1);
00725 
00726     int* final_states = new int[base_states+1];
00727     final_states[base_states] = -1;
00728     for (int i = base_states; i--; ) {
00729       final_states[i] = i;
00730     }
00731 
00732     DFA result(start_state, trans, final_states);
00733 
00734     delete[] trans;
00735     delete[] final_states;
00736 
00737     return result;
00738   }
00739 
00740   IntSetArgs distinct_except_0_counts(unsigned int colors, unsigned int size)
00741   {
00742     IntSetArgs result(colors+1);
00743 
00744     result[0] = IntSet(0, size);
00745 
00746     for (unsigned int i = 1; i <= colors; ++i) {
00747       result[i] = IntSet(0, 1);
00748     }
00749 
00750     return result;
00751   }
00752 
00753 
00754   DFA not_all_equal_dfa(unsigned int colors)
00755   {
00756     /* DFA for not all equal. 
00757      *
00758      * From the start state, there is a transition for each color to
00759      * that colors state.  As long as the same color is seen, the
00760      * automaton stays in that state. If a different color is seen,
00761      * then it goes to the accepting state.
00762      */
00763 
00764     const int nstates = 1 + colors + 1;
00765     const int start_state = 0;
00766     const int final_state = nstates-1;
00767 
00768     DFA::Transition* trans = new DFA::Transition[2*colors + colors*colors + 1];
00769     int current_transition = 0;
00770 
00771     // Each color to its own state
00772     for (unsigned int color = 1; color <= colors; ++color) {
00773       trans[current_transition++] = DFA::Transition(start_state, color, color);
00774     }
00775 
00776     // Each colors state loops on itself, and goes to final on all others
00777     for (unsigned int state = 1; state <= colors; ++state) {
00778       for (unsigned int color = 1; color <= colors; ++color) {
00779         if (state == color) {
00780           trans[current_transition++] = DFA::Transition(state, color, state);
00781         } else {
00782           trans[current_transition++] = DFA::Transition(state, color, final_state);
00783         }
00784       }
00785     }
00786 
00787     // Loop on all colors in final state
00788     for (unsigned int color = 1; color <= colors; ++color) {
00789       trans[current_transition++] = DFA::Transition(final_state, color, final_state);
00790     }
00791 
00792     trans[current_transition++] = DFA::Transition(-1, 0, -1);
00793 
00794     int final_states[] = {final_state, -1};
00795 
00796     DFA result(start_state, trans, final_states);
00797 
00798     delete[] trans;
00799 
00800     return result;
00801   }
00802 
00803 }
00804 
00805 
00806 // STATISTICS: example-any