qecode: /Users/jamian/Desktop/qecode/examples/connect-5-3-3-3.cpp Source File

00001 // Quantified/alternating formulation of the Connect4 game
00002 // with a board of size 3x3 (widthxheight), a winning
00003 // line of length 3, analyzed up to 5 moves for the initial/existential player
00004 
00005 #include "gecode/minimodel.hh"
00006 #include "gecode/int/element.hh"
00007 
00008 #include "qsolver.hh"
00009 #include "implicative.hh"
00010 
00011 #define UNIVERSAL true
00012 #define EXISTENTIAL false
00013 
00014 #define WIDTH 3
00015 #define HEIGHT 3
00016 #define DEPTH 9
00017 
00018 #define VARS_PER_BOARD (WIDTH*HEIGHT)
00019 #define VARS_PER_STEP  (VARS_PER_BOARD + 1)
00020 
00021 #define CELL_VCODE(I,J,TIME) \
00022          ( (((I)-1)*WIDTH) + ((J)-1) + \
00023          (((TIME)==0)? 0 : (((TIME))*(VARS_PER_STEP))))
00024 #define MOVE_VCODE(TIME) \
00025          ( VARS_PER_BOARD + ((TIME)-1)*VARS_PER_STEP )
00026 #define AUX_VCODE(N) ( (N) +  CELL_VCODE(HEIGHT,WIDTH,DEPTH) )
00027 
00028 #define B(I,J,TIME) p.var(CELL_VCODE(I,J,TIME))
00029 #define M(TIME)     p.var(MOVE_VCODE(TIME))
00030 #define AUX(N)      p.bvar(AUX_VCODE(N))
00031 
00032 using namespace Gecode;
00033 using namespace Gecode::MiniModel;
00034 
00035 int main () {
00036             
00037          int scopesSize[] = {19, 10, 10, 10, 10, 10, 10, 10, 18};
00038     bool qts[] = {EXISTENTIAL,UNIVERSAL,EXISTENTIAL,UNIVERSAL,EXISTENTIAL,UNIVERSAL,EXISTENTIAL,UNIVERSAL,EXISTENTIAL};
00039          Implicative p(9, qts, scopesSize);
00040 
00041          p.QIntVar(0, 0, 2);  // B(1,1,0)
00042          p.QIntVar(1, 0, 2);  // B(1,2,0)
00043          p.QIntVar(2, 0, 2);  // B(1,3,0)
00044          p.QIntVar(3, 0, 2);  // B(2,1,0)
00045          p.QIntVar(4, 0, 2);  // B(2,2,0)
00046          p.QIntVar(5, 0, 2);  // B(2,3,0)
00047          p.QIntVar(6, 0, 2);  // B(3,1,0)
00048          p.QIntVar(7, 0, 2);  // B(3,2,0)
00049          p.QIntVar(8, 0, 2);  // B(3,3,0)
00050          p.QIntVar(9, 1, 2);  // M(1)
00051          p.QIntVar(10, 0, 2);  // B(1,1,1)
00052          p.QIntVar(11, 0, 2);  // B(1,2,1)
00053          p.QIntVar(12, 0, 2);  // B(1,3,1)
00054          p.QIntVar(13, 0, 2);  // B(2,1,1)
00055          p.QIntVar(14, 0, 2);  // B(2,2,1)
00056          p.QIntVar(15, 0, 2);  // B(2,3,1)
00057          p.QIntVar(16, 0, 2);  // B(3,1,1)
00058          p.QIntVar(17, 0, 2);  // B(3,2,1)
00059          p.QIntVar(18, 0, 2);  // B(3,3,1)
00060 
00061          // The initial board is empty
00062          post(p.space(), B(1,1,0)==0 );
00063          post(p.space(), B(1,2,0)==0 );
00064          post(p.space(), B(1,3,0)==0 );
00065          post(p.space(), B(2,1,0)==0 );
00066          post(p.space(), B(2,2,0)==0 );
00067          post(p.space(), B(2,3,0)==0 );
00068          post(p.space(), B(3,1,0)==0 );
00069          post(p.space(), B(3,2,0)==0 );
00070          post(p.space(), B(3,3,0)==0 );
00071 
00072          // PA (Precondition Axiom) specifying legal moves at transition 0->1
00073          // A move is valid only if the related colum is not full
00074          post(p.space(), tt( (~(B(3,1,0)==0) || ~(M(1)!=1)) ) );
00075          post(p.space(), tt( (~(B(3,2,0)==0) || ~(M(1)!=2)) ) );
00076          post(p.space(), tt( (~(B(3,3,0)==0) || ~(M(1)!=3)) ) );
00077 
00078          // SSA (Successor State Axiom) linking time 0 to time 1
00079          // The player who moves is "1"
00080 
00081          // If a cell is occupied by player 1, it stays so
00082          post(p.space(), tt( (!(~(B(1,1,0)==1)) || ~(B(1,1,1)==1)) ) );
00083          post(p.space(), tt( (!(~(B(1,2,0)==1)) || ~(B(1,2,1)==1)) ) );
00084          post(p.space(), tt( (!(~(B(1,3,0)==1)) || ~(B(1,3,1)==1)) ) );
00085          post(p.space(), tt( (!(~(B(2,1,0)==1)) || ~(B(2,1,1)==1)) ) );
00086          post(p.space(), tt( (!(~(B(2,2,0)==1)) || ~(B(2,2,1)==1)) ) );
00087          post(p.space(), tt( (!(~(B(2,3,0)==1)) || ~(B(2,3,1)==1)) ) );
00088          post(p.space(), tt( (!(~(B(3,1,0)==1)) || ~(B(3,1,1)==1)) ) );
00089          post(p.space(), tt( (!(~(B(3,2,0)==1)) || ~(B(3,2,1)==1)) ) );
00090          post(p.space(), tt( (!(~(B(3,3,0)==1)) || ~(B(3,3,1)==1)) ) );
00091 
00092          // If a cell is occupied by player 2, it stays so
00093          post(p.space(), tt( (!(~(B(1,1,0)==2)) || ~(B(1,1,1)==2)) ) );
00094          post(p.space(), tt( (!(~(B(1,2,0)==2)) || ~(B(1,2,1)==2)) ) );
00095          post(p.space(), tt( (!(~(B(1,3,0)==2)) || ~(B(1,3,1)==2)) ) );
00096          post(p.space(), tt( (!(~(B(2,1,0)==2)) || ~(B(2,1,1)==2)) ) );
00097          post(p.space(), tt( (!(~(B(2,2,0)==2)) || ~(B(2,2,1)==2)) ) );
00098          post(p.space(), tt( (!(~(B(2,3,0)==2)) || ~(B(2,3,1)==2)) ) );
00099          post(p.space(), tt( (!(~(B(3,1,0)==2)) || ~(B(3,1,1)==2)) ) );
00100          post(p.space(), tt( (!(~(B(3,2,0)==2)) || ~(B(3,2,1)==2)) ) );
00101          post(p.space(), tt( (!(~(B(3,3,0)==2)) || ~(B(3,3,1)==2)) ) );
00102 
00103          // A free cell on top of a free cell stays free
00104          post(p.space(), tt( (!(((~(B(2,1,0)==0) && ~(B(1,1,0)==0)))) || ~(B(2,1,1)==0)) ) );
00105          post(p.space(), tt( (!(((~(B(2,2,0)==0) && ~(B(1,2,0)==0)))) || ~(B(2,2,1)==0)) ) );
00106          post(p.space(), tt( (!(((~(B(2,3,0)==0) && ~(B(1,3,0)==0)))) || ~(B(2,3,1)==0)) ) );
00107          post(p.space(), tt( (!(((~(B(3,1,0)==0) && ~(B(2,1,0)==0)))) || ~(B(3,1,1)==0)) ) );
00108          post(p.space(), tt( (!(((~(B(3,2,0)==0) && ~(B(2,2,0)==0)))) || ~(B(3,2,1)==0)) ) );
00109          post(p.space(), tt( (!(((~(B(3,3,0)==0) && ~(B(2,3,0)==0)))) || ~(B(3,3,1)==0)) ) );
00110 
00111          // A cell that changes value can only turn from "0" to "1" (moving player code)
00112          // ..and at most one such switch can happen in the whole board
00113          post(p.space(), tt( (!((~(B(1,1,0)==0) && ~(B(1,1,1)!=0))) || ((~(B(1,1,1)==1) && ~(M(1)==1)))) ) );
00114          post(p.space(), tt( (!((~(B(1,2,0)==0) && ~(B(1,2,1)!=0))) || ((~(B(1,2,1)==1) && ~(M(1)==2)))) ) );
00115          post(p.space(), tt( (!((~(B(1,3,0)==0) && ~(B(1,3,1)!=0))) || ((~(B(1,3,1)==1) && ~(M(1)==3)))) ) );
00116          post(p.space(), tt( (!((~(B(2,1,0)==0) && ~(B(2,1,1)!=0))) || ((~(B(2,1,1)==1) && ~(M(1)==1)))) ) );
00117          post(p.space(), tt( (!((~(B(2,2,0)==0) && ~(B(2,2,1)!=0))) || ((~(B(2,2,1)==1) && ~(M(1)==2)))) ) );
00118          post(p.space(), tt( (!((~(B(2,3,0)==0) && ~(B(2,3,1)!=0))) || ((~(B(2,3,1)==1) && ~(M(1)==3)))) ) );
00119          post(p.space(), tt( (!((~(B(3,1,0)==0) && ~(B(3,1,1)!=0))) || ((~(B(3,1,1)==1) && ~(M(1)==1)))) ) );
00120          post(p.space(), tt( (!((~(B(3,2,0)==0) && ~(B(3,2,1)!=0))) || ((~(B(3,2,1)==1) && ~(M(1)==2)))) ) );
00121          post(p.space(), tt( (!((~(B(3,3,0)==0) && ~(B(3,3,1)!=0))) || ((~(B(3,3,1)==1) && ~(M(1)==3)))) ) );
00122     
00123     IntVarArgs b1(19);
00124     for( int i=0;i<19;i++) {
00125         b1[i] = p.var(i);
00126     }
00127     branch(p.space(),b1,INT_VAR_SIZE_MIN,INT_VAL_MIN);
00128     
00129          p.nextScope();
00130          p.QIntVar(19, 1, 3);  // M(2)
00131          p.QIntVar(20, 0, 2);  // B(1,1,2)
00132          p.QIntVar(21, 0, 2);  // B(1,2,2)
00133          p.QIntVar(22, 0, 2);  // B(1,3,2)
00134          p.QIntVar(23, 0, 2);  // B(2,1,2)
00135          p.QIntVar(24, 0, 2);  // B(2,2,2)
00136          p.QIntVar(25, 0, 2);  // B(2,3,2)
00137          p.QIntVar(26, 0, 2);  // B(3,1,2)
00138          p.QIntVar(27, 0, 2);  // B(3,2,2)
00139          p.QIntVar(28, 0, 2);  // B(3,3,2)
00140 
00141          // CGA (Cut-Game Axiom) between time 1 and time 2
00142          // If player "1" won at time 1 then player "2" cannot play
00143 
00144          // Non-winning condition for player 1 at time 1
00145          post(p.space(), tt( (~(B(1,1,1)!=1) || ~(B(1,2,1)!=1) || ~(B(1,3,1)!=1)) ) );
00146          post(p.space(), tt( (~(B(1,1,1)!=1) || ~(B(2,1,1)!=1) || ~(B(3,1,1)!=1)) ) );
00147          post(p.space(), tt( (~(B(1,1,1)!=1) || ~(B(2,2,1)!=1) || ~(B(3,3,1)!=1)) ) );
00148          post(p.space(), tt( (~(B(3,1,1)!=1) || ~(B(2,2,1)!=1) || ~(B(1,3,1)!=1)) ) );
00149          post(p.space(), tt( (~(B(1,2,1)!=1) || ~(B(2,2,1)!=1) || ~(B(3,2,1)!=1)) ) );
00150          post(p.space(), tt( (~(B(1,3,1)!=1) || ~(B(2,3,1)!=1) || ~(B(3,3,1)!=1)) ) );
00151          post(p.space(), tt( (~(B(2,1,1)!=1) || ~(B(2,2,1)!=1) || ~(B(2,3,1)!=1)) ) );
00152          post(p.space(), tt( (~(B(3,1,1)!=1) || ~(B(3,2,1)!=1) || ~(B(3,3,1)!=1)) ) );
00153 
00154          // PA (Precondition Axiom) specifying legal moves at transition 1->2
00155          // A move is valid only if the related colum is not full
00156          post(p.space(), tt( (~(B(3,1,1)==0) || ~(M(2)!=1)) ) );
00157          post(p.space(), tt( (~(B(3,2,1)==0) || ~(M(2)!=2)) ) );
00158          post(p.space(), tt( (~(B(3,3,1)==0) || ~(M(2)!=3)) ) );
00159 
00160          // SSA (Successor State Axiom) linking time 1 to time 2
00161          // The player who moves is "2"
00162 
00163          // If a cell is occupied by player 1, it stays so
00164          post(p.space(), tt( (!(~(B(1,1,1)==1)) || ~(B(1,1,2)==1)) ) );
00165          post(p.space(), tt( (!(~(B(1,2,1)==1)) || ~(B(1,2,2)==1)) ) );
00166          post(p.space(), tt( (!(~(B(1,3,1)==1)) || ~(B(1,3,2)==1)) ) );
00167          post(p.space(), tt( (!(~(B(2,1,1)==1)) || ~(B(2,1,2)==1)) ) );
00168          post(p.space(), tt( (!(~(B(2,2,1)==1)) || ~(B(2,2,2)==1)) ) );
00169          post(p.space(), tt( (!(~(B(2,3,1)==1)) || ~(B(2,3,2)==1)) ) );
00170          post(p.space(), tt( (!(~(B(3,1,1)==1)) || ~(B(3,1,2)==1)) ) );
00171          post(p.space(), tt( (!(~(B(3,2,1)==1)) || ~(B(3,2,2)==1)) ) );
00172          post(p.space(), tt( (!(~(B(3,3,1)==1)) || ~(B(3,3,2)==1)) ) );
00173 
00174          // If a cell is occupied by player 2, it stays so
00175          post(p.space(), tt( (!(~(B(1,1,1)==2)) || ~(B(1,1,2)==2)) ) );
00176          post(p.space(), tt( (!(~(B(1,2,1)==2)) || ~(B(1,2,2)==2)) ) );
00177          post(p.space(), tt( (!(~(B(1,3,1)==2)) || ~(B(1,3,2)==2)) ) );
00178          post(p.space(), tt( (!(~(B(2,1,1)==2)) || ~(B(2,1,2)==2)) ) );
00179          post(p.space(), tt( (!(~(B(2,2,1)==2)) || ~(B(2,2,2)==2)) ) );
00180          post(p.space(), tt( (!(~(B(2,3,1)==2)) || ~(B(2,3,2)==2)) ) );
00181          post(p.space(), tt( (!(~(B(3,1,1)==2)) || ~(B(3,1,2)==2)) ) );
00182          post(p.space(), tt( (!(~(B(3,2,1)==2)) || ~(B(3,2,2)==2)) ) );
00183          post(p.space(), tt( (!(~(B(3,3,1)==2)) || ~(B(3,3,2)==2)) ) );
00184 
00185          // A free cell on top of a free cell stays free
00186          post(p.space(), tt( (!(((~(B(2,1,1)==0) && ~(B(1,1,1)==0)))) || ~(B(2,1,2)==0)) ) );
00187          post(p.space(), tt( (!(((~(B(2,2,1)==0) && ~(B(1,2,1)==0)))) || ~(B(2,2,2)==0)) ) );
00188          post(p.space(), tt( (!(((~(B(2,3,1)==0) && ~(B(1,3,1)==0)))) || ~(B(2,3,2)==0)) ) );
00189          post(p.space(), tt( (!(((~(B(3,1,1)==0) && ~(B(2,1,1)==0)))) || ~(B(3,1,2)==0)) ) );
00190          post(p.space(), tt( (!(((~(B(3,2,1)==0) && ~(B(2,2,1)==0)))) || ~(B(3,2,2)==0)) ) );
00191          post(p.space(), tt( (!(((~(B(3,3,1)==0) && ~(B(2,3,1)==0)))) || ~(B(3,3,2)==0)) ) );
00192 
00193          // A cell that changes value can only turn from "0" to "2" (moving player code)
00194          // ..and at most one such switch can happen in the whole board
00195          post(p.space(), tt( (!((~(B(1,1,1)==0) && ~(B(1,1,2)!=0))) || ((~(B(1,1,2)==2) && ~(M(2)==1)))) ) );
00196          post(p.space(), tt( (!((~(B(1,2,1)==0) && ~(B(1,2,2)!=0))) || ((~(B(1,2,2)==2) && ~(M(2)==2)))) ) );
00197          post(p.space(), tt( (!((~(B(1,3,1)==0) && ~(B(1,3,2)!=0))) || ((~(B(1,3,2)==2) && ~(M(2)==3)))) ) );
00198          post(p.space(), tt( (!((~(B(2,1,1)==0) && ~(B(2,1,2)!=0))) || ((~(B(2,1,2)==2) && ~(M(2)==1)))) ) );
00199          post(p.space(), tt( (!((~(B(2,2,1)==0) && ~(B(2,2,2)!=0))) || ((~(B(2,2,2)==2) && ~(M(2)==2)))) ) );
00200          post(p.space(), tt( (!((~(B(2,3,1)==0) && ~(B(2,3,2)!=0))) || ((~(B(2,3,2)==2) && ~(M(2)==3)))) ) );
00201          post(p.space(), tt( (!((~(B(3,1,1)==0) && ~(B(3,1,2)!=0))) || ((~(B(3,1,2)==2) && ~(M(2)==1)))) ) );
00202          post(p.space(), tt( (!((~(B(3,2,1)==0) && ~(B(3,2,2)!=0))) || ((~(B(3,2,2)==2) && ~(M(2)==2)))) ) );
00203          post(p.space(), tt( (!((~(B(3,3,1)==0) && ~(B(3,3,2)!=0))) || ((~(B(3,3,2)==2) && ~(M(2)==3)))) ) );
00204 
00205     IntVarArgs b2(29);
00206     for( int i=0;i<29;i++) {
00207         b2[i] = p.var(i);
00208     }
00209     branch(p.space(),b2,INT_VAR_SIZE_MIN,INT_VAL_MIN);
00210     
00211          p.nextScope();
00212          p.QIntVar(29, 1, 3);  // M(3)
00213          p.QIntVar(30, 0, 2);  // B(1,1,3)
00214          p.QIntVar(31, 0, 2);  // B(1,2,3)
00215          p.QIntVar(32, 0, 2);  // B(1,3,3)
00216          p.QIntVar(33, 0, 2);  // B(2,1,3)
00217          p.QIntVar(34, 0, 2);  // B(2,2,3)
00218          p.QIntVar(35, 0, 2);  // B(2,3,3)
00219          p.QIntVar(36, 0, 2);  // B(3,1,3)
00220          p.QIntVar(37, 0, 2);  // B(3,2,3)
00221          p.QIntVar(38, 0, 2);  // B(3,3,3)
00222 
00223          // CGA (Cut-Game Axiom) between time 2 and time 3
00224          // If player "2" won at time 2 then player "1" cannot play
00225 
00226          // Non-winning condition for player 2 at time 2
00227          post(p.space(), tt( (~(B(1,1,2)!=2) || ~(B(1,2,2)!=2) || ~(B(1,3,2)!=2)) ) );
00228          post(p.space(), tt( (~(B(1,1,2)!=2) || ~(B(2,1,2)!=2) || ~(B(3,1,2)!=2)) ) );
00229          post(p.space(), tt( (~(B(1,1,2)!=2) || ~(B(2,2,2)!=2) || ~(B(3,3,2)!=2)) ) );
00230          post(p.space(), tt( (~(B(3,1,2)!=2) || ~(B(2,2,2)!=2) || ~(B(1,3,2)!=2)) ) );
00231          post(p.space(), tt( (~(B(1,2,2)!=2) || ~(B(2,2,2)!=2) || ~(B(3,2,2)!=2)) ) );
00232          post(p.space(), tt( (~(B(1,3,2)!=2) || ~(B(2,3,2)!=2) || ~(B(3,3,2)!=2)) ) );
00233          post(p.space(), tt( (~(B(2,1,2)!=2) || ~(B(2,2,2)!=2) || ~(B(2,3,2)!=2)) ) );
00234          post(p.space(), tt( (~(B(3,1,2)!=2) || ~(B(3,2,2)!=2) || ~(B(3,3,2)!=2)) ) );
00235 
00236          // PA (Precondition Axiom) specifying legal moves at transition 2->3
00237          // A move is valid only if the related colum is not full
00238          post(p.space(), tt( (~(B(3,1,2)==0) || ~(M(3)!=1)) ) );
00239          post(p.space(), tt( (~(B(3,2,2)==0) || ~(M(3)!=2)) ) );
00240          post(p.space(), tt( (~(B(3,3,2)==0) || ~(M(3)!=3)) ) );
00241 
00242          // SSA (Successor State Axiom) linking time 2 to time 3
00243          // The player who moves is "1"
00244 
00245          // If a cell is occupied by player 1, it stays so
00246          post(p.space(), tt( (!(~(B(1,1,2)==1)) || ~(B(1,1,3)==1)) ) );
00247          post(p.space(), tt( (!(~(B(1,2,2)==1)) || ~(B(1,2,3)==1)) ) );
00248          post(p.space(), tt( (!(~(B(1,3,2)==1)) || ~(B(1,3,3)==1)) ) );
00249          post(p.space(), tt( (!(~(B(2,1,2)==1)) || ~(B(2,1,3)==1)) ) );
00250          post(p.space(), tt( (!(~(B(2,2,2)==1)) || ~(B(2,2,3)==1)) ) );
00251          post(p.space(), tt( (!(~(B(2,3,2)==1)) || ~(B(2,3,3)==1)) ) );
00252          post(p.space(), tt( (!(~(B(3,1,2)==1)) || ~(B(3,1,3)==1)) ) );
00253          post(p.space(), tt( (!(~(B(3,2,2)==1)) || ~(B(3,2,3)==1)) ) );
00254          post(p.space(), tt( (!(~(B(3,3,2)==1)) || ~(B(3,3,3)==1)) ) );
00255 
00256          // If a cell is occupied by player 2, it stays so
00257          post(p.space(), tt( (!(~(B(1,1,2)==2)) || ~(B(1,1,3)==2)) ) );
00258          post(p.space(), tt( (!(~(B(1,2,2)==2)) || ~(B(1,2,3)==2)) ) );
00259          post(p.space(), tt( (!(~(B(1,3,2)==2)) || ~(B(1,3,3)==2)) ) );
00260          post(p.space(), tt( (!(~(B(2,1,2)==2)) || ~(B(2,1,3)==2)) ) );
00261          post(p.space(), tt( (!(~(B(2,2,2)==2)) || ~(B(2,2,3)==2)) ) );
00262          post(p.space(), tt( (!(~(B(2,3,2)==2)) || ~(B(2,3,3)==2)) ) );
00263          post(p.space(), tt( (!(~(B(3,1,2)==2)) || ~(B(3,1,3)==2)) ) );
00264          post(p.space(), tt( (!(~(B(3,2,2)==2)) || ~(B(3,2,3)==2)) ) );
00265          post(p.space(), tt( (!(~(B(3,3,2)==2)) || ~(B(3,3,3)==2)) ) );
00266 
00267          // A free cell on top of a free cell stays free
00268          post(p.space(), tt( (!(((~(B(2,1,2)==0) && ~(B(1,1,2)==0)))) || ~(B(2,1,3)==0)) ) );
00269          post(p.space(), tt( (!(((~(B(2,2,2)==0) && ~(B(1,2,2)==0)))) || ~(B(2,2,3)==0)) ) );
00270          post(p.space(), tt( (!(((~(B(2,3,2)==0) && ~(B(1,3,2)==0)))) || ~(B(2,3,3)==0)) ) );
00271          post(p.space(), tt( (!(((~(B(3,1,2)==0) && ~(B(2,1,2)==0)))) || ~(B(3,1,3)==0)) ) );
00272          post(p.space(), tt( (!(((~(B(3,2,2)==0) && ~(B(2,2,2)==0)))) || ~(B(3,2,3)==0)) ) );
00273          post(p.space(), tt( (!(((~(B(3,3,2)==0) && ~(B(2,3,2)==0)))) || ~(B(3,3,3)==0)) ) );
00274 
00275          // A cell that changes value can only turn from "0" to "1" (moving player code)
00276          // ..and at most one such switch can happen in the whole board
00277          post(p.space(), tt( (!((~(B(1,1,2)==0) && ~(B(1,1,3)!=0))) || ((~(B(1,1,3)==1) && ~(M(3)==1)))) ) );
00278          post(p.space(), tt( (!((~(B(1,2,2)==0) && ~(B(1,2,3)!=0))) || ((~(B(1,2,3)==1) && ~(M(3)==2)))) ) );
00279          post(p.space(), tt( (!((~(B(1,3,2)==0) && ~(B(1,3,3)!=0))) || ((~(B(1,3,3)==1) && ~(M(3)==3)))) ) );
00280          post(p.space(), tt( (!((~(B(2,1,2)==0) && ~(B(2,1,3)!=0))) || ((~(B(2,1,3)==1) && ~(M(3)==1)))) ) );
00281          post(p.space(), tt( (!((~(B(2,2,2)==0) && ~(B(2,2,3)!=0))) || ((~(B(2,2,3)==1) && ~(M(3)==2)))) ) );
00282          post(p.space(), tt( (!((~(B(2,3,2)==0) && ~(B(2,3,3)!=0))) || ((~(B(2,3,3)==1) && ~(M(3)==3)))) ) );
00283          post(p.space(), tt( (!((~(B(3,1,2)==0) && ~(B(3,1,3)!=0))) || ((~(B(3,1,3)==1) && ~(M(3)==1)))) ) );
00284          post(p.space(), tt( (!((~(B(3,2,2)==0) && ~(B(3,2,3)!=0))) || ((~(B(3,2,3)==1) && ~(M(3)==2)))) ) );
00285          post(p.space(), tt( (!((~(B(3,3,2)==0) && ~(B(3,3,3)!=0))) || ((~(B(3,3,3)==1) && ~(M(3)==3)))) ) );
00286 
00287     IntVarArgs b3(39);
00288     for( int i=0;i<39;i++) {
00289         b3[i] = p.var(i);
00290     }
00291     branch(p.space(),b3,INT_VAR_SIZE_MIN,INT_VAL_MIN);
00292     
00293          p.nextScope();
00294          p.QIntVar(39, 1, 3);  // M(4)
00295          p.QIntVar(40, 0, 2);  // B(1,1,4)
00296          p.QIntVar(41, 0, 2);  // B(1,2,4)
00297          p.QIntVar(42, 0, 2);  // B(1,3,4)
00298          p.QIntVar(43, 0, 2);  // B(2,1,4)
00299          p.QIntVar(44, 0, 2);  // B(2,2,4)
00300          p.QIntVar(45, 0, 2);  // B(2,3,4)
00301          p.QIntVar(46, 0, 2);  // B(3,1,4)
00302          p.QIntVar(47, 0, 2);  // B(3,2,4)
00303          p.QIntVar(48, 0, 2);  // B(3,3,4)
00304 
00305          // CGA (Cut-Game Axiom) between time 3 and time 4
00306          // If player "1" won at time 3 then player "2" cannot play
00307 
00308          // Non-winning condition for player 1 at time 3
00309          post(p.space(), tt( (~(B(1,1,3)!=1) || ~(B(1,2,3)!=1) || ~(B(1,3,3)!=1)) ) );
00310          post(p.space(), tt( (~(B(1,1,3)!=1) || ~(B(2,1,3)!=1) || ~(B(3,1,3)!=1)) ) );
00311          post(p.space(), tt( (~(B(1,1,3)!=1) || ~(B(2,2,3)!=1) || ~(B(3,3,3)!=1)) ) );
00312          post(p.space(), tt( (~(B(3,1,3)!=1) || ~(B(2,2,3)!=1) || ~(B(1,3,3)!=1)) ) );
00313          post(p.space(), tt( (~(B(1,2,3)!=1) || ~(B(2,2,3)!=1) || ~(B(3,2,3)!=1)) ) );
00314          post(p.space(), tt( (~(B(1,3,3)!=1) || ~(B(2,3,3)!=1) || ~(B(3,3,3)!=1)) ) );
00315          post(p.space(), tt( (~(B(2,1,3)!=1) || ~(B(2,2,3)!=1) || ~(B(2,3,3)!=1)) ) );
00316          post(p.space(), tt( (~(B(3,1,3)!=1) || ~(B(3,2,3)!=1) || ~(B(3,3,3)!=1)) ) );
00317 
00318          // PA (Precondition Axiom) specifying legal moves at transition 3->4
00319          // A move is valid only if the related colum is not full
00320          post(p.space(), tt( (~(B(3,1,3)==0) || ~(M(4)!=1)) ) );
00321          post(p.space(), tt( (~(B(3,2,3)==0) || ~(M(4)!=2)) ) );
00322          post(p.space(), tt( (~(B(3,3,3)==0) || ~(M(4)!=3)) ) );
00323 
00324          // SSA (Successor State Axiom) linking time 3 to time 4
00325          // The player who moves is "2"
00326 
00327          // If a cell is occupied by player 1, it stays so
00328          post(p.space(), tt( (!(~(B(1,1,3)==1)) || ~(B(1,1,4)==1)) ) );
00329          post(p.space(), tt( (!(~(B(1,2,3)==1)) || ~(B(1,2,4)==1)) ) );
00330          post(p.space(), tt( (!(~(B(1,3,3)==1)) || ~(B(1,3,4)==1)) ) );
00331          post(p.space(), tt( (!(~(B(2,1,3)==1)) || ~(B(2,1,4)==1)) ) );
00332          post(p.space(), tt( (!(~(B(2,2,3)==1)) || ~(B(2,2,4)==1)) ) );
00333          post(p.space(), tt( (!(~(B(2,3,3)==1)) || ~(B(2,3,4)==1)) ) );
00334          post(p.space(), tt( (!(~(B(3,1,3)==1)) || ~(B(3,1,4)==1)) ) );
00335          post(p.space(), tt( (!(~(B(3,2,3)==1)) || ~(B(3,2,4)==1)) ) );
00336          post(p.space(), tt( (!(~(B(3,3,3)==1)) || ~(B(3,3,4)==1)) ) );
00337 
00338          // If a cell is occupied by player 2, it stays so
00339          post(p.space(), tt( (!(~(B(1,1,3)==2)) || ~(B(1,1,4)==2)) ) );
00340          post(p.space(), tt( (!(~(B(1,2,3)==2)) || ~(B(1,2,4)==2)) ) );
00341          post(p.space(), tt( (!(~(B(1,3,3)==2)) || ~(B(1,3,4)==2)) ) );
00342          post(p.space(), tt( (!(~(B(2,1,3)==2)) || ~(B(2,1,4)==2)) ) );
00343          post(p.space(), tt( (!(~(B(2,2,3)==2)) || ~(B(2,2,4)==2)) ) );
00344          post(p.space(), tt( (!(~(B(2,3,3)==2)) || ~(B(2,3,4)==2)) ) );
00345          post(p.space(), tt( (!(~(B(3,1,3)==2)) || ~(B(3,1,4)==2)) ) );
00346          post(p.space(), tt( (!(~(B(3,2,3)==2)) || ~(B(3,2,4)==2)) ) );
00347          post(p.space(), tt( (!(~(B(3,3,3)==2)) || ~(B(3,3,4)==2)) ) );
00348 
00349          // A free cell on top of a free cell stays free
00350          post(p.space(), tt( (!(((~(B(2,1,3)==0) && ~(B(1,1,3)==0)))) || ~(B(2,1,4)==0)) ) );
00351          post(p.space(), tt( (!(((~(B(2,2,3)==0) && ~(B(1,2,3)==0)))) || ~(B(2,2,4)==0)) ) );
00352          post(p.space(), tt( (!(((~(B(2,3,3)==0) && ~(B(1,3,3)==0)))) || ~(B(2,3,4)==0)) ) );
00353          post(p.space(), tt( (!(((~(B(3,1,3)==0) && ~(B(2,1,3)==0)))) || ~(B(3,1,4)==0)) ) );
00354          post(p.space(), tt( (!(((~(B(3,2,3)==0) && ~(B(2,2,3)==0)))) || ~(B(3,2,4)==0)) ) );
00355          post(p.space(), tt( (!(((~(B(3,3,3)==0) && ~(B(2,3,3)==0)))) || ~(B(3,3,4)==0)) ) );
00356 
00357          // A cell that changes value can only turn from "0" to "2" (moving player code)
00358          // ..and at most one such switch can happen in the whole board
00359          post(p.space(), tt( (!((~(B(1,1,3)==0) && ~(B(1,1,4)!=0))) || ((~(B(1,1,4)==2) && ~(M(4)==1)))) ) );
00360          post(p.space(), tt( (!((~(B(1,2,3)==0) && ~(B(1,2,4)!=0))) || ((~(B(1,2,4)==2) && ~(M(4)==2)))) ) );
00361          post(p.space(), tt( (!((~(B(1,3,3)==0) && ~(B(1,3,4)!=0))) || ((~(B(1,3,4)==2) && ~(M(4)==3)))) ) );
00362          post(p.space(), tt( (!((~(B(2,1,3)==0) && ~(B(2,1,4)!=0))) || ((~(B(2,1,4)==2) && ~(M(4)==1)))) ) );
00363          post(p.space(), tt( (!((~(B(2,2,3)==0) && ~(B(2,2,4)!=0))) || ((~(B(2,2,4)==2) && ~(M(4)==2)))) ) );
00364          post(p.space(), tt( (!((~(B(2,3,3)==0) && ~(B(2,3,4)!=0))) || ((~(B(2,3,4)==2) && ~(M(4)==3)))) ) );
00365          post(p.space(), tt( (!((~(B(3,1,3)==0) && ~(B(3,1,4)!=0))) || ((~(B(3,1,4)==2) && ~(M(4)==1)))) ) );
00366          post(p.space(), tt( (!((~(B(3,2,3)==0) && ~(B(3,2,4)!=0))) || ((~(B(3,2,4)==2) && ~(M(4)==2)))) ) );
00367          post(p.space(), tt( (!((~(B(3,3,3)==0) && ~(B(3,3,4)!=0))) || ((~(B(3,3,4)==2) && ~(M(4)==3)))) ) );
00368 
00369     IntVarArgs b4(49);
00370     for( int i=0;i<49;i++) {
00371         b4[i] = p.var(i);
00372     }
00373     branch(p.space(),b4,INT_VAR_SIZE_MIN,INT_VAL_MIN);
00374     
00375          p.nextScope();
00376          p.QIntVar(49, 1, 3);  // M(5)
00377          p.QIntVar(50, 0, 2);  // B(1,1,5)
00378          p.QIntVar(51, 0, 2);  // B(1,2,5)
00379          p.QIntVar(52, 0, 2);  // B(1,3,5)
00380          p.QIntVar(53, 0, 2);  // B(2,1,5)
00381          p.QIntVar(54, 0, 2);  // B(2,2,5)
00382          p.QIntVar(55, 0, 2);  // B(2,3,5)
00383          p.QIntVar(56, 0, 2);  // B(3,1,5)
00384          p.QIntVar(57, 0, 2);  // B(3,2,5)
00385          p.QIntVar(58, 0, 2);  // B(3,3,5)
00386 
00387          // CGA (Cut-Game Axiom) between time 4 and time 5
00388          // If player "2" won at time 4 then player "1" cannot play
00389 
00390          // Non-winning condition for player 2 at time 4
00391          post(p.space(), tt( (~(B(1,1,4)!=2) || ~(B(1,2,4)!=2) || ~(B(1,3,4)!=2)) ) );
00392          post(p.space(), tt( (~(B(1,1,4)!=2) || ~(B(2,1,4)!=2) || ~(B(3,1,4)!=2)) ) );
00393          post(p.space(), tt( (~(B(1,1,4)!=2) || ~(B(2,2,4)!=2) || ~(B(3,3,4)!=2)) ) );
00394          post(p.space(), tt( (~(B(3,1,4)!=2) || ~(B(2,2,4)!=2) || ~(B(1,3,4)!=2)) ) );
00395          post(p.space(), tt( (~(B(1,2,4)!=2) || ~(B(2,2,4)!=2) || ~(B(3,2,4)!=2)) ) );
00396          post(p.space(), tt( (~(B(1,3,4)!=2) || ~(B(2,3,4)!=2) || ~(B(3,3,4)!=2)) ) );
00397          post(p.space(), tt( (~(B(2,1,4)!=2) || ~(B(2,2,4)!=2) || ~(B(2,3,4)!=2)) ) );
00398          post(p.space(), tt( (~(B(3,1,4)!=2) || ~(B(3,2,4)!=2) || ~(B(3,3,4)!=2)) ) );
00399 
00400          // PA (Precondition Axiom) specifying legal moves at transition 4->5
00401          // A move is valid only if the related colum is not full
00402          post(p.space(), tt( (~(B(3,1,4)==0) || ~(M(5)!=1)) ) );
00403          post(p.space(), tt( (~(B(3,2,4)==0) || ~(M(5)!=2)) ) );
00404          post(p.space(), tt( (~(B(3,3,4)==0) || ~(M(5)!=3)) ) );
00405 
00406          // SSA (Successor State Axiom) linking time 4 to time 5
00407          // The player who moves is "1"
00408 
00409          // If a cell is occupied by player 1, it stays so
00410          post(p.space(), tt( (!(~(B(1,1,4)==1)) || ~(B(1,1,5)==1)) ) );
00411          post(p.space(), tt( (!(~(B(1,2,4)==1)) || ~(B(1,2,5)==1)) ) );
00412          post(p.space(), tt( (!(~(B(1,3,4)==1)) || ~(B(1,3,5)==1)) ) );
00413          post(p.space(), tt( (!(~(B(2,1,4)==1)) || ~(B(2,1,5)==1)) ) );
00414          post(p.space(), tt( (!(~(B(2,2,4)==1)) || ~(B(2,2,5)==1)) ) );
00415          post(p.space(), tt( (!(~(B(2,3,4)==1)) || ~(B(2,3,5)==1)) ) );
00416          post(p.space(), tt( (!(~(B(3,1,4)==1)) || ~(B(3,1,5)==1)) ) );
00417          post(p.space(), tt( (!(~(B(3,2,4)==1)) || ~(B(3,2,5)==1)) ) );
00418          post(p.space(), tt( (!(~(B(3,3,4)==1)) || ~(B(3,3,5)==1)) ) );
00419 
00420          // If a cell is occupied by player 2, it stays so
00421          post(p.space(), tt( (!(~(B(1,1,4)==2)) || ~(B(1,1,5)==2)) ) );
00422          post(p.space(), tt( (!(~(B(1,2,4)==2)) || ~(B(1,2,5)==2)) ) );
00423          post(p.space(), tt( (!(~(B(1,3,4)==2)) || ~(B(1,3,5)==2)) ) );
00424          post(p.space(), tt( (!(~(B(2,1,4)==2)) || ~(B(2,1,5)==2)) ) );
00425          post(p.space(), tt( (!(~(B(2,2,4)==2)) || ~(B(2,2,5)==2)) ) );
00426          post(p.space(), tt( (!(~(B(2,3,4)==2)) || ~(B(2,3,5)==2)) ) );
00427          post(p.space(), tt( (!(~(B(3,1,4)==2)) || ~(B(3,1,5)==2)) ) );
00428          post(p.space(), tt( (!(~(B(3,2,4)==2)) || ~(B(3,2,5)==2)) ) );
00429          post(p.space(), tt( (!(~(B(3,3,4)==2)) || ~(B(3,3,5)==2)) ) );
00430 
00431          // A free cell on top of a free cell stays free
00432          post(p.space(), tt( (!(((~(B(2,1,4)==0) && ~(B(1,1,4)==0)))) || ~(B(2,1,5)==0)) ) );
00433          post(p.space(), tt( (!(((~(B(2,2,4)==0) && ~(B(1,2,4)==0)))) || ~(B(2,2,5)==0)) ) );
00434          post(p.space(), tt( (!(((~(B(2,3,4)==0) && ~(B(1,3,4)==0)))) || ~(B(2,3,5)==0)) ) );
00435          post(p.space(), tt( (!(((~(B(3,1,4)==0) && ~(B(2,1,4)==0)))) || ~(B(3,1,5)==0)) ) );
00436          post(p.space(), tt( (!(((~(B(3,2,4)==0) && ~(B(2,2,4)==0)))) || ~(B(3,2,5)==0)) ) );
00437          post(p.space(), tt( (!(((~(B(3,3,4)==0) && ~(B(2,3,4)==0)))) || ~(B(3,3,5)==0)) ) );
00438 
00439          // A cell that changes value can only turn from "0" to "1" (moving player code)
00440          // ..and at most one such switch can happen in the whole board
00441          post(p.space(), tt( (!((~(B(1,1,4)==0) && ~(B(1,1,5)!=0))) || ((~(B(1,1,5)==1) && ~(M(5)==1)))) ) );
00442          post(p.space(), tt( (!((~(B(1,2,4)==0) && ~(B(1,2,5)!=0))) || ((~(B(1,2,5)==1) && ~(M(5)==2)))) ) );
00443          post(p.space(), tt( (!((~(B(1,3,4)==0) && ~(B(1,3,5)!=0))) || ((~(B(1,3,5)==1) && ~(M(5)==3)))) ) );
00444          post(p.space(), tt( (!((~(B(2,1,4)==0) && ~(B(2,1,5)!=0))) || ((~(B(2,1,5)==1) && ~(M(5)==1)))) ) );
00445          post(p.space(), tt( (!((~(B(2,2,4)==0) && ~(B(2,2,5)!=0))) || ((~(B(2,2,5)==1) && ~(M(5)==2)))) ) );
00446          post(p.space(), tt( (!((~(B(2,3,4)==0) && ~(B(2,3,5)!=0))) || ((~(B(2,3,5)==1) && ~(M(5)==3)))) ) );
00447          post(p.space(), tt( (!((~(B(3,1,4)==0) && ~(B(3,1,5)!=0))) || ((~(B(3,1,5)==1) && ~(M(5)==1)))) ) );
00448          post(p.space(), tt( (!((~(B(3,2,4)==0) && ~(B(3,2,5)!=0))) || ((~(B(3,2,5)==1) && ~(M(5)==2)))) ) );
00449          post(p.space(), tt( (!((~(B(3,3,4)==0) && ~(B(3,3,5)!=0))) || ((~(B(3,3,5)==1) && ~(M(5)==3)))) ) );
00450 
00451     IntVarArgs b5(59);
00452     for( int i=0;i<59;i++) {
00453         b5[i] = p.var(i);
00454     }
00455     branch(p.space(),b5,INT_VAR_SIZE_MIN,INT_VAL_MIN);
00456     
00457          p.nextScope();
00458          p.QIntVar(59, 1, 3);  // M(6)
00459          p.QIntVar(60, 0, 2);  // B(1,1,6)
00460          p.QIntVar(61, 0, 2);  // B(1,2,6)
00461          p.QIntVar(62, 0, 2);  // B(1,3,6)
00462          p.QIntVar(63, 0, 2);  // B(2,1,6)
00463          p.QIntVar(64, 0, 2);  // B(2,2,6)
00464          p.QIntVar(65, 0, 2);  // B(2,3,6)
00465          p.QIntVar(66, 0, 2);  // B(3,1,6)
00466          p.QIntVar(67, 0, 2);  // B(3,2,6)
00467          p.QIntVar(68, 0, 2);  // B(3,3,6)
00468 
00469          // CGA (Cut-Game Axiom) between time 5 and time 6
00470          // If player "1" won at time 5 then player "2" cannot play
00471 
00472          // Non-winning condition for player 1 at time 5
00473          post(p.space(), tt( (~(B(1,1,5)!=1) || ~(B(1,2,5)!=1) || ~(B(1,3,5)!=1)) ) );
00474          post(p.space(), tt( (~(B(1,1,5)!=1) || ~(B(2,1,5)!=1) || ~(B(3,1,5)!=1)) ) );
00475          post(p.space(), tt( (~(B(1,1,5)!=1) || ~(B(2,2,5)!=1) || ~(B(3,3,5)!=1)) ) );
00476          post(p.space(), tt( (~(B(3,1,5)!=1) || ~(B(2,2,5)!=1) || ~(B(1,3,5)!=1)) ) );
00477          post(p.space(), tt( (~(B(1,2,5)!=1) || ~(B(2,2,5)!=1) || ~(B(3,2,5)!=1)) ) );
00478          post(p.space(), tt( (~(B(1,3,5)!=1) || ~(B(2,3,5)!=1) || ~(B(3,3,5)!=1)) ) );
00479          post(p.space(), tt( (~(B(2,1,5)!=1) || ~(B(2,2,5)!=1) || ~(B(2,3,5)!=1)) ) );
00480          post(p.space(), tt( (~(B(3,1,5)!=1) || ~(B(3,2,5)!=1) || ~(B(3,3,5)!=1)) ) );
00481 
00482          // PA (Precondition Axiom) specifying legal moves at transition 5->6
00483          // A move is valid only if the related colum is not full
00484          post(p.space(), tt( (~(B(3,1,5)==0) || ~(M(6)!=1)) ) );
00485          post(p.space(), tt( (~(B(3,2,5)==0) || ~(M(6)!=2)) ) );
00486          post(p.space(), tt( (~(B(3,3,5)==0) || ~(M(6)!=3)) ) );
00487 
00488          // SSA (Successor State Axiom) linking time 5 to time 6
00489          // The player who moves is "2"
00490 
00491          // If a cell is occupied by player 1, it stays so
00492          post(p.space(), tt( (!(~(B(1,1,5)==1)) || ~(B(1,1,6)==1)) ) );
00493          post(p.space(), tt( (!(~(B(1,2,5)==1)) || ~(B(1,2,6)==1)) ) );
00494          post(p.space(), tt( (!(~(B(1,3,5)==1)) || ~(B(1,3,6)==1)) ) );
00495          post(p.space(), tt( (!(~(B(2,1,5)==1)) || ~(B(2,1,6)==1)) ) );
00496          post(p.space(), tt( (!(~(B(2,2,5)==1)) || ~(B(2,2,6)==1)) ) );
00497          post(p.space(), tt( (!(~(B(2,3,5)==1)) || ~(B(2,3,6)==1)) ) );
00498          post(p.space(), tt( (!(~(B(3,1,5)==1)) || ~(B(3,1,6)==1)) ) );
00499          post(p.space(), tt( (!(~(B(3,2,5)==1)) || ~(B(3,2,6)==1)) ) );
00500          post(p.space(), tt( (!(~(B(3,3,5)==1)) || ~(B(3,3,6)==1)) ) );
00501 
00502          // If a cell is occupied by player 2, it stays so
00503          post(p.space(), tt( (!(~(B(1,1,5)==2)) || ~(B(1,1,6)==2)) ) );
00504          post(p.space(), tt( (!(~(B(1,2,5)==2)) || ~(B(1,2,6)==2)) ) );
00505          post(p.space(), tt( (!(~(B(1,3,5)==2)) || ~(B(1,3,6)==2)) ) );
00506          post(p.space(), tt( (!(~(B(2,1,5)==2)) || ~(B(2,1,6)==2)) ) );
00507          post(p.space(), tt( (!(~(B(2,2,5)==2)) || ~(B(2,2,6)==2)) ) );
00508          post(p.space(), tt( (!(~(B(2,3,5)==2)) || ~(B(2,3,6)==2)) ) );
00509          post(p.space(), tt( (!(~(B(3,1,5)==2)) || ~(B(3,1,6)==2)) ) );
00510          post(p.space(), tt( (!(~(B(3,2,5)==2)) || ~(B(3,2,6)==2)) ) );
00511          post(p.space(), tt( (!(~(B(3,3,5)==2)) || ~(B(3,3,6)==2)) ) );
00512 
00513          // A free cell on top of a free cell stays free
00514          post(p.space(), tt( (!(((~(B(2,1,5)==0) && ~(B(1,1,5)==0)))) || ~(B(2,1,6)==0)) ) );
00515          post(p.space(), tt( (!(((~(B(2,2,5)==0) && ~(B(1,2,5)==0)))) || ~(B(2,2,6)==0)) ) );
00516          post(p.space(), tt( (!(((~(B(2,3,5)==0) && ~(B(1,3,5)==0)))) || ~(B(2,3,6)==0)) ) );
00517          post(p.space(), tt( (!(((~(B(3,1,5)==0) && ~(B(2,1,5)==0)))) || ~(B(3,1,6)==0)) ) );
00518          post(p.space(), tt( (!(((~(B(3,2,5)==0) && ~(B(2,2,5)==0)))) || ~(B(3,2,6)==0)) ) );
00519          post(p.space(), tt( (!(((~(B(3,3,5)==0) && ~(B(2,3,5)==0)))) || ~(B(3,3,6)==0)) ) );
00520 
00521          // A cell that changes value can only turn from "0" to "2" (moving player code)
00522          // ..and at most one such switch can happen in the whole board
00523          post(p.space(), tt( (!((~(B(1,1,5)==0) && ~(B(1,1,6)!=0))) || ((~(B(1,1,6)==2) && ~(M(6)==1)))) ) );
00524          post(p.space(), tt( (!((~(B(1,2,5)==0) && ~(B(1,2,6)!=0))) || ((~(B(1,2,6)==2) && ~(M(6)==2)))) ) );
00525          post(p.space(), tt( (!((~(B(1,3,5)==0) && ~(B(1,3,6)!=0))) || ((~(B(1,3,6)==2) && ~(M(6)==3)))) ) );
00526          post(p.space(), tt( (!((~(B(2,1,5)==0) && ~(B(2,1,6)!=0))) || ((~(B(2,1,6)==2) && ~(M(6)==1)))) ) );
00527          post(p.space(), tt( (!((~(B(2,2,5)==0) && ~(B(2,2,6)!=0))) || ((~(B(2,2,6)==2) && ~(M(6)==2)))) ) );
00528          post(p.space(), tt( (!((~(B(2,3,5)==0) && ~(B(2,3,6)!=0))) || ((~(B(2,3,6)==2) && ~(M(6)==3)))) ) );
00529          post(p.space(), tt( (!((~(B(3,1,5)==0) && ~(B(3,1,6)!=0))) || ((~(B(3,1,6)==2) && ~(M(6)==1)))) ) );
00530          post(p.space(), tt( (!((~(B(3,2,5)==0) && ~(B(3,2,6)!=0))) || ((~(B(3,2,6)==2) && ~(M(6)==2)))) ) );
00531          post(p.space(), tt( (!((~(B(3,3,5)==0) && ~(B(3,3,6)!=0))) || ((~(B(3,3,6)==2) && ~(M(6)==3)))) ) );
00532 
00533     IntVarArgs b6(69);
00534     for( int i=0;i<69;i++) {
00535         b6[i] = p.var(i);
00536     }
00537     branch(p.space(),b6,INT_VAR_SIZE_MIN,INT_VAL_MIN);
00538     
00539          p.nextScope();
00540          p.QIntVar(69, 1, 3);  // M(7)
00541          p.QIntVar(70, 0, 2);  // B(1,1,7)
00542          p.QIntVar(71, 0, 2);  // B(1,2,7)
00543          p.QIntVar(72, 0, 2);  // B(1,3,7)
00544          p.QIntVar(73, 0, 2);  // B(2,1,7)
00545          p.QIntVar(74, 0, 2);  // B(2,2,7)
00546          p.QIntVar(75, 0, 2);  // B(2,3,7)
00547          p.QIntVar(76, 0, 2);  // B(3,1,7)
00548          p.QIntVar(77, 0, 2);  // B(3,2,7)
00549          p.QIntVar(78, 0, 2);  // B(3,3,7)
00550 
00551          // CGA (Cut-Game Axiom) between time 6 and time 7
00552          // If player "2" won at time 6 then player "1" cannot play
00553 
00554          // Non-winning condition for player 2 at time 6
00555          post(p.space(), tt( (~(B(1,1,6)!=2) || ~(B(1,2,6)!=2) || ~(B(1,3,6)!=2)) ) );
00556          post(p.space(), tt( (~(B(1,1,6)!=2) || ~(B(2,1,6)!=2) || ~(B(3,1,6)!=2)) ) );
00557          post(p.space(), tt( (~(B(1,1,6)!=2) || ~(B(2,2,6)!=2) || ~(B(3,3,6)!=2)) ) );
00558          post(p.space(), tt( (~(B(3,1,6)!=2) || ~(B(2,2,6)!=2) || ~(B(1,3,6)!=2)) ) );
00559          post(p.space(), tt( (~(B(1,2,6)!=2) || ~(B(2,2,6)!=2) || ~(B(3,2,6)!=2)) ) );
00560          post(p.space(), tt( (~(B(1,3,6)!=2) || ~(B(2,3,6)!=2) || ~(B(3,3,6)!=2)) ) );
00561          post(p.space(), tt( (~(B(2,1,6)!=2) || ~(B(2,2,6)!=2) || ~(B(2,3,6)!=2)) ) );
00562          post(p.space(), tt( (~(B(3,1,6)!=2) || ~(B(3,2,6)!=2) || ~(B(3,3,6)!=2)) ) );
00563 
00564          // PA (Precondition Axiom) specifying legal moves at transition 6->7
00565          // A move is valid only if the related colum is not full
00566          post(p.space(), tt( (~(B(3,1,6)==0) || ~(M(7)!=1)) ) );
00567          post(p.space(), tt( (~(B(3,2,6)==0) || ~(M(7)!=2)) ) );
00568          post(p.space(), tt( (~(B(3,3,6)==0) || ~(M(7)!=3)) ) );
00569 
00570          // SSA (Successor State Axiom) linking time 6 to time 7
00571          // The player who moves is "1"
00572 
00573          // If a cell is occupied by player 1, it stays so
00574          post(p.space(), tt( (!(~(B(1,1,6)==1)) || ~(B(1,1,7)==1)) ) );
00575          post(p.space(), tt( (!(~(B(1,2,6)==1)) || ~(B(1,2,7)==1)) ) );
00576          post(p.space(), tt( (!(~(B(1,3,6)==1)) || ~(B(1,3,7)==1)) ) );
00577          post(p.space(), tt( (!(~(B(2,1,6)==1)) || ~(B(2,1,7)==1)) ) );
00578          post(p.space(), tt( (!(~(B(2,2,6)==1)) || ~(B(2,2,7)==1)) ) );
00579          post(p.space(), tt( (!(~(B(2,3,6)==1)) || ~(B(2,3,7)==1)) ) );
00580          post(p.space(), tt( (!(~(B(3,1,6)==1)) || ~(B(3,1,7)==1)) ) );
00581          post(p.space(), tt( (!(~(B(3,2,6)==1)) || ~(B(3,2,7)==1)) ) );
00582          post(p.space(), tt( (!(~(B(3,3,6)==1)) || ~(B(3,3,7)==1)) ) );
00583 
00584          // If a cell is occupied by player 2, it stays so
00585          post(p.space(), tt( (!(~(B(1,1,6)==2)) || ~(B(1,1,7)==2)) ) );
00586          post(p.space(), tt( (!(~(B(1,2,6)==2)) || ~(B(1,2,7)==2)) ) );
00587          post(p.space(), tt( (!(~(B(1,3,6)==2)) || ~(B(1,3,7)==2)) ) );
00588          post(p.space(), tt( (!(~(B(2,1,6)==2)) || ~(B(2,1,7)==2)) ) );
00589          post(p.space(), tt( (!(~(B(2,2,6)==2)) || ~(B(2,2,7)==2)) ) );
00590          post(p.space(), tt( (!(~(B(2,3,6)==2)) || ~(B(2,3,7)==2)) ) );
00591          post(p.space(), tt( (!(~(B(3,1,6)==2)) || ~(B(3,1,7)==2)) ) );
00592          post(p.space(), tt( (!(~(B(3,2,6)==2)) || ~(B(3,2,7)==2)) ) );
00593          post(p.space(), tt( (!(~(B(3,3,6)==2)) || ~(B(3,3,7)==2)) ) );
00594 
00595          // A free cell on top of a free cell stays free
00596          post(p.space(), tt( (!(((~(B(2,1,6)==0) && ~(B(1,1,6)==0)))) || ~(B(2,1,7)==0)) ) );
00597          post(p.space(), tt( (!(((~(B(2,2,6)==0) && ~(B(1,2,6)==0)))) || ~(B(2,2,7)==0)) ) );
00598          post(p.space(), tt( (!(((~(B(2,3,6)==0) && ~(B(1,3,6)==0)))) || ~(B(2,3,7)==0)) ) );
00599          post(p.space(), tt( (!(((~(B(3,1,6)==0) && ~(B(2,1,6)==0)))) || ~(B(3,1,7)==0)) ) );
00600          post(p.space(), tt( (!(((~(B(3,2,6)==0) && ~(B(2,2,6)==0)))) || ~(B(3,2,7)==0)) ) );
00601          post(p.space(), tt( (!(((~(B(3,3,6)==0) && ~(B(2,3,6)==0)))) || ~(B(3,3,7)==0)) ) );
00602 
00603          // A cell that changes value can only turn from "0" to "1" (moving player code)
00604          // ..and at most one such switch can happen in the whole board
00605          post(p.space(), tt( (!((~(B(1,1,6)==0) && ~(B(1,1,7)!=0))) || ((~(B(1,1,7)==1) && ~(M(7)==1)))) ) );
00606          post(p.space(), tt( (!((~(B(1,2,6)==0) && ~(B(1,2,7)!=0))) || ((~(B(1,2,7)==1) && ~(M(7)==2)))) ) );
00607          post(p.space(), tt( (!((~(B(1,3,6)==0) && ~(B(1,3,7)!=0))) || ((~(B(1,3,7)==1) && ~(M(7)==3)))) ) );
00608          post(p.space(), tt( (!((~(B(2,1,6)==0) && ~(B(2,1,7)!=0))) || ((~(B(2,1,7)==1) && ~(M(7)==1)))) ) );
00609          post(p.space(), tt( (!((~(B(2,2,6)==0) && ~(B(2,2,7)!=0))) || ((~(B(2,2,7)==1) && ~(M(7)==2)))) ) );
00610          post(p.space(), tt( (!((~(B(2,3,6)==0) && ~(B(2,3,7)!=0))) || ((~(B(2,3,7)==1) && ~(M(7)==3)))) ) );
00611          post(p.space(), tt( (!((~(B(3,1,6)==0) && ~(B(3,1,7)!=0))) || ((~(B(3,1,7)==1) && ~(M(7)==1)))) ) );
00612          post(p.space(), tt( (!((~(B(3,2,6)==0) && ~(B(3,2,7)!=0))) || ((~(B(3,2,7)==1) && ~(M(7)==2)))) ) );
00613          post(p.space(), tt( (!((~(B(3,3,6)==0) && ~(B(3,3,7)!=0))) || ((~(B(3,3,7)==1) && ~(M(7)==3)))) ) );
00614 
00615     IntVarArgs b7(79);
00616     for( int i=0;i<79;i++) {
00617         b7[i] = p.var(i);
00618     }
00619     branch(p.space(),b7,INT_VAR_SIZE_MIN,INT_VAL_MIN);
00620     
00621          p.nextScope();
00622          p.QIntVar(79, 1, 3);  // M(8)
00623          p.QIntVar(80, 0, 2);  // B(1,1,8)
00624          p.QIntVar(81, 0, 2);  // B(1,2,8)
00625          p.QIntVar(82, 0, 2);  // B(1,3,8)
00626          p.QIntVar(83, 0, 2);  // B(2,1,8)
00627          p.QIntVar(84, 0, 2);  // B(2,2,8)
00628          p.QIntVar(85, 0, 2);  // B(2,3,8)
00629          p.QIntVar(86, 0, 2);  // B(3,1,8)
00630          p.QIntVar(87, 0, 2);  // B(3,2,8)
00631          p.QIntVar(88, 0, 2);  // B(3,3,8)
00632 
00633          // CGA (Cut-Game Axiom) between time 7 and time 8
00634          // If player "1" won at time 7 then player "2" cannot play
00635 
00636          // Non-winning condition for player 1 at time 7
00637          post(p.space(), tt( (~(B(1,1,7)!=1) || ~(B(1,2,7)!=1) || ~(B(1,3,7)!=1)) ) );
00638          post(p.space(), tt( (~(B(1,1,7)!=1) || ~(B(2,1,7)!=1) || ~(B(3,1,7)!=1)) ) );
00639          post(p.space(), tt( (~(B(1,1,7)!=1) || ~(B(2,2,7)!=1) || ~(B(3,3,7)!=1)) ) );
00640          post(p.space(), tt( (~(B(3,1,7)!=1) || ~(B(2,2,7)!=1) || ~(B(1,3,7)!=1)) ) );
00641          post(p.space(), tt( (~(B(1,2,7)!=1) || ~(B(2,2,7)!=1) || ~(B(3,2,7)!=1)) ) );
00642          post(p.space(), tt( (~(B(1,3,7)!=1) || ~(B(2,3,7)!=1) || ~(B(3,3,7)!=1)) ) );
00643          post(p.space(), tt( (~(B(2,1,7)!=1) || ~(B(2,2,7)!=1) || ~(B(2,3,7)!=1)) ) );
00644          post(p.space(), tt( (~(B(3,1,7)!=1) || ~(B(3,2,7)!=1) || ~(B(3,3,7)!=1)) ) );
00645 
00646          // PA (Precondition Axiom) specifying legal moves at transition 7->8
00647          // A move is valid only if the related colum is not full
00648          post(p.space(), tt( (~(B(3,1,7)==0) || ~(M(8)!=1)) ) );
00649          post(p.space(), tt( (~(B(3,2,7)==0) || ~(M(8)!=2)) ) );
00650          post(p.space(), tt( (~(B(3,3,7)==0) || ~(M(8)!=3)) ) );
00651 
00652          // SSA (Successor State Axiom) linking time 7 to time 8
00653          // The player who moves is "2"
00654 
00655          // If a cell is occupied by player 1, it stays so
00656          post(p.space(), tt( (!(~(B(1,1,7)==1)) || ~(B(1,1,8)==1)) ) );
00657          post(p.space(), tt( (!(~(B(1,2,7)==1)) || ~(B(1,2,8)==1)) ) );
00658          post(p.space(), tt( (!(~(B(1,3,7)==1)) || ~(B(1,3,8)==1)) ) );
00659          post(p.space(), tt( (!(~(B(2,1,7)==1)) || ~(B(2,1,8)==1)) ) );
00660          post(p.space(), tt( (!(~(B(2,2,7)==1)) || ~(B(2,2,8)==1)) ) );
00661          post(p.space(), tt( (!(~(B(2,3,7)==1)) || ~(B(2,3,8)==1)) ) );
00662          post(p.space(), tt( (!(~(B(3,1,7)==1)) || ~(B(3,1,8)==1)) ) );
00663          post(p.space(), tt( (!(~(B(3,2,7)==1)) || ~(B(3,2,8)==1)) ) );
00664          post(p.space(), tt( (!(~(B(3,3,7)==1)) || ~(B(3,3,8)==1)) ) );
00665 
00666          // If a cell is occupied by player 2, it stays so
00667          post(p.space(), tt( (!(~(B(1,1,7)==2)) || ~(B(1,1,8)==2)) ) );
00668          post(p.space(), tt( (!(~(B(1,2,7)==2)) || ~(B(1,2,8)==2)) ) );
00669          post(p.space(), tt( (!(~(B(1,3,7)==2)) || ~(B(1,3,8)==2)) ) );
00670          post(p.space(), tt( (!(~(B(2,1,7)==2)) || ~(B(2,1,8)==2)) ) );
00671          post(p.space(), tt( (!(~(B(2,2,7)==2)) || ~(B(2,2,8)==2)) ) );
00672          post(p.space(), tt( (!(~(B(2,3,7)==2)) || ~(B(2,3,8)==2)) ) );
00673          post(p.space(), tt( (!(~(B(3,1,7)==2)) || ~(B(3,1,8)==2)) ) );
00674          post(p.space(), tt( (!(~(B(3,2,7)==2)) || ~(B(3,2,8)==2)) ) );
00675          post(p.space(), tt( (!(~(B(3,3,7)==2)) || ~(B(3,3,8)==2)) ) );
00676 
00677          // A free cell on top of a free cell stays free
00678          post(p.space(), tt( (!(((~(B(2,1,7)==0) && ~(B(1,1,7)==0)))) || ~(B(2,1,8)==0)) ) );
00679          post(p.space(), tt( (!(((~(B(2,2,7)==0) && ~(B(1,2,7)==0)))) || ~(B(2,2,8)==0)) ) );
00680          post(p.space(), tt( (!(((~(B(2,3,7)==0) && ~(B(1,3,7)==0)))) || ~(B(2,3,8)==0)) ) );
00681          post(p.space(), tt( (!(((~(B(3,1,7)==0) && ~(B(2,1,7)==0)))) || ~(B(3,1,8)==0)) ) );
00682          post(p.space(), tt( (!(((~(B(3,2,7)==0) && ~(B(2,2,7)==0)))) || ~(B(3,2,8)==0)) ) );
00683          post(p.space(), tt( (!(((~(B(3,3,7)==0) && ~(B(2,3,7)==0)))) || ~(B(3,3,8)==0)) ) );
00684 
00685          // A cell that changes value can only turn from "0" to "2" (moving player code)
00686          // ..and at most one such switch can happen in the whole board
00687          post(p.space(), tt( (!((~(B(1,1,7)==0) && ~(B(1,1,8)!=0))) || ((~(B(1,1,8)==2) && ~(M(8)==1)))) ) );
00688          post(p.space(), tt( (!((~(B(1,2,7)==0) && ~(B(1,2,8)!=0))) || ((~(B(1,2,8)==2) && ~(M(8)==2)))) ) );
00689          post(p.space(), tt( (!((~(B(1,3,7)==0) && ~(B(1,3,8)!=0))) || ((~(B(1,3,8)==2) && ~(M(8)==3)))) ) );
00690          post(p.space(), tt( (!((~(B(2,1,7)==0) && ~(B(2,1,8)!=0))) || ((~(B(2,1,8)==2) && ~(M(8)==1)))) ) );
00691          post(p.space(), tt( (!((~(B(2,2,7)==0) && ~(B(2,2,8)!=0))) || ((~(B(2,2,8)==2) && ~(M(8)==2)))) ) );
00692          post(p.space(), tt( (!((~(B(2,3,7)==0) && ~(B(2,3,8)!=0))) || ((~(B(2,3,8)==2) && ~(M(8)==3)))) ) );
00693          post(p.space(), tt( (!((~(B(3,1,7)==0) && ~(B(3,1,8)!=0))) || ((~(B(3,1,8)==2) && ~(M(8)==1)))) ) );
00694          post(p.space(), tt( (!((~(B(3,2,7)==0) && ~(B(3,2,8)!=0))) || ((~(B(3,2,8)==2) && ~(M(8)==2)))) ) );
00695          post(p.space(), tt( (!((~(B(3,3,7)==0) && ~(B(3,3,8)!=0))) || ((~(B(3,3,8)==2) && ~(M(8)==3)))) ) );
00696 
00697     IntVarArgs b8(89);
00698     for( int i=0;i<89;i++) {
00699         b8[i] = p.var(i);
00700     }
00701     branch(p.space(),b8,INT_VAR_SIZE_MIN,INT_VAL_MIN);
00702     
00703          p.nextScope();
00704          p.QIntVar(89, 1, 3);  // M(9)
00705          p.QIntVar(90, 0, 2);  // B(1,1,9)
00706          p.QIntVar(91, 0, 2);  // B(1,2,9)
00707          p.QIntVar(92, 0, 2);  // B(1,3,9)
00708          p.QIntVar(93, 0, 2);  // B(2,1,9)
00709          p.QIntVar(94, 0, 2);  // B(2,2,9)
00710          p.QIntVar(95, 0, 2);  // B(2,3,9)
00711          p.QIntVar(96, 0, 2);  // B(3,1,9)
00712          p.QIntVar(97, 0, 2);  // B(3,2,9)
00713          p.QIntVar(98, 0, 2);  // B(3,3,9)
00714          p.QBoolVar(99); // AUX(1)
00715          p.QBoolVar(100); // AUX(2)
00716          p.QBoolVar(101); // AUX(3)
00717          p.QBoolVar(102); // AUX(4)
00718          p.QBoolVar(103); // AUX(5)
00719          p.QBoolVar(104); // AUX(6)
00720          p.QBoolVar(105); // AUX(7)
00721          p.QBoolVar(106); // AUX(8)
00722 
00723          // CGA (Cut-Game Axiom) between time 8 and time 9
00724          // If player "2" won at time 8 then player "1" cannot play
00725 
00726          // Non-winning condition for player 2 at time 8
00727          post(p.space(), tt( (~(B(1,1,8)!=2) || ~(B(1,2,8)!=2) || ~(B(1,3,8)!=2)) ) );
00728          post(p.space(), tt( (~(B(1,1,8)!=2) || ~(B(2,1,8)!=2) || ~(B(3,1,8)!=2)) ) );
00729          post(p.space(), tt( (~(B(1,1,8)!=2) || ~(B(2,2,8)!=2) || ~(B(3,3,8)!=2)) ) );
00730          post(p.space(), tt( (~(B(3,1,8)!=2) || ~(B(2,2,8)!=2) || ~(B(1,3,8)!=2)) ) );
00731          post(p.space(), tt( (~(B(1,2,8)!=2) || ~(B(2,2,8)!=2) || ~(B(3,2,8)!=2)) ) );
00732          post(p.space(), tt( (~(B(1,3,8)!=2) || ~(B(2,3,8)!=2) || ~(B(3,3,8)!=2)) ) );
00733          post(p.space(), tt( (~(B(2,1,8)!=2) || ~(B(2,2,8)!=2) || ~(B(2,3,8)!=2)) ) );
00734          post(p.space(), tt( (~(B(3,1,8)!=2) || ~(B(3,2,8)!=2) || ~(B(3,3,8)!=2)) ) );
00735 
00736          // PA (Precondition Axiom) specifying legal moves at transition 8->9
00737          // A move is valid only if the related colum is not full
00738          post(p.space(), tt( (~(B(3,1,8)==0) || ~(M(9)!=1)) ) );
00739          post(p.space(), tt( (~(B(3,2,8)==0) || ~(M(9)!=2)) ) );
00740          post(p.space(), tt( (~(B(3,3,8)==0) || ~(M(9)!=3)) ) );
00741 
00742          // SSA (Successor State Axiom) linking time 8 to time 9
00743          // The player who moves is "1"
00744 
00745          // If a cell is occupied by player 1, it stays so
00746          post(p.space(), tt( (!(~(B(1,1,8)==1)) || ~(B(1,1,9)==1)) ) );
00747          post(p.space(), tt( (!(~(B(1,2,8)==1)) || ~(B(1,2,9)==1)) ) );
00748          post(p.space(), tt( (!(~(B(1,3,8)==1)) || ~(B(1,3,9)==1)) ) );
00749          post(p.space(), tt( (!(~(B(2,1,8)==1)) || ~(B(2,1,9)==1)) ) );
00750          post(p.space(), tt( (!(~(B(2,2,8)==1)) || ~(B(2,2,9)==1)) ) );
00751          post(p.space(), tt( (!(~(B(2,3,8)==1)) || ~(B(2,3,9)==1)) ) );
00752          post(p.space(), tt( (!(~(B(3,1,8)==1)) || ~(B(3,1,9)==1)) ) );
00753          post(p.space(), tt( (!(~(B(3,2,8)==1)) || ~(B(3,2,9)==1)) ) );
00754          post(p.space(), tt( (!(~(B(3,3,8)==1)) || ~(B(3,3,9)==1)) ) );
00755 
00756          // If a cell is occupied by player 2, it stays so
00757          post(p.space(), tt( (!(~(B(1,1,8)==2)) || ~(B(1,1,9)==2)) ) );
00758          post(p.space(), tt( (!(~(B(1,2,8)==2)) || ~(B(1,2,9)==2)) ) );
00759          post(p.space(), tt( (!(~(B(1,3,8)==2)) || ~(B(1,3,9)==2)) ) );
00760          post(p.space(), tt( (!(~(B(2,1,8)==2)) || ~(B(2,1,9)==2)) ) );
00761          post(p.space(), tt( (!(~(B(2,2,8)==2)) || ~(B(2,2,9)==2)) ) );
00762          post(p.space(), tt( (!(~(B(2,3,8)==2)) || ~(B(2,3,9)==2)) ) );
00763          post(p.space(), tt( (!(~(B(3,1,8)==2)) || ~(B(3,1,9)==2)) ) );
00764          post(p.space(), tt( (!(~(B(3,2,8)==2)) || ~(B(3,2,9)==2)) ) );
00765          post(p.space(), tt( (!(~(B(3,3,8)==2)) || ~(B(3,3,9)==2)) ) );
00766 
00767          // A free cell on top of a free cell stays free
00768          post(p.space(), tt( (!(((~(B(2,1,8)==0) && ~(B(1,1,8)==0)))) || ~(B(2,1,9)==0)) ) );
00769          post(p.space(), tt( (!(((~(B(2,2,8)==0) && ~(B(1,2,8)==0)))) || ~(B(2,2,9)==0)) ) );
00770          post(p.space(), tt( (!(((~(B(2,3,8)==0) && ~(B(1,3,8)==0)))) || ~(B(2,3,9)==0)) ) );
00771          post(p.space(), tt( (!(((~(B(3,1,8)==0) && ~(B(2,1,8)==0)))) || ~(B(3,1,9)==0)) ) );
00772          post(p.space(), tt( (!(((~(B(3,2,8)==0) && ~(B(2,2,8)==0)))) || ~(B(3,2,9)==0)) ) );
00773          post(p.space(), tt( (!(((~(B(3,3,8)==0) && ~(B(2,3,8)==0)))) || ~(B(3,3,9)==0)) ) );
00774 
00775          // A cell that changes value can only turn from "0" to "1" (moving player code)
00776          // ..and at most one such switch can happen in the whole board
00777          post(p.space(), tt( (!((~(B(1,1,8)==0) && ~(B(1,1,9)!=0))) || ((~(B(1,1,9)==1) && ~(M(9)==1)))) ) );
00778          post(p.space(), tt( (!((~(B(1,2,8)==0) && ~(B(1,2,9)!=0))) || ((~(B(1,2,9)==1) && ~(M(9)==2)))) ) );
00779          post(p.space(), tt( (!((~(B(1,3,8)==0) && ~(B(1,3,9)!=0))) || ((~(B(1,3,9)==1) && ~(M(9)==3)))) ) );
00780          post(p.space(), tt( (!((~(B(2,1,8)==0) && ~(B(2,1,9)!=0))) || ((~(B(2,1,9)==1) && ~(M(9)==1)))) ) );
00781          post(p.space(), tt( (!((~(B(2,2,8)==0) && ~(B(2,2,9)!=0))) || ((~(B(2,2,9)==1) && ~(M(9)==2)))) ) );
00782          post(p.space(), tt( (!((~(B(2,3,8)==0) && ~(B(2,3,9)!=0))) || ((~(B(2,3,9)==1) && ~(M(9)==3)))) ) );
00783          post(p.space(), tt( (!((~(B(3,1,8)==0) && ~(B(3,1,9)!=0))) || ((~(B(3,1,9)==1) && ~(M(9)==1)))) ) );
00784          post(p.space(), tt( (!((~(B(3,2,8)==0) && ~(B(3,2,9)!=0))) || ((~(B(3,2,9)==1) && ~(M(9)==2)))) ) );
00785          post(p.space(), tt( (!((~(B(3,3,8)==0) && ~(B(3,3,9)!=0))) || ((~(B(3,3,9)==1) && ~(M(9)==3)))) ) );
00786 
00787          // Winning condition for player 1 at time 9
00788          post(p.space(), tt( (!(BoolExpr(AUX(1))) || (~(B(1,1,9)==1))) ) );
00789          post(p.space(), tt( (!(BoolExpr(AUX(1))) || (~(B(1,2,9)==1))) ) );
00790          post(p.space(), tt( (!(BoolExpr(AUX(1))) || (~(B(1,3,9)==1))) ) );
00791          post(p.space(), tt( (!(BoolExpr(AUX(2))) || (~(B(1,1,9)==1))) ) );
00792          post(p.space(), tt( (!(BoolExpr(AUX(2))) || (~(B(2,1,9)==1))) ) );
00793          post(p.space(), tt( (!(BoolExpr(AUX(2))) || (~(B(3,1,9)==1))) ) );
00794          post(p.space(), tt( (!(BoolExpr(AUX(3))) || (~(B(1,1,9)==1))) ) );
00795          post(p.space(), tt( (!(BoolExpr(AUX(3))) || (~(B(2,2,9)==1))) ) );
00796          post(p.space(), tt( (!(BoolExpr(AUX(3))) || (~(B(3,3,9)==1))) ) );
00797          post(p.space(), tt( (!(BoolExpr(AUX(4))) || (~(B(3,1,9)==1))) ) );
00798          post(p.space(), tt( (!(BoolExpr(AUX(4))) || (~(B(2,2,9)==1))) ) );
00799          post(p.space(), tt( (!(BoolExpr(AUX(4))) || (~(B(1,3,9)==1))) ) );
00800          post(p.space(), tt( (!(BoolExpr(AUX(5))) || (~(B(1,2,9)==1))) ) );
00801          post(p.space(), tt( (!(BoolExpr(AUX(5))) || (~(B(2,2,9)==1))) ) );
00802          post(p.space(), tt( (!(BoolExpr(AUX(5))) || (~(B(3,2,9)==1))) ) );
00803          post(p.space(), tt( (!(BoolExpr(AUX(6))) || (~(B(1,3,9)==1))) ) );
00804          post(p.space(), tt( (!(BoolExpr(AUX(6))) || (~(B(2,3,9)==1))) ) );
00805          post(p.space(), tt( (!(BoolExpr(AUX(6))) || (~(B(3,3,9)==1))) ) );
00806          post(p.space(), tt( (!(BoolExpr(AUX(7))) || (~(B(2,1,9)==1))) ) );
00807          post(p.space(), tt( (!(BoolExpr(AUX(7))) || (~(B(2,2,9)==1))) ) );
00808          post(p.space(), tt( (!(BoolExpr(AUX(7))) || (~(B(2,3,9)==1))) ) );
00809          post(p.space(), tt( (!(BoolExpr(AUX(8))) || (~(B(3,1,9)==1))) ) );
00810          post(p.space(), tt( (!(BoolExpr(AUX(8))) || (~(B(3,2,9)==1))) ) );
00811          post(p.space(), tt( (!(BoolExpr(AUX(8))) || (~(B(3,3,9)==1))) ) );
00812          post(p.space(), tt( (BoolExpr(AUX(1)) || BoolExpr(AUX(2)) || BoolExpr(AUX(3)) || BoolExpr(AUX(4)) || BoolExpr(AUX(5)) || BoolExpr(AUX(6)) || BoolExpr(AUX(7)) || BoolExpr(AUX(8))) ) );
00813 
00814     IntVarArgs b9(99);
00815     for( int i=0;i<99;i++) {
00816         b9[i] = p.var(i);
00817     }
00818     branch(p.space(),b9,INT_VAR_SIZE_MIN,INT_VAL_MIN);
00819     
00820     BoolVarArgs b10(8);
00821     b10[0]=p.bvar(99);
00822     b10[1]=p.bvar(100);
00823     b10[2]=p.bvar(101);
00824     b10[3]=p.bvar(102);
00825     b10[4]=p.bvar(103);
00826     b10[5]=p.bvar(104);
00827     b10[6]=p.bvar(105);
00828     b10[7]=p.bvar(106);
00829     branch(p.space(),b10,INT_VAR_SIZE_MIN,INT_VAL_MIN);
00830     
00831          // Now we set-up the space, define the solver, and run it    
00832          p.makeStructure();
00833     
00834     QSolver solver(&p);
00835 
00836          unsigned long int nodes=0;
00837 
00838          Strategy outcome = solver.solve(nodes);
00839     cout<<nodes<<" nodes crossed."<<endl;
00840 
00841          return 0;
00842 }