{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# N-Bishops Puzzle\n",
    "\n",
    "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*.\n",
    "\n",
    "This puzzle is a variation of the N-Queens puzzle. You can find the N-Queens puzzle in our modeling examples as well. In this 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`. \n",
    "\n",
    "There are two encodings shown below. The first and following 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`).\n",
    "\n",
    "First of all we have to load the machine, if you are struggeling with any operation of our jupyter kernel, try out `:help` or take a look at our `ProB Jupyter Noteboook Overview`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Loaded machine: NBishopsSets"
      ]
     },
     "execution_count": 1,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "::load\n",
    "MACHINE NBishopsSets\n",
    "CONSTANTS n, nbishops, hasbishop\n",
    "PROPERTIES\n",
    " n=8 &\n",
    " hasbishop <: (1..n)*(1..n) &\n",
    " !(i,j).(i:1..n & j:1..n\n",
    "    =>\n",
    "    ( (i,j): hasbishop\n",
    "       =>\n",
    "        (!k.(k:(i+1)..n =>\n",
    "           (k,j+k-i) /: hasbishop &\n",
    "           (k,j-k+i) /: hasbishop\n",
    "        ))\n",
    "    ))\n",
    " & nbishops = card(hasbishop)\n",
    " & nbishops >13\n",
    "END"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "One can try and find the maximum number of bishops by gradually\n",
    "increasing the lower limit for nbishops in the last line of the model\n",
    "before the final END. The maximum number of bishops that can be placed\n",
    "is 2*n - 2; see [here](http://mathworld.wolfram.com/BishopsProblem.html).\n",
    "\n",
    "To show this graphically, we will now include the ANIMATION_FUNCTION for this example. The ANIMATION_FUNCTION has to be declared in the `DEFINITIONS` section as follows:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Loaded machine: NBishopsSets"
      ]
     },
     "execution_count": 2,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "::load\n",
    "MACHINE NBishopsSets\n",
    "DEFINITIONS\n",
    "      BWOFFSET(x,y) == (x+y) mod 2;\n",
    "      ANIMATION_FUNCTION_DEFAULT == ( {r,c,i|r:1..n & c:1..n & i=(r+c) mod 2 }  );\n",
    "      ANIMATION_FUNCTION == {r,c,i|(r,c):hasbishop & i= 2+BWOFFSET(r,c)} ;\n",
    "      ANIMATION_IMG0 == \"images/ChessPieces/Chess_emptyl45.gif\";\n",
    "      ANIMATION_IMG1 == \"images/ChessPieces/Chess_emptyd45.gif\";\n",
    "      ANIMATION_IMG2 == \"images/ChessPieces/Chess_bll45.gif\";\n",
    "      ANIMATION_IMG3 == \"images/ChessPieces/Chess_bld45.gif\";\n",
    "     SET_PREF_TK_CUSTOM_STATE_VIEW_PADDING == 1;\n",
    "CONSTANTS n, nbishops, hasbishop\n",
    "PROPERTIES\n",
    " n=8 &\n",
    " hasbishop <: (1..n)*(1..n) &\n",
    " !(i,j).(i:1..n & j:1..n\n",
    "    =>\n",
    "    ( (i,j): hasbishop\n",
    "       =>\n",
    "        (!k.(k:(i+1)..n =>\n",
    "           (k,j+k-i) /: hasbishop &\n",
    "           (k,j-k+i) /: hasbishop\n",
    "        ))\n",
    "    ))\n",
    " & nbishops = card(hasbishop)\n",
    " & nbishops >13\n",
    "END"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We will now initialise the machine and run the default setting to take a look at the animation."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Machine constants set up using operation 0: $setup_constants()"
      ]
     },
     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":constants"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Machine initialised using operation 1: $initialise_machine()"
      ]
     },
     "execution_count": 4,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":init"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "With the `:show` command from the jupyter kernel you can see the results of the N-Queens problem for yourself.\n",
    "\n",
    "Please note, that the image paths given in the DEFINITIONS have to be relative to the jupyter notebook."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "<table style=\"font-family:monospace\"><tbody>\n",
       "<tr>\n",
       "<td style=\"padding:1px\"><img alt=\"2\" src=\"images/ChessPieces/Chess_bll45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"3\" src=\"images/ChessPieces/Chess_bld45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"2\" src=\"images/ChessPieces/Chess_bll45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"3\" src=\"images/ChessPieces/Chess_bld45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"2\" src=\"images/ChessPieces/Chess_bll45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"3\" src=\"images/ChessPieces/Chess_bld45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"2\" src=\"images/ChessPieces/Chess_bll45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"3\" src=\"images/ChessPieces/Chess_bld45.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:1px\"><img alt=\"1\" src=\"images/ChessPieces/Chess_emptyd45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"2\" src=\"images/ChessPieces/Chess_bll45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"3\" src=\"images/ChessPieces/Chess_bld45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"2\" src=\"images/ChessPieces/Chess_bll45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"3\" src=\"images/ChessPieces/Chess_bld45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"2\" src=\"images/ChessPieces/Chess_bll45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"3\" src=\"images/ChessPieces/Chess_bld45.gif\"/></td>\n",
       "<td style=\"padding:1px\"><img alt=\"0\" src=\"images/ChessPieces/Chess_emptyl45.gif\"/></td>\n",
       "</tr>\n",
       "</tbody></table>"
      ],
      "text/plain": [
       "<Animation function visualisation>"
      ]
     },
     "execution_count": 5,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":show"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "For the chess pieces we have used the images available at [this site](https://commons.wikimedia.org/wiki/Category:SVG_chess_pieces). These images are available under the [Creative Commons](https://en.wikipedia.org/wiki/Creative_Commons)\n",
    "[Attribution-Share Alike 3.0 Unported license](https://creativecommons.org/licenses/by-sa/3.0/deed.en). The same applies to the screenshots shown here."
   ]
  },
  {
   "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": 2
}