00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024
00025
00026
00027
00028
00029
00030
00031
00032
00033
00034
00035
00036
00037
00038 #include <gecode/minimodel.hh>
00039 #include <gecode/search.hh>
00040
00041 #include "test/test.hh"
00042
00043 namespace Test {
00044
00046 namespace NoGoods {
00047
00048 using namespace Gecode;
00049
00051 void dummy(Space&) {
00052 }
00053
00055 class Queens : public Space {
00056 public:
00058 const static int n = 18;
00060 IntVarArray q;
00062 Queens(IntValBranch ivb, bool assign, bool null)
00063 : q(*this,n,0,n-1) {
00064 distinct(*this, IntArgs::create(n,0,1), q, IPL_VAL);
00065 distinct(*this, IntArgs::create(n,0,-1), q, IPL_VAL);
00066 distinct(*this, q, IPL_VAL);
00067 if (assign) {
00068 IntVar x(*this,0,1); Gecode::assign(*this, x, INT_ASSIGN_MIN());
00069 }
00070 {
00071 IntVarArgs q1(n/2), q2(n/2);
00072 for (int i=0; i<n/2; i++) {
00073 q1[i] = q[i]; q2[i] = q[n/2 + i];
00074 }
00075 branch(*this, q1, INT_VAR_NONE(), ivb);
00076 if (null)
00077 branch(*this, &dummy);
00078 branch(*this, q2, INT_VAR_NONE(), ivb);
00079 }
00080 if (assign) {
00081 IntVar x(*this,0,1); Gecode::assign(*this, x, INT_ASSIGN_MIN());
00082 }
00083 }
00085 Queens(Queens& s) : Space(s) {
00086 q.update(*this, s.q);
00087 }
00089 virtual Space* copy(void) {
00090 return new Queens(*this);
00091 }
00093 bool same(const Queens& s) const {
00094 for (int i=0; i<q.size(); i++)
00095 if (q[i].val() != s.q[i].val())
00096 return false;
00097 return true;
00098 }
00100 static unsigned int nodeinc(void) {
00101 return 500;
00102 }
00104 static std::string name(void) {
00105 return "Queens";
00106 }
00108 static std::string val(IntValBranch ivb) {
00109 switch (ivb.select()) {
00110 case IntValBranch::SEL_MIN: return "INT_VAL_MIN";
00111 case IntValBranch::SEL_MAX: return "INT_VAL_MAX";
00112 case IntValBranch::SEL_SPLIT_MIN: return "INT_VAL_SPLIT_MIN";
00113 case IntValBranch::SEL_SPLIT_MAX: return "INT_VAL_SPLIT_MAX";
00114 case IntValBranch::SEL_VALUES_MIN: return "INT_VALUES_MIN";
00115 case IntValBranch::SEL_VALUES_MAX: return "INT_VALUES_MAX";
00116 default: GECODE_NEVER;
00117 }
00118 return "";
00119 }
00120 };
00121
00122 #ifdef GECODE_HAS_SET_VARS
00123
00124 class Hamming : public Space {
00125 private:
00127 static const int size = 16;
00129 static const int distance = 4;
00131 static const int bits = 8;
00133 SetVarArray x;
00134 public:
00136 Hamming(SetValBranch svb, bool assign, bool null) :
00137 x(*this,size,IntSet::empty,1,bits) {
00138 SetVarArgs cx(x.size());
00139 for (int i=x.size(); i--;)
00140 cx[i] = expr(*this, -x[i]);
00141
00142 for (int i=0; i<x.size(); i++)
00143 for (int j=i+1; j<x.size(); j++)
00144 rel(*this,
00145 cardinality(x[j] & cx[i]) +
00146 cardinality(x[i] & cx[j]) >= distance);
00147
00148 if (assign) {
00149 IntVar x(*this,0,1); Gecode::assign(*this, x, INT_ASSIGN_MIN());
00150 }
00151 {
00152 SetVarArgs x1(size/2), x2(size/2);
00153 for (int i=0; i<size/2; i++) {
00154 x1[i] = x[i]; x2[i] = x[size/2 + i];
00155 }
00156 branch(*this, x1, SET_VAR_NONE(), svb);
00157 if (null)
00158 branch(*this, &dummy);
00159 branch(*this, x2, SET_VAR_NONE(), svb);
00160 }
00161 if (assign) {
00162 IntVar x(*this,0,1); Gecode::assign(*this, x, INT_ASSIGN_MIN());
00163 }
00164 }
00166 Hamming(Hamming& s) : Space(s) {
00167 x.update(*this, s.x);
00168 }
00170 virtual Space* copy(void) {
00171 return new Hamming(*this);
00172 }
00174 bool same(const Hamming& s) const {
00175 for (int i=0; i<x.size(); i++) {
00176 SetVarGlbRanges a(x[i]), b(s.x[i]);
00177 if (!Iter::Ranges::equal(a,b))
00178 return false;
00179 }
00180 return true;
00181 }
00183 static unsigned int nodeinc(void) {
00184 return 35;
00185 }
00187 static std::string name(void) {
00188 return "Hamming";
00189 }
00191 static std::string val(SetValBranch svb) {
00192 switch (svb.select()) {
00193 case SetValBranch::SEL_MIN_INC: return "SET_VAL_MIN_INC";
00194 case SetValBranch::SEL_MAX_INC: return "SET_VAL_MAX_INC";
00195 case SetValBranch::SEL_MIN_EXC: return "SET_VAL_MIN_EXC";
00196 case SetValBranch::SEL_MAX_EXC: return "SET_VAL_MAX_EXC";
00197 default: GECODE_NEVER;
00198 }
00199 return "";
00200 }
00201 };
00202 #endif
00203
00205 template<class Model, class ValBranch>
00206 class NoGoods : public Base {
00207 protected:
00209 ValBranch vb;
00211 unsigned int t;
00213 bool a;
00215 bool n;
00216 public:
00218 static std::string str(unsigned int i) {
00219 std::stringstream s;
00220 s << i;
00221 return s.str();
00222 }
00224 NoGoods(ValBranch vb0, unsigned int t0, bool a0, bool n0)
00225 : Base("NoGoods::"+Model::name()+"::"+Model::val(vb0)+"::"+str(t0)+
00226 "::"+(a0 ? "+" : "-")+"::"+(n0 ? "+" : "-")),
00227 vb(vb0), t(t0), a(a0), n(n0) {}
00229 virtual bool run(void) {
00230 Model* m = new Model(vb,a,n);
00231
00232 Model* s_plain = dfs(m);
00233
00234 {
00235 Search::NodeStop ns(Model::nodeinc());
00236 Search::Options o;
00237 o.stop = &ns;
00238 o.threads = t;
00239 o.nogoods_limit = 256U;
00240 Search::Engine* e = Search::dfsengine(m,o);
00241 while (true) {
00242 Model* s = static_cast<Model*>(e->next());
00243 delete s;
00244 if (!e->stopped())
00245 break;
00246
00247 e->nogoods().post(*m);
00248 ns.limit(ns.limit()+Model::nodeinc());
00249 }
00250 delete e;
00251 }
00252
00253 Model* s_nogoods = dfs(m);
00254
00255 bool ok = ((s_nogoods != NULL) &&
00256 ((t != 1) || s_plain->same(*s_nogoods)));
00257
00258 delete m;
00259 delete s_nogoods;
00260 delete s_plain;
00261
00262 return ok;
00263 }
00264 };
00265
00266
00268 class Create {
00269 public:
00271 Create(void) {
00272 bool a = false;
00273 do {
00274 bool n = false;
00275 do {
00276 for (unsigned int t = 1; t<=4; t++) {
00277 (void) new NoGoods<Queens,IntValBranch>(INT_VAL_MIN(),t,a,n);
00278 (void) new NoGoods<Queens,IntValBranch>(INT_VAL_MAX(),t,a,n);
00279 (void) new NoGoods<Queens,IntValBranch>(INT_VAL_SPLIT_MIN(),t,a,n);
00280 (void) new NoGoods<Queens,IntValBranch>(INT_VAL_SPLIT_MAX(),t,a,n);
00281 (void) new NoGoods<Queens,IntValBranch>(INT_VALUES_MIN(),t,a,n);
00282 (void) new NoGoods<Queens,IntValBranch>(INT_VALUES_MAX(),t,a,n);
00283 #ifdef GECODE_HAS_SET_VARS
00284 (void) new NoGoods<Hamming,SetValBranch>(SET_VAL_MIN_INC(),t,a,n);
00285 (void) new NoGoods<Hamming,SetValBranch>(SET_VAL_MIN_EXC(),t,a,n);
00286 (void) new NoGoods<Hamming,SetValBranch>(SET_VAL_MAX_INC(),t,a,n);
00287 (void) new NoGoods<Hamming,SetValBranch>(SET_VAL_MAX_EXC(),t,a,n);
00288 #endif
00289 }
00290 n = !n;
00291 } while (n);
00292 a = !a;
00293 } while (a);
00294 }
00295 };
00296
00297 Create c;
00298 }
00299
00300 }
00301
00302