This puzzle is a variation of the N-Queens puzzle: we try to place as many bishops as possible on a n by n chess board. In contrast to the N-Queens puzzle, one can place more than one bishop per row. As such, we can now longer represent the positions of the bishops as an total function 1..n >-> 1..n. There are two encodings we show below. The first represents the bishops as a subset of the Cartesian product (1..n)*(1..n), i.e., a set of positions (aka a binary relation on 1..n).
MACHINE NBishopsSets CONSTANTS n, nbishops, hasbishop PROPERTIES n=8 & hasbishop <: (1..n)*(1..n) & !(i,j).(i:1..n & j:1..n => ( (i,j): hasbishop => (!k.(k:(i+1)..n => (k,j+k-i) /: hasbishop & (k,j-k+i) /: hasbishop )) )) & nbishops = card(hasbishop) & nbishops >13 END
One can try and find the maximum number of bishops by gradually increasing the lower limit for nbishops in the last line of the model before the final END. The maximum number of bishops that can be placed is 2*n - 2; see http://mathworld.wolfram.com/BishopsProblem.html.
ProB 1.5.1 can solve this puzzle with nbishops >13 in about half a second.
One can use graphical visualisation features to display the solution, by declaring the ANIMATION FUNCTION inside the DEFINITIONS section as follows:
DEFINITIONS BWOFFSET(x,y) == (x+y) mod 2; ANIMATION_FUNCTION_DEFAULT == ( {r,c,i|r:1..n & c:1..n & i=(r+c) mod 2 } ); ANIMATION_FUNCTION == {r,c,i|(r,c):hasbishop & i= 2+BWOFFSET(r,c)} ; ANIMATION_IMG0 == "ChessPieces/Chess_emptyl45.gif"; ANIMATION_IMG1 == "ChessPieces/Chess_emptyd45.gif"; ANIMATION_IMG2 == "ChessPieces/Chess_bll45.gif"; ANIMATION_IMG3 == "ChessPieces/Chess_bld45.gif"; SET_PREF_TK_CUSTOM_STATE_VIEW_PADDING == 1; END
This will lead to ProB to show the solution graphically, as follows:
For the chess pieces we have used the images available at wikimedia.org. These images are available under the Creative Commons Attribution-Share Alike 3.0 Unported license. The same applies to the screenshots shown here.