// ************************************************************************** // // 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 // // ************************************************************************** // // Connect Four (Vier Gewinnt) // // Here is a short summary of [Alli88], where many important observations // on the Connect-Four game were made. // // The first result is that player White has no winning strategy on boards // with 2n rows and m<=6 columns, since the following rules form a strategy // for player Black to prevent White from winning (stated for 6 columns): // // (1) If White inserts a man in one of the columns {1,2,5,6} at row r, // put a man in the same column at row r+1. // (2) If White inserts a man in one of the columns {3,4} at row 1, // put a man in the other column at row 1. // (3) If White inserts a man in one of the columns {3,4} at row r>1, // put a man in the same column at row r+1. // // Using these rules, Black will have the fields with even rows in columns {1,2,5,6} // and one of the columns in {3,4}, and the fields with odd rows in the other column // of {3,4}. Thus, player White can not have four connected men. // // The above strategy is essentially based on the follow-up rule, which means that // the same column is selected. This way, vertical groups are directly prevented, // and if also horizontal ones are disturbed in some way, there is only the chance // to achieve diagonal groups. However, this is also not possible if the follow-up // rule is played accordingly. Hence, the question concentrates on disturbing the // construction of a horizontal group while following the follow-up rule... // // The follow-up rule tells us furthermore that one of the players can occupy all // the even fields and the other one the odd fields if the number of empty fields // is even. Thus, if a special square is wanted, one can play the follow-up // strategy to finally receive that square... // // Black can also use a follow-up strategy to prevent White from winning on a // 2n x 7 board if White does not start the game in the middle column. // // // However, this does not mean that player Black has a strategy to win. Using // brute-force state space traversals, we found that player Black has a winning // strategy on the 4x6 board, but not on the 4x4 and 4x5 boards. On the 4x5 board, // however, player Black has two winning states of the five possible states that // appear after the first move (of player White) in the game (these are the // corner fields). Hence, Black has still good chances to win on the 4x5 board // as well. // // Moreover, [Alli88] shows that player White has a winning strategy on the // 6x7 board if White follows the following rules: // // (1) If there is a winning move, make it. // (2) If the opponent can win at a square by his next move, play that move first. // (3) Taking the central square is more important than other fields. // (4) Taking corner squares is more important than taking squares on the edges. // // It has been shown in [Alli88] that White has no winning strategy on a 4x7 board, // but it has a winning strategy on a 6x7 board. Moreover, it is easily seen that // White will only save its winning strategy by first inserting a man in the middle // column 3. Otherwise, Black can play the follow-up strategy together with a strategy // to disturb the construction of horizontal groups, and therefore is able to prevent // White from winning. // ------------------------------------------------------------ package ConnectFour; import ConnectFour.*; macro rows = 4; macro cols = 6; module ConnectFour( nat{cols} col_black, ?col_white, [cols][rows]bool black, [cols()][rows()]bool white, event blackHasWon, event whiteHasWon, bool turnWhite, nat{cols} c, nat{rows} r, nat{rows()} !mr) { do { c = (turnWhite?col_white:col_black); // check whether selected row is already full if( !(black[c][rows-1] | white[c][rows-1]) ) { // find the least free row r in column c if(not(black[c][0] or white[c][0])) r = 0; else for( i=1 .. rows-1 ) if(black[c][i-1] or white[c][i-1]) if(not(black[c][i] or white[c][i])) r = i; // insert coin in field [c][r] and check winning cond. if(turnWhite) { next(white[c][r]) = true; HasWon(white,c,r,whiteHasWon); } else { next(black[c][r]) = true; HasWon(black,c,r,blackHasWon); } // toggle turn variable next(turnWhite) = !turnWhite; } pause; } while(!(blackHasWon | whiteHasWon)); }