00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022 #include "set.hh"
00023 #include "examples/support.hh"
00024 #include "minimodel.hh"
00025
00026 #include "examples/sudoku.icc"
00027
00029 IntVarArgs unionOfArgs(const IntVarArgs as, const IntVarArgs bs) {
00030 IntVarArgs res(as.size() + bs.size());
00031 for (int i=as.size(); i--;)
00032 res[i] = as[i];
00033 for (int i=bs.size(); i--;)
00034 res[as.size()+i] = bs[i];
00035 return res;
00036 }
00037
00043 void same(Space* home, IntVarArgs a, IntVarArgs b) {
00044 SetVar u(home, IntSet::empty, 1, 81);
00045 rel(home, SOT_DUNION, a, u);
00046 rel(home, SOT_DUNION, b, u);
00047 }
00048
00060 class SudokuMixed : public Example {
00061 protected:
00062 static const int n = 3;
00063 SetVarArray x;
00064 public:
00066 SudokuMixed(const Options& opt)
00067 : x(this,n*n,IntSet::empty,1,n*n*n*n,9,9) {
00068
00069 const int nn = n*n;
00070
00071
00072
00073
00074
00075
00076 IntVarArray y(this,n*n*n*n,1,n*n);
00077
00078 MiniModel::Matrix<IntVarArray> m(y, nn, nn);
00079
00080
00081 for (int i=0; i<nn; i++) {
00082 distinct(this, m.row(i), opt.icl);
00083 distinct(this, m.col(i), opt.icl);
00084 }
00085
00086
00087 for (int i=0; i<nn; i+=n)
00088 for (int j=0; j<nn; j+=n) {
00089 distinct(this, m.slice(i, i+n, j, j+n), opt.icl);
00090 }
00091
00092
00093 for (int i=0; i<nn; i++)
00094 for (int j=0; j<nn; j++)
00095 if (examples[opt.size][i][j] != 0)
00096 rel(this, m(i,j), IRT_EQ, examples[opt.size][i][j]);
00097
00098
00099 for (int i=0; i<nn; i+=n) {
00100 for (int j=0; j<nn; j+=n) {
00101 MiniModel::Matrix<IntVarArgs> block = m.slice(i, i+n, j, j+n);
00102 for (int r1=0; r1<2; r1++)
00103 for (int r2=r1+1; r2<3; r2++) {
00104 IntVarArgs b1 = unionOfArgs(block.col(r1), block.col(r2));
00105 IntVarArgs b2 = unionOfArgs(block.row(r1), block.row(r2));
00106 IntVarArgs r(0);
00107 IntVarArgs c(0);
00108 switch (r1+r2) {
00109 case 1:
00110 r = unionOfArgs(m.slice(0,i,j+2,j+3), m.slice(i+n,nn,j+2,j+3));
00111 c = unionOfArgs(m.slice(i+2,i+3,0,j), m.slice(i+2,i+3,j+n,nn));
00112 assert(r.size()==6);
00113 break;
00114 case 2:
00115 r = unionOfArgs(m.slice(0,i,j+1,j+2), m.slice(i+n,nn,j+1,j+2));
00116 c = unionOfArgs(m.slice(i+1,i+2,0,j), m.slice(i+1,i+2,j+n,nn));
00117 assert(r.size()==6);
00118 break;
00119 case 3:
00120 r = unionOfArgs(m.slice(0,i,j+0,j+1), m.slice(i+n,nn,j+0,j+1));
00121 c = unionOfArgs(m.slice(i+0,i+1,0,j), m.slice(i+0,i+1,j+n,nn));
00122 assert(r.size()==6);
00123 break;
00124 default:
00125 assert(false);
00126 }
00127 same(this, r, b1);
00128 same(this, c, b2);
00129 }
00130 }
00131 }
00132
00133
00134
00135
00136
00137
00138
00139 IntSet is0(0,0);
00140 SetVar dummySet0(this, is0, is0);
00141 IntVar dummyInt0(this, 0, 0);
00142 SetVarArgs xs(nn+1);
00143 xs[0] = dummySet0;
00144 for (int i=0; i<nn; i++)
00145 xs[i+1] = x[i];
00146 IntVarArgs ys(nn*nn+1);
00147 ys[0] = dummyInt0;
00148 for (int i=0; i<nn*nn; i++)
00149 ys[i+1] = y[i];
00150
00151 channelVarVal(this, ys, xs);
00152
00153 gcc(this, y, 9, ICL_DOM);
00154
00155
00156
00157
00158
00159
00160
00161
00162 IntSet row[9];
00163 IntSet col[9];
00164 IntSet block[9];
00165
00166
00167 for (int i=0; i<9; i++) {
00168 IntSet dsr((i*nn)+1, (i*nn)+9);
00169 row[i] = dsr;
00170
00171 int dsc_arr[9] = { 1+i, 10+i, 19+i, 28+i, 37+i, 46+i, 55+i, 64+i, 73+i };
00172 IntSet dsc(dsc_arr, 9);
00173
00174 col[i] = dsc;
00175 }
00176
00177
00178 for (int i=0; i<3; i++)
00179 for (int j=0; j<3; j++) {
00180 int dsb_arr[9] = {
00181 (j*27)+(i*3)+1, (j*27)+(i*3)+2, (j*27)+(i*3)+3,
00182 (j*27)+(i*3)+10, (j*27)+(i*3)+11, (j*27)+(i*3)+12,
00183 (j*27)+(i*3)+19, (j*27)+(i*3)+20, (j*27)+(i*3)+21
00184 };
00185 IntSet dsb(dsb_arr, 9);
00186 block[i*3+j]=dsb;
00187 }
00188
00189
00190 for (int i=0; i<nn-1; i++)
00191 for (int j=i+1; j<nn; j++)
00192 rel(this, x[i], SRT_DISJ, x[j]);
00193 distinct(this, x, nn);
00194
00195
00196
00197 for (int i=0; i<nn; i++)
00198 for (int j=0; j<nn; j++) {
00199 SetVar inter_row(this, IntSet::empty, 1, 9*9, 1, 1);
00200 rel(this, x[i], SOT_INTER, row[j], SRT_EQ, inter_row);
00201 SetVar inter_col(this, IntSet::empty, 1, 9*9, 1, 1);
00202 rel(this, x[i], SOT_INTER, col[j], SRT_EQ, inter_col);
00203 SetVar inter_block(this, IntSet::empty, 1, 9*9, 1, 1);
00204 rel(this, x[i], SOT_INTER, block[j], SRT_EQ, inter_block);
00205 }
00206
00207
00208 for (int i=0; i<nn; i++)
00209 for (int j=0; j<nn; j++)
00210 if (examples[opt.size][i][j] != 0) {
00211 int idx = examples[opt.size][i][j]-1;
00212 dom(this, x[idx], SRT_SUP, (i+1)+(j*nn) );
00213 }
00214
00215 branch(this, x, SETBVAR_NONE, SETBVAL_MIN);
00216 }
00217
00219 SudokuMixed(bool share, SudokuMixed& s) : Example(share,s) {
00220 x.update(this, share, s.x);
00221 }
00222
00224 virtual Space*
00225 copy(bool share) {
00226 return new SudokuMixed(share,*this);
00227 }
00228
00230 virtual void
00231 print(void) {
00232 std::cout << '\t';
00233 for (int i = 0; i<n*n*n*n; i++) {
00234 for (int j=0; j<n*n; j++) {
00235 if (x[j].contains(i+1)) {
00236 std::cout << j+1 << " ";
00237 break;
00238 }
00239 }
00240 if((i+1)%(n*n) == 0)
00241 std::cout << std::endl << '\t';
00242 }
00243 std::cout << std::endl;
00244 }
00245 };
00246
00247
00251 int
00252 main(int argc, char** argv) {
00253 Options opt("Sudoku (Mixed Model)");
00254 opt.iterations = 200;
00255 opt.size = 0;
00256 opt.icl = ICL_DOM;
00257 opt.solutions = 1;
00258 opt.naive = true;
00259 opt.parse(argc,argv);
00260 if (opt.size >= n_examples) {
00261 std::cerr << "Error: size must be between 0 and "
00262 << n_examples-1 << std::endl;
00263 return 1;
00264 }
00265 Example::run<SudokuMixed,DFS>(opt);
00266 return 0;
00267 }
00268
00269
00270