"Machine constants set up using operation 0: $setup_constants()"
"Changed to state with index -1"
]
},
"execution_count": 15,
"execution_count": 5,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":goto -1"
]
},
{
"cell_type": "code",
"execution_count": 6,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Machine constants set up using operation 2: $setup_constants()"
]
},
"execution_count": 6,
"metadata": {},
"output_type": "execute_result"
}
...
...
@@ -264,16 +284,36 @@
},
{
"cell_type": "code",
"execution_count": 19,
"execution_count": 7,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Machine constants set up using operation 0: $setup_constants()"
"Changed to state with index -1"
]
},
"execution_count": 19,
"execution_count": 7,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":goto -1"
]
},
{
"cell_type": "code",
"execution_count": 8,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Machine constants set up using operation 4: $setup_constants()"
]
},
"execution_count": 8,
"metadata": {},
"output_type": "execute_result"
}
...
...
@@ -284,16 +324,16 @@
},
{
"cell_type": "code",
"execution_count": 20,
"execution_count": 9,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Machine initialised using operation 1: $initialise_machine()"
"Machine initialised using operation 5: $initialise_machine()"
]
},
"execution_count": 20,
"execution_count": 9,
"metadata": {},
"output_type": "execute_result"
}
...
...
@@ -304,7 +344,7 @@
},
{
"cell_type": "code",
"execution_count": 21,
"execution_count": 10,
"metadata": {},
"outputs": [
{
...
...
@@ -397,7 +437,7 @@
"<Animation function visualisation>"
]
},
"execution_count": 21,
"execution_count": 10,
"metadata": {},
"output_type": "execute_result"
}
...
...
@@ -438,7 +478,7 @@
},
{
"cell_type": "code",
"execution_count": 9,
"execution_count": 11,
"metadata": {},
"outputs": [
{
...
...
@@ -447,7 +487,7 @@
"Loaded machine: JustQueens_FindOptimal_CBC"
]
},
"execution_count": 9,
"execution_count": 11,
"metadata": {},
"output_type": "execute_result"
}
...
...
@@ -506,16 +546,16 @@
},
{
"cell_type": "code",
"execution_count": 10,
"execution_count": 12,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"Execution time: 17.606007400 seconds"
"Execution time: 10.936093583 seconds"
],
"text/plain": [
"Execution time: 17.606007400 seconds"
"Execution time: 10.936093583 seconds"
]
},
"metadata": {},
...
...
@@ -527,7 +567,7 @@
"Machine constants set up using operation 0: $setup_constants()"
]
},
"execution_count": 10,
"execution_count": 12,
"metadata": {},
"output_type": "execute_result"
}
...
...
@@ -538,7 +578,7 @@
},
{
"cell_type": "code",
"execution_count": 11,
"execution_count": 13,
"metadata": {},
"outputs": [
{
...
...
@@ -547,7 +587,7 @@
"Machine initialised using operation 1: $initialise_machine()"
]
},
"execution_count": 11,
"execution_count": 13,
"metadata": {},
"output_type": "execute_result"
}
...
...
@@ -558,7 +598,7 @@
},
{
"cell_type": "code",
"execution_count": 12,
"execution_count": 14,
"metadata": {},
"outputs": [
{
...
...
@@ -570,7 +610,7 @@
"7"
]
},
"execution_count": 12,
"execution_count": 14,
"metadata": {},
"output_type": "execute_result"
}
...
...
@@ -581,7 +621,7 @@
},
{
"cell_type": "code",
"execution_count": 13,
"execution_count": 15,
"metadata": {},
"outputs": [
{
...
...
@@ -657,7 +697,7 @@
"<Animation function visualisation>"
]
},
"execution_count": 13,
"execution_count": 15,
"metadata": {},
"output_type": "execute_result"
}
...
...
%% Cell type:markdown id: tags:
# Peaceable Armies of Queens
Use `:help` to get an overview for the jupyter notebook commands. If you need more insight on how to use this tool, consider reading *ProB Jupyter Notebook Overview*.
The paper [Models and symmetry breaking for 'peaceable armies of queens'](https://link.springer.com/chapter/10.1007/978-3-540-24664-0_19) by Smith, Petrie and Gent describes a challenging constraint programming problem.
A variation of the problem can be found on page 329 of the [Handbook on Constraint Programming](https://www.elsevier.com/books/handbook-of-constraint-programming/rossi/978-0-444-52726-4).
The challenge is to place two equal-sized armies of white and black queens onto a chessboard. We can distinguish between two problems:
* checking whether two armies of n queens can be placed on a dim*dim chessboard,
* for a given board of size dim*dim find the maximal size n of armies that can be placed onto the board, i.e., solving an optimisation problem.
In this notebook, we take a look at both of the problems and visualize them with the `ANIMATION_FUNCTION`.
%% Cell type:markdown id: tags:
## Checking
First we will take a look at the model for the checking problem. This problem is quite straightforward to encode in B. Most of the lines in the DEFINITIONS section are for our visualization with the `ANIMATION_FUNCTION`.
We will load (`::load`), set up the constants (`:constants`), and initialize the machine (`:init`), before we visualize it (`:show`).
This machine is a great one to understand setting up various constants within jupyter notebook.
If you reload the machine (by pressing `SHIFT`+`ENTER` in the code cell with our machine code) you can change the constants for the queens to change their positions on the board.
Try it out! Reload the machine and run the next cell. Then, initialise and visualise as ususal.
You can change the collums of the queens with the constants `blackc`/`whitec` and the rows with the constants `blackr`/`whiter`.
%% Cell type:code id: tags:
``` prob
:goto -1
```
%% Output
Changed to state with index -1
%% Cell type:code id: tags:
``` prob
:constants blackc(2)=2 & blackr(2)=6
```
%% Output
Machine constants set up using operation 0: $setup_constants()
Machine constants set up using operation 2: $setup_constants()
%% Cell type:code id: tags:
``` prob
:goto -1
```
%% Output
Changed to state with index -1
%% Cell type:code id: tags:
``` prob
:constants whitec(2)=4 & whiter(2)=4
```
%% Output
Machine constants set up using operation 0: $setup_constants()
Machine constants set up using operation 4: $setup_constants()
%% Cell type:code id: tags:
``` prob
:init
```
%% Output
Machine initialised using operation 1: $initialise_machine()
Machine initialised using operation 5: $initialise_machine()
One can obviously use the above model to try and manually find a maximal value of n for a given board size dim. Below, we have encoded this process as B constraints, by setting up the problem twice: once for the army size n and a second time for army size n+1. The second encoding is wrapped into a negated existential quantification.
ProB solves this optimisation problem in about 660 seconds for a board size of 8. This is very competitive with the timings reported in the above mentioned constraint solving paper using new symmetry breaking techniques and much more low-level encoding on state of the art constraint solving libraries such as ILOG.
To find out how long our jupyter notebook kernel needs to run this, we can use the command `:time`:
Times and specs:
```
Acer TravelMate X349-G2-M,
8 GB RAM,
Intel(R) Core(TM) i5-7200U CPU @ 2.50GHz 2.70 GHz Prozessor,
Windows 10 OS
dim=5 --> optimum n=4 0.326799900 secs
dim=6 --> optimum n=5 0.954069900 secs
dim=7 --> optimum n=7 19.829867700 secs
dim=8 --> optimum n=9 658.281314000 secs
```
If you want to check out the optimization for dim=5, dim=6, dim=8, you can do so by changing the constant in the `PROPERTIES` section of the machine code cell.
*EDITOR'S NOTE* : 660 seconds are 11 minutes, and that is why we only recomment to work with dim=5, dim=6 and dim=7 for the purposes of this notebook. However, if you really want to try out dim=8... You know how to.
