"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. \n",
"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).\n",
"\n",
"The challenge is to place two equal-sized armies of white and black queens onto a chessboard. We can distinguish between two problems:\n",
"\n",
"* checking whether two armies of n queens can be placed on a dim*dim chessboard,\n",
"\n",
"* 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.\n",
"\n",
"In this notebook, we take a look at both of the problems and visualize them with the `ANIMATION_FUNCTION`."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Checking\n",
"\n",
"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`.\n",
"\n",
"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. \n",
"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.\n",
"\n",
"Try it out! Reload the machine and run the next cell. Then, initialise and visualise as ususal.\n",
"\n",
"You can change the collums of the queens with the constants `blackc`/`whitec` and the rows with the constants `blackr`/`whiter`."
]
},
{
"cell_type": "code",
"execution_count": 15,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Machine constants set up using operation 0: $setup_constants()"
]
},
"execution_count": 15,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":constants blackc(2)=2 & blackr(2)=6"
]
},
{
"cell_type": "code",
"execution_count": 19,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Machine constants set up using operation 0: $setup_constants()"
]
},
"execution_count": 19,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":constants whitec(2)=4 & whiter(2)=4"
]
},
{
"cell_type": "code",
"execution_count": 20,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Machine initialised using operation 1: $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.\n",
"\n",
"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.\n",
"\n",
"To find out how long our jupyter notebook kernel needs to run this, we can use the command `:time`:\n",
"\n",
"Times and specs:\n",
"```\n",
"Acer TravelMate X349-G2-M, \n",
"8 GB RAM, \n",
"Intel(R) Core(TM) i5-7200U CPU @ 2.50GHz 2.70 GHz Prozessor, \n",
"Windows 10 OS\n",
"\n",
"dim=5 --> optimum n=4 0.326799900 secs\n",
"dim=6 --> optimum n=5 0.954069900 secs\n",
"dim=7 --> optimum n=7 19.829867700 secs\n",
"dim=8 --> optimum n=9 658.281314000 secs\n",
"```\n",
"\n",
"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.\n",
"\n",
"*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."
"Enter a B expression or predicate to evaluate it. To load a B machine, enter its source code directly, or use `:load` to load an external machine file.\n",
"\n",
"You can also use any of the following commands. For more help on a particular command, run `:help commandname`.\n",
"\n",
"## Evaluation\n",
"\n",
"* `:eval` - Evaluate a formula and display the result.\n",
"* `:solve` - Solve a predicate with the specified solver.\n",
"* `:table` - Display an expression as a table.\n",
"* `:type` - Display the static type of a formula.\n",
"* `:prettyprint` - Pretty-print a predicate.\n",
"* `:let` - Evaluate an expression and store it in a local variable.\n",
"* `:unlet` - Remove a local variable.\n",
"* `:assert` - Ensure that the predicate is true, and show an error otherwise.\n",
"\n",
"## Animation\n",
"\n",
"* `::load` - Load a B machine from the given source code.\n",
"* `:load` - Load a machine from a file.\n",
"* `:constants` - Set up the current machine's constants.\n",
"* `:init` - Initialise the current machine with the specified predicate\n",
"* `:exec` - Execute an operation.\n",
"* `:browse` - Show information about the current state.\n",
"* `:trace` - Display all states and executed operations in the current trace.\n",
"* `:goto` - Go to the state with the specified index in the current trace.\n",
"* `:find` - Try to find a state for which the given predicate is true (in addition to the machine's invariant).\n",
"\n",
"## Visualisation\n",
"\n",
"* `:show` - Show the machine's animation function visualisation for the current state.\n",
"* `:dot` - Execute and show a dot visualisation.\n",
"\n",
"## Verification\n",
"\n",
"* `:check` - Check the machine's properties, invariant, or assertions in the current state.\n",
"* `:modelcheck` - Run the ProB model checker on the current model.\n",
"\n",
"## Other\n",
"\n",
"* `::render` - Render some content with the specified MIME type.\n",
"* `:bsymb` - Load all bsymb.sty command definitions, so that they can be used in $\\LaTeX$ formulas in Markdown cells.\n",
"* `:groovy` - Evaluate the given Groovy expression.\n",
"* `:help` - Display help for a specific command, or general help about the REPL.\n",
"* `:pref` - View or change the value of one or more preferences.\n",
"* `:stats` - Show statistics about the state space.\n",
"* `:time` - Execute the given command and measure how long it takes to execute.\n",
"* `:version` - Display version info about the ProB CLI and ProB 2.\n"
],
"text/plain": [
"Enter a B expression or predicate to evaluate it. To load a B machine, enter its source code directly, or use :load to load an external machine file.\n",
"You can also use any of the following commands. For more help on a particular command, run :help commandname.\n",
"\n",
"Evaluation:\n",
":eval - Evaluate a formula and display the result.\n",
":solve - Solve a predicate with the specified solver.\n",
":table - Display an expression as a table.\n",
":type - Display the static type of a formula.\n",
":prettyprint - Pretty-print a predicate.\n",
":let - Evaluate an expression and store it in a local variable.\n",
":unlet - Remove a local variable.\n",
":assert - Ensure that the predicate is true, and show an error otherwise.\n",
"\n",
"Animation:\n",
"::load - Load a B machine from the given source code.\n",
":load - Load a machine from a file.\n",
":constants - Set up the current machine's constants.\n",
":init - Initialise the current machine with the specified predicate\n",
":exec - Execute an operation.\n",
":browse - Show information about the current state.\n",
":trace - Display all states and executed operations in the current trace.\n",
":goto - Go to the state with the specified index in the current trace.\n",
":find - Try to find a state for which the given predicate is true (in addition to the machine's invariant).\n",
"\n",
"Visualisation:\n",
":show - Show the machine's animation function visualisation for the current state.\n",
":dot - Execute and show a dot visualisation.\n",
"\n",
"Verification:\n",
":check - Check the machine's properties, invariant, or assertions in the current state.\n",
":modelcheck - Run the ProB model checker on the current model.\n",
"\n",
"Other:\n",
"::render - Render some content with the specified MIME type.\n",
":bsymb - Load all bsymb.sty command definitions, so that they can be used in $\\LaTeX$ formulas in Markdown cells.\n",
":groovy - Evaluate the given Groovy expression.\n",
":help - Display help for a specific command, or general help about the REPL.\n",
":pref - View or change the value of one or more preferences.\n",
":stats - Show statistics about the state space.\n",
":time - Execute the given command and measure how long it takes to execute.\n",
":version - Display version info about the ProB CLI and ProB 2.\n"
]
},
"execution_count": 22,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":help"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
}
],
"metadata": {
"kernelspec": {
"display_name": "ProB 2",
"language": "prob",
"name": "prob2"
},
"language_info": {
"codemirror_mode": "prob2_jupyter_repl",
"file_extension": ".prob",
"mimetype": "text/x-prob2-jupyter-repl",
"name": "prob"
}
},
"nbformat": 4,
"nbformat_minor": 4
}
%% Cell type:markdown id: tags:
# Peaceable Armies of Queens
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
:constants blackc(2)=2 & blackr(2)=6
```
%% Output
Machine constants set up using operation 0: $setup_constants()
%% Cell type:code id: tags:
``` prob
:constants whitec(2)=4 & whiter(2)=4
```
%% Output
Machine constants set up using operation 0: $setup_constants()
%% Cell type:code id: tags:
``` prob
:init
```
%% Output
Machine initialised using operation 1: $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.
Enter a B expression or predicate to evaluate it. To load a B machine, enter its source code directly, or use `:load` to load an external machine file.
You can also use any of the following commands. For more help on a particular command, run `:help commandname`.
## Evaluation
* `:eval` - Evaluate a formula and display the result.
* `:solve` - Solve a predicate with the specified solver.
* `:table` - Display an expression as a table.
* `:type` - Display the static type of a formula.
* `:prettyprint` - Pretty-print a predicate.
* `:let` - Evaluate an expression and store it in a local variable.
* `:unlet` - Remove a local variable.
* `:assert` - Ensure that the predicate is true, and show an error otherwise.
## Animation
* `::load` - Load a B machine from the given source code.
* `:load` - Load a machine from a file.
* `:constants` - Set up the current machine's constants.
* `:init` - Initialise the current machine with the specified predicate
* `:exec` - Execute an operation.
* `:browse` - Show information about the current state.
* `:trace` - Display all states and executed operations in the current trace.
* `:goto` - Go to the state with the specified index in the current trace.
* `:find` - Try to find a state for which the given predicate is true (in addition to the machine's invariant).
## Visualisation
* `:show` - Show the machine's animation function visualisation for the current state.
* `:dot` - Execute and show a dot visualisation.
## Verification
* `:check` - Check the machine's properties, invariant, or assertions in the current state.
* `:modelcheck` - Run the ProB model checker on the current model.
## Other
* `::render` - Render some content with the specified MIME type.
* `:bsymb` - Load all bsymb.sty command definitions, so that they can be used in $\LaTeX$ formulas in Markdown cells.
* `:groovy` - Evaluate the given Groovy expression.
* `:help` - Display help for a specific command, or general help about the REPL.
* `:pref` - View or change the value of one or more preferences.
* `:stats` - Show statistics about the state space.
* `:time` - Execute the given command and measure how long it takes to execute.
* `:version` - Display version info about the ProB CLI and ProB 2.
Enter a B expression or predicate to evaluate it. To load a B machine, enter its source code directly, or use :load to load an external machine file.
You can also use any of the following commands. For more help on a particular command, run :help commandname.
Evaluation:
:eval - Evaluate a formula and display the result.
:solve - Solve a predicate with the specified solver.
:table - Display an expression as a table.
:type - Display the static type of a formula.
:prettyprint - Pretty-print a predicate.
:let - Evaluate an expression and store it in a local variable.
:unlet - Remove a local variable.
:assert - Ensure that the predicate is true, and show an error otherwise.
Animation:
::load - Load a B machine from the given source code.
:load - Load a machine from a file.
:constants - Set up the current machine's constants.
:init - Initialise the current machine with the specified predicate
:exec - Execute an operation.
:browse - Show information about the current state.
:trace - Display all states and executed operations in the current trace.
:goto - Go to the state with the specified index in the current trace.
:find - Try to find a state for which the given predicate is true (in addition to the machine's invariant).
Visualisation:
:show - Show the machine's animation function visualisation for the current state.
:dot - Execute and show a dot visualisation.
Verification:
:check - Check the machine's properties, invariant, or assertions in the current state.
:modelcheck - Run the ProB model checker on the current model.
Other:
::render - Render some content with the specified MIME type.
:bsymb - Load all bsymb.sty command definitions, so that they can be used in $\LaTeX$ formulas in Markdown cells.
:groovy - Evaluate the given Groovy expression.
:help - Display help for a specific command, or general help about the REPL.
:pref - View or change the value of one or more preferences.
:stats - Show statistics about the state space.
:time - Execute the given command and measure how long it takes to execute.
:version - Display version info about the ProB CLI and ProB 2.
