// ************************************************************************** // // 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 // // ************************************************************************** // // N queens are to be placed on a NxN chessboard so that no queen can // attack another queen. It is known that there are no solutions for // chessboards with N<=6. // // ************************************************************************** macro N = 6; module Queens( [N][N]bool q ) { nothing; } satisfies { s [ProveA]: assert !( // -- each row contains a queen ------------- ( forall(i=0..N-1) exists(j=0..N-1) q[i][j] ) & // -- forbid row attacks -------------------- ( forall(i=0..N-1) forall(j=0..N-1) (q[i][j] -> forall(k=1..N-1) !q[i][(j+k)%N]) ) & // -- forbid column attacks -------------------- ( forall(i=0..N-1) forall(j=0..N-1) (q[i][j] -> forall(k=1..N-1) !q[(i+k)%N][j]) ) & // -- forbid diagonal attacks -------------------- ( forall(i=0..N-1) forall(j=0..N-1) (q[i][j] -> forall(k=1..N-1) !q[(i+k)%N][(j+k)%N]) ) & // -- forbid diagonal attacks -------------------- (forall(i=0..N-1) forall(j=0..N-1) (q[i][j] -> forall(k=1..N-1) !q[(i+k)%N][(N+j-k)%N]) ) ); }