N-Queens - Revision history

Michael Leuschel at 15:54, 20 February 2014

2014-02-20T15:54:11Z

← Older revision		Revision as of 15:54, 20 February 2014
Line 18:		Line 18:
	ProB 1.3.7 can solve this puzzle in about 0.150 seconds (for n=40, on a 1.7 GHz Mac Book Air).		ProB 1.3.7 can solve this puzzle in about 0.150 seconds (for n=40, on a 1.7 GHz Mac Book Air).

	One can use graphical visualisation features to display the solution, by declaring the ANIMATION FUNCTION as follows:		One can use [[Graphical_Visualization\|graphical visualisation]] features to display the solution, by declaring the ANIMATION FUNCTION as follows:

	<pre>		<pre>
Line 45:		Line 45:


	Instead of using ProB's standard constraint-solving backend, you can also use our Kodkod backend to solve this puzzle.		Instead of using ProB's standard constraint-solving backend, you can also use our [[Using_ProB_with_KODKOD\|Kodkod backend]] to solve this puzzle.
	To do this, either "Enable Kodkod for Properties" in the ProB Tcl/Tk "Preferences" menu or		To do this, either "Enable Kodkod for Properties" in the ProB Tcl/Tk "Preferences" menu or
	add the following to the DEFINITIONS in the machine file above:		add the following to the DEFINITIONS in the machine file above:

Michael Leuschel at 15:52, 20 February 2014

2014-02-20T15:52:31Z

@@ Line 1: / Line 1: @@
 The N-Queens is a famous constraint solving benchmark puzzle.
 It is a generalisation of the original [http://en.wikipedia.org/wiki/Eight_queens_puzzle eight queens puzzle], where the goal is to place eight queens on a 8*8 chessboard so that no two queens attach each other.
@@ Line 44: / Line 43: @@
 [[File:ProB_Queens_40_Screenshot.png|600px|center]]

Michael Leuschel: Created page with ' The N-Queens is a famous constraint solving benchmark puzzle. It is a generalisation of the original [http://en.wikipedia.org/wiki/Eight_queens_puzzle eight queens puzzle], wher…'

2014-02-20T15:46:44Z

Created page with ' The N-Queens is a famous constraint solving benchmark puzzle. It is a generalisation of the original [http://en.wikipedia.org/wiki/Eight_queens_puzzle eight queens puzzle], wher…'

New page

The N-Queens is a famous constraint solving benchmark puzzle.
It is a generalisation of the original [http://en.wikipedia.org/wiki/Eight_queens_puzzle eight queens puzzle], where the goal is to place eight queens on a 8*8 chessboard so that no two queens attach each other.

Here is one way to encode the N-Queens puzzle in B.

<pre>
MACHINE NQueens
CONSTANTS n,queens
PROPERTIES
n = 40 &
queens : 1..n >-> 1..n /* for each column the row in which the queen is in */
&
!(q1,q2).(q1:1..n & q2:2..n & q2>q1
=> queens(q1)+q2-q1 /= queens(q2) & queens(q1)-q2+q1 /= queens(q2))
END
</pre>

ProB 1.3.7 can solve this puzzle in about 0.150 seconds (for n=40, on a 1.7 GHz Mac Book Air).

One can use graphical visualisation features to display the solution, by declaring the ANIMATION FUNCTION as follows:

<pre>
MACHINE NQueens40
CONSTANTS n,queens
PROPERTIES
n = 40 &
queens : 1..n >-> 1..n /* for each column the row in which the queen is in */
&
!(q1,q2).(q1:1..n & q2:2..n & q2>q1
=> queens(q1)+q2-q1 /= queens(q2) & queens(q1)-q2+q1 /= queens(q2))
DEFINITIONS
ANIMATION_FUNCTION_DEFAULT == ( {r,c,i|r:1..n & c:1..n & i=(r+c) mod 2 } );
ANIMATION_FUNCTION == ( {r,c,i|c:1..n & r=queens(c) & i=2+((r+c) mod 2) } );
ANIMATION_IMG0 == "images/sm_empty_box.gif";
ANIMATION_IMG1 == "images/sm_gray_box.gif";
ANIMATION_IMG2 == "images/sm_queen_white.gif";
ANIMATION_IMG3 == "images/sm_queen_black.gif";
SET_PREF_CLPFD == TRUE;
END
</pre>

This will lead to ProB to show the solution graphically, as follows (the screenshot is unfortunately cropped and does not show all rows):

[[File:ProB_Queens_40_Screenshot.png|600px|center]]