2019_06_Hooks5-z3.ipynb

{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {
    "id": "Oq1xibzMT1Wl"
   },
   "outputs": [],
   "source": [
    "import numpy as np\n",
    "import pandas as pd\n",
    "import time\n",
    "import seaborn as sns\n",
    "import matplotlib.pyplot as plt\n",
    "import requests\n",
    "from bs4 import BeautifulSoup\n",
    "import itertools\n",
    "from z3 import *\n",
    "from scipy.ndimage import measurements\n",
    "from IPython.display import Markdown, display,Image,HTML"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {
    "id": "ICTfvjZUT1Wr"
   },
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "The grid presented here can be partitioned into 9 L-shaped “hooks”. The largest\n",
       "is 9-by-9 (contains 17 squares), the next largest is 8-by-8 (contains 15\n",
       "squares), and so on. The smallest hook is just a single square. Find where the\n",
       "hooks are located, and place nine 9’s in the largest hook, eight 8’s in the\n",
       "next-largest, etc., down to one 1 in the smallest hook. The filled squares must form a connected region. (Squares are “connected” if\n",
       "they are orthogonally adjacent.) A number outside the grid indicates the sum of the first consecutive block of\n",
       "filled squares when looking in that direction. (As shown in the example.)\n",
       "Furthermore, every 2-by-2 region must contain at least one unfilled square. The answer to this puzzle is the product of the areas of the connected groups of\n",
       "empty squares in the completed grid."
      ],
      "text/plain": [
       "<IPython.core.display.Markdown object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "url='https://www.janestreet.com/puzzles/hooks-5-index/'\n",
    "res = requests.get(url)\n",
    "soup = BeautifulSoup(res.content, 'html.parser')\n",
    "x =[text for text in soup.body.stripped_strings]\n",
    "#display([(i,j) for i,j in enumerate(x)])\n",
    "display(Markdown(\" \".join(x[11:15])))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "id": "U9Yh1D3HT1Ws"
   },
   "source": [
    "### Puzzle details\n",
    "<img src=\"https://www.janestreet.com/puzzles/hooks_5.png\" width=\"300\" height=\"300\">"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {
    "id": "0VI0NM6ET1Wt"
   },
   "outputs": [],
   "source": [
    "#Setup the constraints\n",
    "top_labels  = [41, 8, 0, 0,14, 0,15, 0, 0]\n",
    "bot_labels  = [ 0, 9, 0,17, 0,15, 0,35, 0]\n",
    "left_labels = [ 0, 0,25, 0,15, 0,26, 0, 0]\n",
    "right_labels =[25, 0, 0, 0,10, 0, 0, 0,27]\n",
    "params = [top_labels,bot_labels,left_labels,right_labels]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {
    "id": "844RhDFpT1Wu"
   },
   "outputs": [],
   "source": [
    "def sol_print(solved,matrix):\n",
    "    fig,ax = plt.subplots(1,1,figsize=(4,4))\n",
    "    x = np.array((solved*matrix).astype('int').astype('str'))\n",
    "    x[x==\"0\"] =\"\"\n",
    "    ax =sns.heatmap(solved,annot=x,cbar=False,cmap=\"tab10\",fmt=\"\",linewidths=2,linecolor='k',annot_kws={\"fontsize\":12,\"color\":\"k\"},alpha=.6)\n",
    "    ax.tick_params(left=False, bottom=False,labelleft=False, labelright=True)\n",
    "    ax.axis(\"off\")\n",
    "    plt.tight_layout()\n",
    "    plt.show()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {
    "id": "844RhDFpT1Wu"
   },
   "outputs": [],
   "source": [
    "def neigh(x,y,N):\n",
    "    return [(i+x,j+y) for i,j in [(-1,0),(0,-1),(1,0),(0,1)] if i+x >=0 and i+x <N and j+y >=0 and j+y <N]\n",
    "\n",
    "def areas(grid):\n",
    "    labels, num = measurements.label(np.logical_not(grid!=0))\n",
    "    areas = measurements.sum(np.logical_not(grid!=0), labels, index=range(1, num+1))\n",
    "    print(areas)\n",
    "    return np.prod(areas)\n",
    "\n",
    "def numbers(split,line,hook_line):\n",
    "    block = 0\n",
    "    inblock =0\n",
    "    for n,p in enumerate(split):         \n",
    "        if p ==1:\n",
    "            if inblock == 0:\n",
    "                block += line[n]*hook_line[n]\n",
    "                inblock = 1\n",
    "            else:\n",
    "                block += line[n]*hook_line[n]         \n",
    "        else:\n",
    "            if inblock == 1:\n",
    "                yield block\n",
    "                block = 0\n",
    "                inblock = 0                    \n",
    "    if inblock == 1:\n",
    "        yield block\n",
    "            \n",
    "def constraint(line,hook_line,split,param):\n",
    "    nums =[i for i in numbers(split,line,hook_line)]\n",
    "    return Implies(And([line[i] == int(e) for i,e in enumerate(split)]),nums[0] == param)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {
    "colab": {
     "base_uri": "https://localhost:8080/",
     "height": 374
    },
    "id": "zexQ8t1kT1W3",
    "outputId": "7c2aec4e-d2fb-45d8-fc7e-679051faafed"
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "setup done in 8.30 seconds\n"
     ]
    },
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAARgAAAEYCAYAAACHjumMAAAAOXRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjUuMSwgaHR0cHM6Ly9tYXRwbG90bGliLm9yZy/YYfK9AAAACXBIWXMAAAsTAAALEwEAmpwYAAAmbUlEQVR4nO3de3gU9b0/8M/c9jI7mxsLIZdNICGrSZZLDAlWjUi5iLUI+alRGgXx9Hl+tfV5WnugYpsDR4sELVHRcnrBG6dHfQS8FMSqRy1U4EdQBIGsEshlE0xCNpuE7CY72d2Z+f3hSX8+fZK0vzLf78TZz+uvbJZn3t8vmbyZGXbmy2iaBgghRAJr9AAQQuaFBYMQIgYLBiFEDBYMQogYLBiEEDH8eG+WzxN9tAYyorkpmuF2CyBYmE4zZyZaLs6VTu6AuwQYi5VqLgDAcP2hotG+P27BAADU1mZ8pP9wxnZHlb+Kdq4RmYmWi3Oll5u65ddUc/vW318x1nt4ioQQIgYLBiFEDBYMQogYLBiEEDFYMAghYrBgEELEYMEghIjBgkEIEYMFgxAi5u9+kveb4ty5Yalua6CivT2WzvGgzJ5lb96wMf2IIDDEnqhlRCaiI5H2p+ip4ykDT9Vep3RccLGiQxar7z3quLW6VY9tm+YIpm5roMLpZCO79+T+4T/+I2vP+fPDGc/u6C02WyaiI1H2Jy0WZS49/OCNlpIy/5S3Ptop/eAnfwn/btu3ow2fJeuxfdMUTF+f4rx+vtQkiqySnW2JFBbZ2tvao6lmy0R0JMr+FDtzMkUNDzicP1p3muEFzb5kWQefM70rsnd3gR7bN03BLFosnT54IDwjHFJ4f2tU9DXIOXPniu1my0R0JMr+pGkaM8p3mfgFf5oe2zfNNZh588TOgwcGCysr/Ws0DZiSEltjZWVSq9kyER2Jsj9Ziuf0M6IUCT29Zbbzvn89LX/wp8x4a1MGP31Ghx7bN8URjKJosHHDxe+UXGVv2btv2nMvvezeOTSkWR/d1D3PTJmIjkTanxirVU2u2fxu9LNPcgKVC+4eeuOVWcLMkiY2NW1Qj+2bomACgbgtFFKlNWtSG+x2Vk1PF4YXLpLONjTIOWbKRHQk2v5kLb261/XC6/umvH1k56Qdr76tBgNJfEFhtx7bNkXBTJ0qyMnJbGjnzr6iWExjgsG45cMPwp7MTCFopkxER6LtT8PHj6apQ4OcGhrgB7bVzlJDA6Ljru+f1WPbprkGs/6hKe/99jfBa1Ysb53DsqDm5Vk61q6bfMRsmYiORNqfIm+9XtBf80AhqArL5+Z1pm5+ej9rF1U9tm2agikrE4NlZeI+s2ciOhJpf0rZ+Hg9ANST2LYpTpEQQhMTFgxCiBgsGIQQMVgwCCFisGAQQsRgwSCEiMGCQQgRgwWDECKG0bSxH5blcvF9FMcCAADhsCoCAC9J7ICZMxMtF+dKJ3cYLDwrJVHNBQBQerpHfW7NuJ/kdbsFMqMZR1tbjJekLGBZegdXw8M9fFpaGtXMRMvFudLJVad7ALiJc2IybsEIFqaztjbjI1qDAQC4o8pfxbIsrF69ehetzLq6OuqZiZaLc6WTCxwLaU/soJrbt/7+irHemzhVhxAyHSwYhBAxWDAIIWKwYBBCxGDBIISIwYJBCBGDBYMQIgYLBiFEjGmeyUvbpk2b7v36a0VROI/H41u5cuVho8ZEUiLNN5HmCgAQPXU8ZeCp2uuUjgsuVnTIYvW9Rx23VrfqsW0smH9STU3N8yNfRyIRvq6ubpXX620yckwkJdJ8E2muWizKXHr4wRutNyz2OX//yn75w3cyBrb+cqlwpfc1S/HsS5e7fTxF0kF9fX2e1WqNeL3eLqPHQkMizdfsc42dOZmihgcczh+tO83wgmZfsqyDz5neFdm7u0CP7WPB6MDn83kKCgoaGWaUdcRNKJHma/a5apo2ysQ0Jn7Bn6bH9rFgLlNXV5cUCAQyysvLG40eCw2JNN9EmKuleE4/I0qR0NNbZmvDw2zk7Tez461NGRCN6nL5BK/BXKZjx44VuFyurszMzJDRY6EhkeabCHNlrFY1uWbzu6FfP35toHLBHC7LHRBmljQxgoArO04EjY2NntLS0pNGj4OWRJpvoszVWnp1r/WF1/+6omTPquXLrRULdTlqw1Oky+Dz+dJlWXaUl5c3Gz0WGhJpvok01+HjR9PUoUFODQ3wA9tqZ6mhAdFx1/fP6rFtPIK5DCdOnPC43e4Wh8MRM3osNCTSfBNprpG3Xi/or3mgEFSF5XPzOlM3P72ftYt4imS06upqqk/7M1oizTeR5pqy8fF6AKgnsW08RUIIEYMFgxAiBgsGIUQMFgxCiBgsGIQQMVgwCCFisGAQQsRgwSCEiMGCQQgRw2iaNuabLhffR3EsAAAQDquionC8zWYboJUpy7IIAFQzEy0X50onN85xPCslUc0FAFB6ulNH+/64twq43QKZ0YyjrS3GS1ImsCy9g6uenh6+OCWfaiYAwPmgn89RI8Aputz28Q9r1jQ+12KhmmtEplG5zZrGO1OTgaX8kKrueIyXC4oBuIlzYjJuwQgWprO2NoPqPRl3VPmrWJaF1atX76KVWVdXV8WyLOxauY1aJgDA3O2VVRww8GJODtXc+efPUc81ItOo3Pnnz1WxDAP3Lbia6lwf2ft+FXAspD2xg2pu3/r7K8Z6b+JUHULIdLBgEELEYMEghIjBgkEIEYMFgxAiBgsGIUQMFgxCiBgsGIQQMaZ46PemTZvu/fprRVE4j8fjW7ly5WHS2duPvpT/wvE9pb2RASnJ6hh6ZNGPD9xSuJDKOsYnI5GkVW3+20vsYvPOnJw/mzXTyNxEED11PGXgqdrrlI4LLlZ0yGL1vUcdt1a36rFtUxRMTU3N8yNfRyIRvq6ubpXX620infvqqf1Zvzv2yrzHlv7s/SUzru1u6m0XSWd+3cMXu65zWywBs2camWt2WizKXHr4wRutNyz2OX//yn75w3cyBrb+cqlwpfc1S/HsS5e7fdOdItXX1+dZrdaI1+slfhSx/ehLc++es+L4TZ7ruzmWA49r2pDHNW2IdC4AwLPBYL7IstHZNtuXNPKMyjQyNxHEzpxMUcMDDueP1p1meEGzL1nWwedM74rs3V2gx/ZNVzA+n89TUFDQyBC+0SymxJm2/o7JwUi/veSZ5Xd6t91cvea19dcODIc5osEAEIzHhf/s6527MT39/5DOMjLTyNxEoWnaKL8oGhO/4E/TY/umKpiuri4pEAhklJeX67Ku7nha+7+0K5rKftTycd6e7z2z90/3PPtac2+76xfvPXkV6ex/v9hVtlByfuGx2gZJZxmZaWRuorAUz+lnRCkSenrLbG14mI28/WZ2vLUpA6JRXS6fmKpgjh07VuByuboyMzNDpLMkixgHALjNu/RM/qScIXdyhlw955ZTn1w4nUMy99BgeNIZWc762ZQpp0nmGJ1pZG4iYaxWNblm87vRzz7JCVQuuHvojVdmCTNLmtjUNF0K3RQXeUc0NjZ6SktLT9LIynBOjqbYnIMMw4z9xC4C/hIezOxVFOf8pvPVAABRTRNUTWMWNzWl/nd+/utmyTQyN9FYS6/utb7w+r6R1z2rli+3VizU5SzANAXj8/nSZVl2lJeXN9PKXJh/zdndZ97xVhYtbrfwFvXlk/tmlrtn+Ulm3u9yff691NTzI6+fCgRmd8fjzsczyD23x4hMI3MTzfDxo2lC4cxLoChM+PntRWpoQHTc9f2zemzbNAVz4sQJj9vtbnE4HDFamVuWrv30B29usC16/p47BZZXvpVT0vTo4p+eIJmZxHHxJI6Lj7wWWSYmMEw822KRzZRpZG6iibz1ekF/zQOFoCosn5vXmbr56f2sXdTlEYCmKZjq6mrq/6rZeKv64m2PHQKAQ7SzR2zOyDyeCJlG5ppdysbH6wGgnsS2TXWRFyE0sWDBIISIwYJBCBGDBYMQIgYLBiFEDBYMQogYLBiEEDFYMAghYhhNG/tWGpeL76M4FgAACIdVUVE46ouV88DxyTaJ6qLhl+SwqClRPollqeaGVFXUAKjmGpFpVG5IVUWFZXi7IFCdayQWE2O8wLNSEtVcAAClpzt1tO+P+0let1sgM5pxtLXFeEnKpLoQfU9PD1+ckk81EwDgfNDPD2ZxMMTRXSQ91iHz1nQr1VwjMkdy50QtwAG93OboMO9MTQaW8DOJ/lZ3KMxDQTEAN3FOTMYtGMHCdNbW0r2x7I4qfxXLsrB69WpqC3jX1dVVsSwLu1Zuo7po+NztlVUMx8D0B6dTzf3iJ19QzzUicySXAwZezMmhljv//LkqlmHgvgVXU53rI3vfrwKOhbQndlDN7Vt/f8VY702cqkMImQ4WDEKIGCwYhBAxWDAIIWKwYBBCxGDBIISIwYJBCBGDBYMQIsYUz+TdtGnTvV9/rSgK5/F4fCtXrjxs1JjMpmVLy4KIP5KlxTWBE7mh1OtTP0u/Nf0Lo8dlJr965+CyQGhwyshSOKJFGNx4y6JXSedGTx1PGXiq9jql44KLFR2yWH3vUcet1a16bNsUBVNTU/P8yNeRSISvq6tb5fV6m4wck9lMXj75pDhdPMjaWHWwcTDF/6R/mZgv9jjnOHuMHpuZLLgy//BNM6+gVtxaLMpcevjBG603LPY5f//KfvnDdzIGtv5yqXCl9zVL8exLl7t9050i1dfX51mt1ojX6+0yeixmIhVKfayN/WopCwY0ANDkDjnJ2FGhyxU7czJFDQ84nD9ad5rhBc2+ZFkHnzO9K7J3d4Ee2zfFEczX+Xw+T0FBQSND+UazROB/0n9d+EzYoykaL7iEntSK1Dajx2Q2h861lH90rqU82W67tKio4FhpblYnyTxN00b5RdGY+AV/mh7bN1XBdHV1SYFAIGPFihUHjR6LGeU+kHtIi2uHB44PpIcbwhmsldVlcS70lZu8V9RPc6X2CTynHDzbPGP3x6eWTpYcr+VMSiH2+AVL8Zx+RpQioae3zHbe96+n5Q/+lBlvbcrgp8/o0GP7pjpFOnbsWIHL5erKzMwMGT0Ws2J4Rkuel9wV649JF/dcLDJ6PGbizZ7aLdmsMSvPq0uKPY1TkqSLJ9s73CQzGatVTa7Z/G70s09yApUL7h5645VZwsySJjY1bVCP7ZvqCKaxsdFTWlp60uhxJAQVmGhPFK/BkKVpQP5BNtbSq3utL7y+b+R1z6rly60VCxv12LZpjmB8Pl+6LMuO8vLyZqPHYjbR7qgtsD+QHw/FeS2uMb0He7MHvxicIRVKXxo9NrO4FJEt9c1t2XIszsUVlXnfd37GxYFQxqzsqe2ks4ePH01ThwY5NTTAD2yrnaWGBkTHXd8/q8e2TXMEc+LECY/b7W5xOBwxo8diOgxA/+H+ou4/dleABgzn5EKupa4jkxZP8hs9NLOIKyr7wedNZW982pDCMKAl2239t5bOfHe6K+2y/6v474m89XpBf80DhaAqLJ+b15m6+en9rF3U5fqaaQqmurqa6pP3EollskUu2Fyw7+//SfTPmiSJ8s9vXvCGEdkpGx+vB4B6Ets2zSkSQmjiwYJBCBGDBYMQIgYLBiFEDBYMQogYLBiEEDFYMAghYrBgEELEYMEghIhhNE0b802Xi++jOBYAAAiHVVFRON5msxG7Rf1vybIs8sDxyTaJWiYAwCU5LA4zUZ5zcFRzlSFFBA2o5hqROZJriQGfxLLUckOqKiosw9sFgepcI7GYGOMFnpWSqOYCACg93amjfX/cWwXcboHMaMbR1hbjJSkTWJbewVVPTw9fnJJPNRMA4HzQz7NZHDAc3YdjyR0yf00yAM+O/Y+L3j6PA9+XUgTActQyAQDUWDvv5WTgyN+U/FfN0WHemZoMLOWHnnWHwjwUFANwE+fEZNyCESxMZ21tBtV7fO6o8lexLAurV6/eRSuzrq6uimVZ2LVyG7VMAIC52yurGI6B6Q9Op5r7xU++qOJZDT5c7aCWm1UXqgKWg6krN1Oda/v2VVUcMPBiTg613Pnnz1WxDAP3Lbia6lwf2ft+FXAspD2xg2pu3/r7K8Z6b+JUHULIdLBgEELEYMEghIjBgkEIEYMFgxAiBgsGIUQMFgxCiBgsGIQQMbo/9PvcuWGpbmugor09ls7xoMyeZW/esDH9iCAwxD42umnTpnu//lpRFM7j8fhWrlx5mFSmkVq2tCyI+CNZWlwTOJEbSr0+9bP0W9OpLZhOU++HzxVHGo9cER8IpNlyZp5Pv/PRA7SyT0YiSava/LeX2MXmnTk5fyad96t3Di4LhAanMMxXvyuiRRjceMuiV0nnkqR7wdRtDVQ4nWxk957cP/T2xi3r1nbe/OyO3uL7fjjpjN5ZI2pqap4f+ToSifB1dXWrvF5vE6k8o01ePvmkOF08yNpYdbBxMMX/pH+ZmC/2OOc4e4wem95456RB59zln8otn2ZrSozqKhgPX+y6zm2xBGhmLrgy//BNM68wzT8Wup8i9fUpzuvnS02iyCrZ2ZZIYZGtva09OuqNUCTU19fnWa3WiNfr7aKVSZtUKPWxtv9ZF5oBDQA0uUM25SqLSWUrWpPm3tLK2qRhmrnPBoP5IstGZ9tsuLjcZdD9X4RFi6XTBw+EZyy4wdEZDCoWX4Occ3tVysd654zF5/N5CgoKGhnKN5rR5n/Sf134TNijKRovuISe1IrUNqPHZBbBeFz4z77euc+63W+92Nt7Jc3sQ+dayj8611KebLddWlRUcKw0N6uTZr7edC+YefPEzoMHBgsrK/1rNA2YkhJbY2VlUqveOaPp6uqSAoFAxooVKw7SyDNS7gO5h7S4dnjg+EB6uCGcwVpZXVbiQwD/frGrbKHk/MJjtemyAPw/6ibvFfXTXKl9As8pB882z9j98amlkyXHazmTUqg/fkEvup4iKYoGGzdc/E7JVfaWvfumPffSy+6dQ0Oa9dFN3fP0zBnLsWPHClwuV1dmZmaIRp7RGJ7Rkucld8X6Y9LFPReLjB6PGRwaDE86I8tZP5sy5TTtbG/21G7JZo1ZeV5dUuxpnJIkXTzZ3uGmPQ496XoEEwjEbaGQKq1Zk9pgt7Oq3c4OL1wknd31an8ZEFqa8usaGxs9paWlJ0nnTDgqMNGeqCmvwdD2l/BgZq+iOOc3na8GAIhqmqBqGrO4qSn1v/PzX6c8HE0Dig+yIUDXI5ipUwU5OZkN7dzZVxSLaUwwGLd8+EHYk5kpBPXMGY3P50uXZdlRXl7eTDrLSNHuqC2wP5AfD8V5La4xvQd7swe/GJwhFUqmvBipxWOMOjzEaZrKaJr61dfxGLFfuvtdrs//OG36K7typ+3ZlTttzw0Oyee12dtecLvfJpUJAHApIlvqm9uy5Viciysq877v/IyLA6GMWdlT20nmkqb7NZj1D01577e/CV6zYnnrHJYFNS/P0rF23eQjeuf8rRMnTnjcbneLw+GIkc4yFAPQf7i/qPuP3RWgAcM5uZBrqevIpMWT/EYPjYTgu7++avDMB6Ujr9ufqipweBced938wHESeUkcF0/iuPjIa5FlYgLDxLMtFplE3oi4orIffN5U9sanDSkMA1qy3dZ/a+nMd6e70i6RzCVN94IpKxODZWXiPr23+/dUV1dTffKeUSyTLXLB5gLqf79Gcd38ALEy+Udszsikkj1JEuWf37zgDRpZNOGtAgghYrBgEELEYMEghIjBgkEIEYMFgxAiBgsGIUQMFgxCiBgsGIQQMYymjf2gOZeL76M4FgAACIdVUVE43mazUbuDVJZlkQeOT7ZJVO9avSSHxWEmasiC8DZV41NtDLXcflkTh8DCs5T/jlU5LFqVGJ/EstRyQ6oqKizD2wWB6lwjsZgY4wWelZKo332t9HSP+syncT/J63YLZEYzjra2GC9JmVQXou/p6eGLU/KpZgIAnA/6eTaLA4ajez+b3CHzc5MBeIrT/bxH5UvTFOBZup98/7xH5bMUG3AU7xlsjg7zztRkYCk/k6g7FOahoBiAmzgnJuMWjGBhOmtrM6h+BP+OKn8Vy7KwevVqagt419XVVbEsC7tWbqO6aPjc7ZVVDMfA9AenU8394idfVPGsBh+udlDLzaoLVfEsUM0cyeWAgRdzcqjlzj9/roplGLhvwdVU5/rI3vergGMh7YkdVHP71t9fMdZ7E6fqEEKmgwWDECIGCwYhRAwWDEKIGCwYhBAxWDAIIWKwYBBCxGDBIISIwYJBCBGj+0O/z50bluq2Bira22PpHA/K7Fn25g0b048IAjP2TU/o/0vLlpYFEX8kS4trAidyQ6nXp36Wfms6sQXTw1GN/V+vDlV82qlmhaOadarEDDxUYT32v0stRJfUMCrXKL965+CyQGhwCsN89bsiWoTBjbcsetXocV0O3QumbmugwulkI7v35P6htzduWbe28+Znd/QW3/fDSWf0zkpUk5dPPilOFw+yNlYdbBxM8T/pXybmiz3OOc4eEnlRBdhMJxvessi2d1Y6G/798VjOj/8kLyrL5HZflcGFSWQamWukBVfmH75p5hXE/rGgTfdTpL4+xXn9fKlJFFklO9sSKSyytbe1R0e90xL9c6RCqY+1/c9a1AxoAKDJHTKxlR3T7Ez8xRX241dlcGGeZeCHZZa2KQ4mdKA1PplUppG5SD+6H8EsWiydPnggPGPBDY7OYFCx+BrknNurUj7WOyfR+Z/0Xxc+E/ZoisYLLqEntSK1jVb2uaBq7wxryWWZHNXHeRiVS9Ohcy3lH51rKU+22y4tKio4Vpqb1Wn0mC6H7gUzb57YefDAYGFlpX+NpgFTUmJrrKxMatU7J9HlPpB7SItrhweOD6SHG8IZrPV/jmgIi8Q09tZdQ99enMc3VuTy/TQyjcyl6SbvFfXTXKl9As8pB882z9j98amlkyXHazmTUqg/30Uvup4iKYoGGzdc/E7JVfaWvfumPffSy+6dQ0Oa9dFN3fP0zEFfYXhGS56X3BXrj0kX91wsIp0XVzVY8l9DC3gW1Neq7IdJ5xmdS5s3e2q3ZLPGrDyvLin2NE5Jki6ebO9wGz2uy6FrwQQCcVsopEpr1qQ22O2smp4uDC9cJJ1taJBz9MxBf0MFJtoTJXYNBgBA1TS46b+G5vdFNPufVzveswsMlSMmo3InCE0Dik/KIkDXgpk6VZCTk9nQzp19RbGYxgSDccuHH4Q9mZlCUM+cRBbtjtoC+wP58VCc1+Ia03uwN3vwi8EZUqH0JcncZS9HKlovaakH7hHfSbYxCsmsiZBL26WIbKlvbsuWY3EurqjM+77zMy4OhDJmZU/9Rv+XvO7XYNY/NOW93/4meM2K5a1zWBbUvDxLx9p1k4/onZOwGID+w/1F3X/srgANGM7JhVxLXUcmLZ7kJxV5skuR3j4fL+RZULKfCK8a+f6/zbf+5RcV1vNmyzVCXFHZDz5vKnvj04YUhgEt2W7rv7V05rvTXWl0nzGqM90LpqxMDJaVifv03i76imWyRS7YXED173fOVC6sbUz6Pc1MI3ONMEkS5Z/fvOANo8ehN7xVACFEDBYMQogYLBiEEDFYMAghYrBgEELEYMEghIjBgkEIEYMFgxAihtG0sR8053Lx1G+LD4dVUVE43mazUbuDVJZlkQeOT7ZJVO9avSSHxWEmynMOjmquMqSINlXjU20Mtdx+WRM1AKqZI7mKwvBJLEstN6SqosIyvF0QqM41EouJMV7gWSmJ+t3XSk/3qM98GveTvG63QGY042hri/GSlAksS+/gqqenhy9OyaeaCQBwPujnM+wOYBm697N1s2HelUQ3NxQP8y6J/lxD8TCfnkI3Vw6F+QwD5todCvNQUAzATZwTk3ELRrAwnbW1GR/RGgwAwB1V/iqWZWH16tW7aGXW1dVVsSwLu1Zuo5YJADB3e2UVywDct+BqqrmP7H2/imUYqrlGZBqVa+RcgWMh7YkdVHP71t9fMdZ7E6fqEEKmgwWDECIGCwYhRAwWDEKIGCwYhBAxWDAIIWKwYBBCxGDBIISI0f2ZvOfODUt1WwMV7e2xdI4HZfYse/OGjelHBIEZ+56Ey7Rp06Z7v/5aURTO4/H4Vq5cSXwNne1HX8p/4fie0t7IgJRkdQw9sujHB24pXNhFMtOMi6Qjc/5cdS+Yuq2BCqeTjezek/uH3t64Zd3azpuf3dFbfN8PJ53RO2tETU3N8yNfRyIRvq6ubpXX620ilTfi1VP7s3537JV5jy392ftLZlzb3dTbLpLOHGG2RdLRV8z2c9W9YPr6FOfN3006I4qsIoqWSGGRrb2tPTrqjVAk1NfX51mt1ojX6yV6FAEAsP3oS3PvnrPi+E2e67sBADyuaUOkMxH6JtG9YBYtlk4fPBCeseAGR2cwqFh8DXLO7VUpH+udMxafz+cpKChoZAjfaBZT4kxbf8fkYKTfX/LM8jtjapwry57Zuu27NUeTrBLxBcLMtkg6+orZfq66F8y8eWLnwQODhZWV/jWaBkxJia2xsjKpVe+c0XR1dUmBQCBjxYoVB0lntfZ/aVc0lf2o5eO8Pd97Zq+FF9S7dq298RfvPXnVM8v+jWihmnGRdGTOn6uu/4ukKBps3HDxOyVX2Vv27pv23Esvu3cODWnWRzd1z9MzZyzHjh0rcLlcXZmZmSHSWZJFjAMA3OZdeiZ/Us6QOzlDrp5zy6lPLpwmvg63GRdJR+b8uepaMIFA3BYKqdKaNakNdjurpqcLwwsXSWcbGmTiv3QAAI2NjZ6ioqJGGlkZzsnRFJtzcOSKv8G+8Yuko1F943+uuhbM1KmCnJzMhnbu7CuKxTQmGIxbPvwg7MnMFIJ65ozG5/Oly7LsKC8vbyadNWJh/jVnd595x+vv+9LWGQpYXj65b2a5exaxNaIBzLtIeqIz689V92sw6x+a8t5vfxO8ZsXy1jksC2penqVj7brJR/TO+VsnTpzwuN3uFofDESOdNWLL0rWf/uDNDbZFz99zp8DyyrdySpoeXfzTEyQzzbpIeqIz689V94IpKxODZWUi1cXZAQCqq6upPnkPAMDGW9UXb3vsEAAcopVp1kXSE51Zf654qwBCiBgsGIQQMVgwCCFisGAQQsRgwSCEiMGCQQgRgwWDECIGCwYhRAwWDEKIGEbTxr5Xz+Xi+yiOBQAAwmFVVBSOt9ls1G5Rl2VZ5IHjk20S1dviL8lhUdFivF0QqOZGYjERAKjmGpFpVK6Rc43xAs9KSdQf76D0dI/6ULlxbxVwuwUyoxlHW1uMl6RMYFl6B1c9PT18cUo+1UwAgPNBP5+X6k6IXJwrndz+vGkA3MQ5MRm3YAQL01lbm0H1Hp87qvxVLMvC6tWrd9HKrKurq2JZFnat3EYtEwBg7vbKhMnFudLJBY6FtCd2UM3tW39/xVjvTZyqQwiZDhYMQogYLBiEEDFYMAghYrBgEELEYMEghIjBgkEIEYMFgxAiRveHfp87NyzVbQ1UtLfH0jkelNmz7M0bNqYfEYQJsX6QaWw/+lL+C8f3lPZGBqQkq2PokUU/PnBL4UKi63EbkWlkrhHMNlfdC6Zua6DC6WQju/fk/qG3N25Zt7bz5md39Bbf98NJZ/TOSlSvntqf9btjr8x7bOnP3l8y49rupt520YyZRuYawYxz1b1g+voU583fTTojiqwiipZIYZGtva09OuqNUOifs/3oS3PvnrPi+E2e67sBADyuaUNmzDQy1whmnKvuBbNosXT64IHwjAU3ODqDQcXia5Bzbq9KIboYfCKJKXGmrb9jcjDS7y95ZvmdMTXOlWXPbN323ZqjSVZJMUumkblGMOtcdb/IO2+e2NnVFU+trPSv+Zd/uXCX2y0EKiuTWvXOSVSt/V/aFU1lP2r5OG/P957Z+6d7nn2tubfd9Yv3nrzKTJlG5hrBrHPVtWAURYONGy5+p+Qqe8vefdOee+ll986hIc366KbueXrmJDLJIsYBAG7zLj2TPylnyJ2cIVfPueXUJxdO55gp08hcI5h1rroWTCAQt4VCqrRmTWqD3c6q6enC8MJF0tmGBvkb/Zc0kWQ4J0dTbM5BhqH3v3JGZBqZawSzzlXXgpk6VZCTk9nQzp19RbGYxgSDccuHH4Q9mZlCUM+cRLcw/5qzu8+84/X3fWnrDAUsL5/cN7PcPctvtkwjc41gxrnqfpF3/UNT3vvtb4LXrFjeOodlQc3Ls3SsXTf5iN45iWzL0rWf/uDNDbZFz99zp8DyyrdySpoeXfzTE2bLNDLXCGacq+4FU1YmBsvKxH16bxf9Pzbeqr5422OHAOCQmTONzDWCGeeKtwoghIjBgkEIEYMFgxAiBgsGIUQMFgxCiBgsGIQQMVgwCCFisGAQQsQwmjb2rQ8uF99HcSwAABAOq6KicLzNZqO2gLcsyyIPHJ9sk6guGn5JDosAkBC5OFc6uTIHPCslUc0FAFB6ukd95tO4n+QdcJeQGc044m0tPJ+VC8MUF/BW2lp4JisXeikvGj4y10TIxbnSyRWycgEo545n3IJhLNbO1C2//ojWYAAAArcvob6AtxGZiZaLczVvbt/6+yvGem/iVB1CyHSwYBBCxGDBIISIwYJBCBGDBYMQIgYLBiFEDBYMQogYLBiEEDG6P5M3eup4ysBTtdcpHRdcrOiQxep7jzpurW7VO2ei5CKyEml/MuM+rOsRjBaLMpcefvBGS0mZf8pbH+2UfvCTv4R/t+3b0YbPkvXMmSi5iKxE2p/Mug/rWjCxMydT1PCAw/mjdacZXtDsS5Z18DnTuyJ7dxfomTNRchFZibQ/mXUf1vcIRtOYUb7LxC/40/TMmSi5iKxE2p/Mug/rWjCW4jn9jChFQk9vma0ND7ORt9/Mjrc2ZUA0qvu1nomQi8hKpP3JrPuwroNnrFY1uWbzu6FfP35toHLBHC7LHRBmljQxgqDqmTNRchFZibQ/mXUf1r0draVX91pfeP2vKzv2rFq+3FqxsFHvnImSi8hKpP3JjPuw7p+DGT5+NE0dGuTU0AA/sK12lhoaEB13ff+s3jkTJReRlUj7kxn3Yd2PYCJvvV7QX/NAIagKy+fmdaZufno/axeJH+YZlYvISqT9yYz7sO4Fk7Lx8XoAqNd7uxM1F5GVSPuTGfdhvFUAIUQMFgxCiBgsGIQQMVgwCCFisGAQQsRgwSCEiMGCQQgRgwWDECIGCwYhRAyjadqYb1rnXeejOBYAAIg3NWZw7lxgLNZOM2cmWi7O1by5AADD9YeKRvv+uAWDEEKXA0+REELEYMEghIjBgkEIEYMFgxAiBgsGIUQMFgxCiJj/C++M/k/4pri8AAAAAElFTkSuQmCC\n",
      "text/plain": [
       "<Figure size 288x288 with 1 Axes>"
      ]
     },
     "metadata": {
      "needs_background": "light"
     },
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Took 19.4440 seconds\n",
      "[5. 5. 5. 5. 1. 5. 5. 5.]\n",
      "solution is 78,125\n"
     ]
    }
   ],
   "source": [
    "start = time.time()\n",
    "N =9\n",
    "#set up the solver and variables.\n",
    "s = Tactic(\"qffd\").solver()\n",
    "\n",
    "# H== hooks\n",
    "H = np.array(IntVector(\"h\",N**2),dtype=object).reshape((N,N))\n",
    "\n",
    "row_fix =IntVector(\"r\",N)\n",
    "col_fix =IntVector(\"c\",N)\n",
    "\n",
    "s += [And(e>0,e<=N) for (i,j),e in np.ndenumerate(H)]\n",
    "s += [And(e>=0,e<N) for e in row_fix+col_fix]\n",
    "\n",
    "s += Distinct(row_fix)\n",
    "s += Distinct(col_fix)\n",
    "\n",
    "for n in range(1,N+1):\n",
    "    s+=PbEq([(e==n,1) for _,e in np.ndenumerate(H)],2*n-1)\n",
    "    if n!=1:\n",
    "        s+=PbEq([(If(e==int(n),Sum([H[k,l] ==int(n) for k,l in neigh(i,j,N)]),0)==1,1) for (i,j),e in np.ndenumerate(H)],2)\n",
    "        \n",
    "for n in range(N):\n",
    "    s += [Implies(e == int(n+1),Or(i == row_fix[n],j == col_fix[n])) for (i,j),e in np.ndenumerate(H)]\n",
    "    \n",
    "\n",
    "# Y = filled    \n",
    "Y = np.array(IntVector(\"y\",N**2),dtype=object).reshape((N,N))\n",
    "s += [Or(e==0,e==1) for (i,j),e in np.ndenumerate(Y)]\n",
    "\n",
    "for n in range(1,N+1):\n",
    "    s+=PbEq([(And(e==n,Y[i,j]==1),1) for (i,j),e in np.ndenumerate(H)],n)\n",
    "\n",
    "# no 2x2\n",
    "s += [Or(Y[i,j] ==0,Y[i+1,j] ==0,Y[i,j+1] ==0,Y[i+1,j+1] ==0) for j in range(N-1) for i in range(N-1)]\n",
    "    \n",
    "edge ={}\n",
    "Z = np.array(IntVector('z', N*N),dtype=object).reshape(N,N)\n",
    "\n",
    "# create edges and variable to define order in connectivity tree\n",
    "for i in range(N):\n",
    "    for j in range(N):  \n",
    "        for (k,l) in neigh(i,j,N):\n",
    "            edge[(i,j,k,l)] = Int(\"e%d%d%d%d\" % (i,j,k,l))\n",
    "            s+=Or(edge[(i,j,k,l)] ==0,edge[(i,j,k,l)] ==1)\n",
    "\n",
    "# no edges into or out of unfilled cells. Only one edge per cell     \n",
    "for i in range(N):\n",
    "    for j in range(N):       \n",
    "        s += Implies(Y[i,j] ==0 , Sum([edge[(k,l,i,j)] for (k,l) in neigh(i,j,N)]) == 0)\n",
    "        s += Implies(Y[i,j] ==0 , Sum([edge[(i,j,k,l)] for (k,l) in neigh(i,j,N)]) == 0)\n",
    "        s += Implies(Y[i,j] > 0 , Sum([edge[(k,l,i,j)] for (k,l) in neigh(i,j,N)]) <= 1)\n",
    "        for (k,l) in neigh(i,j,N):\n",
    "            # Make edges one way to form a tree\n",
    "            s += (edge[(i,j,k,l)] + edge[(k,l,i,j)]) <= 1\n",
    "\n",
    "    # limit the order values\n",
    "    s += [And(e>= 0 ,e <=int(N*N)) for (i,j),e in np.ndenumerate(Z)]\n",
    "\n",
    "    # order is ascending along edges\n",
    "    for i in range(N):\n",
    "        for j in range(N):            \n",
    "            s += [Implies(And(Y[i,j]!=0,edge[(k,l,i,j)]==1),Z[i,j] > Z[k,l]) for (k,l) in neigh(i,j,N)]\n",
    "\n",
    "    # only one cell with no feed in => root\n",
    "    s += PbEq([(And(Y[i,j] != 0,Sum([edge[(k,l,i,j)] for (k,l) in neigh(i,j,N) ]) == 0),1) for i in range(N) for j in range(N)],1)\n",
    "\n",
    "    \n",
    "for i,p in enumerate(params[0]):\n",
    "    if p >0:\n",
    "        for shape in itertools.product([0,1],repeat=N):\n",
    "            if np.sum(shape)> 1 :\n",
    "                s +=constraint(Y[:,i],H[:,i],shape,p)\n",
    "\n",
    "for i,p in enumerate(params[1]):\n",
    "    if p >0:\n",
    "        for shape in itertools.product([0,1],repeat=N):\n",
    "            if np.sum(shape)> 1 :\n",
    "                s +=constraint(Y[::-1,i],H[::-1,i],shape,p)\n",
    "                \n",
    "for i,p in enumerate(params[2]):\n",
    "    if p >0:\n",
    "        for shape in itertools.product([0,1],repeat=N):\n",
    "            if np.sum(shape)> 1 :\n",
    "                s +=constraint(Y[i,:],H[i,:],shape,p)\n",
    "                \n",
    "for i,p in enumerate(params[3]):\n",
    "    if p >0:\n",
    "        for shape in itertools.product([0,1],repeat=N):\n",
    "            if np.sum(shape)> 1 :\n",
    "                s +=constraint(Y[i,::-1],H[i,::-1],shape,p)\n",
    "               \n",
    "print(\"setup done in {:.2f} seconds\".format(time.time()-start))       \n",
    "if s.check() == sat:\n",
    "    m = s.model()\n",
    "    evalu = np.vectorize(lambda x:m.evaluate(x).as_long())\n",
    "    result_x =  evalu(H)\n",
    "    result_y =  evalu(Y)\n",
    "    sol_print(result_x,result_y)\n",
    "    print(\"Took {:.4f} seconds\".format(time.time()- start))\n",
    "    soln = result_x*result_y\n",
    "    print(\"solution is {:,.0f}\".format(areas(soln)))\n",
    "else:\n",
    "    print(\"Fail\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "The completed grid is shown above. The product of the areas of the regions of blank squares is 78125 . Congrats to everyone who solved this month’s puzzle!"
      ],
      "text/plain": [
       "<IPython.core.display.Markdown object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "url='https://www.janestreet.com/puzzles/hooks-5-solution/'\n",
    "res = requests.get(url)\n",
    "soup = BeautifulSoup(res.content, 'html.parser')\n",
    "x =[text for text in soup.body.stripped_strings]\n",
    "#display([(i,j) for i,j in enumerate(x)])\n",
    "display(Markdown(\" \".join(x[11:15])))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "id": "ld_NFUIfT1W9"
   },
   "source": [
    "### Puzzle solution\n",
    "<img src=\"https://www.janestreet.com/puzzles/20190701_hooks_5_sol.png\" width=\"250\" height=\"400\">\n",
    "\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "colab": {
   "include_colab_link": true,
   "name": "JaneSt-Feb18.ipynb",
   "provenance": []
  },
  "kernelspec": {
   "display_name": "Python 3 (ipykernel)",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.9.12"
  },
  "vscode": {
   "interpreter": {
    "hash": "aee8b7b246df8f9039afb4144a1f6fd8d2ca17a180786b69acc140d282b71a49"
   }
  }
 },
 "nbformat": 4,
 "nbformat_minor": 4
}