// ************************************************************************** // // eses eses // eses eses // eses eseses esesese eses Embedded Systems Group // ese ese ese ese ese // ese eseseses eseseses ese Department of Computer Science // eses eses ese eses // eses eseses eseseses eses University of Kaiserslautern // eses eses // // ************************************************************************** // // Knight's Tour // // The problem is to find a path for a Knight on a (N)x(N) chessboard, // such that every field is visited exactly once. It is known that // there is a Hamilton circuit (a Knight's Tour where start and end // points are identical) iff N>=6 and N is even. // // A Knight's Tour can be easily obtained by divide and conquer // algorithms or heuristics like Warnsdorff's rule (from 1823). // For further references see the PDF files. // // ************************************************************************** macro N = 4; module KnightsTour( bv{3} move, [N][N()]bool q, nat{N} x, y ) { x = 1; y = 0; always { q[x][y] = true; case (move==0b000) do { if(x>=2 & y>=1) if(!q[x-2][y-1]) { next(x) = x-2; next(y) = y-1; } } (move==0b001) do { if(x>=1 & y>=2) if(!q[x-1][y-2]) { next(x) = x-1; next(y) = y-2; } } (move==0b010) do { if(x<N-1 & y>=2) if(!q[x+1][y-2]) { next(x) = x+1; next(y) = y-2; } } (move==0b011) do { if(x<N-2 & y>=1) if(!q[x+2][y-1]) { next(x) = x+2; next(y) = y-1; } } (move==0b100) do { if(x<N-2 & y<N()-1) if(!q[x+2][y+1]) { next(x) = x+2; next(y) = y+1; } } (move==0b101) do { if(x<N-1 & y<N()-2) if(!q[x+1][y+2]) { next(x) = x+1; next(y) = y+2; } } (move==0b110) do { if(x>=1 & y<N-2) if(!q[x-1][y+2]) { next(x) = x-1; next(y) = y+2; } } (move==0b111) do { if(x>=2 & y<N-1) if(!q[x-2][y+1]) { next(x) = x-2; next(y) = y+1; } } default nothing; } } satisfies { spec[DisProveA] : assert ! E F forall(i=0..N-1) forall(j=0..N()-1) q[i][j]; }