No edit summary |
No edit summary |
||
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: |
The N-Queens is a famous constraint solving benchmark puzzle. It is a generalisation of the original 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.
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
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:
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
This will lead to ProB to show the solution graphically, as follows (the screenshot is unfortunately cropped and does not show all rows):
Instead of using ProB's standard constraint-solving backend, you can also use our Kodkod backend to solve this puzzle.
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:
SET_PREF_KODKOD == TRUE
However, using the MiniSat backend solving the N-queens puzzle for n=40 takes 57.1 seconds (on the same hardware as above).