00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023 #include <cstdlib>
00024 #include <ctime>
00025 #include <math.h>
00026
00027 #include <iostream>
00028
00029 #include "gecode/minimodel.hh"
00030 #include "gecode/int/element.hh"
00031
00032 #include "qsolver.hh"
00033 #include "implicative.hh"
00034
00035 #define UNIVERSAL true
00036 #define EXISTENTIAL false
00037
00038
00039
00040
00041
00042
00043
00044 using namespace MiniModel;
00045
00046 int main (int argc, char * const argv[]) {
00047
00048 int depth = 5;
00049 int nbDecisionVar = 2*depth;
00050 int nbScope = nbDecisionVar+1;
00051 bool* qtScopes = new bool[nbScope];
00052 for (int i=0;i<nbScope;i++) {
00053 qtScopes[i] = ((i%2) != 0);
00054 cout << (((i%2) != 0)?"true":"false")<<endl;
00055 }
00056 int boardSize = (int)pow((double)2,(double)depth);
00057
00058 std::srand(std::time(NULL));
00059
00060 IntArgs board(boardSize*boardSize);
00061 for (int i=0; i<boardSize; i++)
00062 for (int j=0; j<boardSize; j++)
00063 board[j*boardSize+i] = (int)( (double)rand() / ((double)RAND_MAX + 1) * 50 ) < 25 ? 0:1;
00064
00065 IntArgs access(nbDecisionVar);
00066 access[nbDecisionVar-1]=1;
00067 access[nbDecisionVar-2]=boardSize;
00068 for (int i=nbDecisionVar-3; i>=0; i--)
00069 access[i]=access[i+2]*2;
00070
00071
00072 for (int i=0; i<boardSize; i++)
00073 {
00074 for (int j=0; j<boardSize; j++)
00075 cout << board[j*boardSize+i] << " ";
00076 cout << endl;
00077 }
00078 cout << endl;
00079 for (int i=0; i<nbDecisionVar; i++)
00080 cout << access[i] << " ";
00081 cout << endl;
00082
00083
00084 int *scopesSize = new int[nbScope];
00085 for (int i=0; i<nbScope-1; i++)
00086 scopesSize[i]=1;
00087 scopesSize[nbScope-1]=2;
00088
00089 Implicative p(nbScope, qtScopes, scopesSize);
00090
00091
00092 for (int i=0; i<nbDecisionVar; i++)
00093 {
00094 p.QIntVar(i, 0, 1);
00095 IntVarArgs b(i+1);
00096 for (int plop=0;plop<(i+1);plop++)
00097 b[plop] = p.var(plop);
00098 branch(p.space(),b,INT_VAR_SIZE_MIN,INT_VAL_MIN);
00099 p.nextScope();
00100 }
00101
00102
00103
00104 p.QIntVar(nbDecisionVar, 0, 1);
00105 p.QIntVar(nbDecisionVar+1, 0, boardSize*boardSize);
00106 IntVarArgs b(nbDecisionVar+2);
00107 for (int plop=0;plop<(nbDecisionVar+2);plop++)
00108 b[plop] = p.var(plop);
00109 branch(p.space(),b,INT_VAR_SIZE_MIN,INT_VAL_MIN);
00110
00111 p.nextScope();
00112
00113
00114 post(p.space(), p.var(nbDecisionVar) == 1);
00115
00116 IntVarArgs X(nbDecisionVar);
00117 for (int i=0; i<nbDecisionVar; i++)
00118 X[i]=p.var(i);
00119
00120 linear(p.space(), access, X, IRT_EQ, p.var(nbDecisionVar+1));
00121
00122 element(p.space(), board, p.var(nbDecisionVar+1), p.var(nbDecisionVar));
00123
00124
00125
00126 p.makeStructure();
00127
00128
00129 QSolver solver(&p);
00130
00131 unsigned long int nodes=0;
00132
00133
00134
00135 Strategy outcome = solver.solve(nodes);
00136
00137 cout << " outcome: " << ( outcome.isFalse()? "FALSE" : "TRUE") << endl;
00138 cout << " nodes visited: " << nodes << endl;
00139
00140 }