2018_02_Hooks3-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 scipy.ndimage import measurements\n",
    "from z3 import *\n",
    "from IPython.display import Markdown, display,Image,HTML"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "id": "U9Yh1D3HT1Ws"
   },
   "source": [
    "### Puzzle details\n",
    "<img src=\"https://www.janestreet.com/puzzles/hook3_puzzle-01.png\" width=\"300\" height=\"300\">"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {
    "id": "0VI0NM6ET1Wt"
   },
   "outputs": [],
   "source": [
    "#Setup the constraints\n",
    "top_labels = [0,35,42,18,18,0, 36, 63,0]\n",
    "bot_labels = [0,40,32,40,10,12,0,56,0]\n",
    "left_labels = [0,56,0,32,40,15,16,25,0]\n",
    "right_labels =[0,49,63,0,18,42,63,54,0]\n",
    "params = [top_labels,bot_labels,left_labels,right_labels]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {
    "id": "0VI0NM6ET1Wt"
   },
   "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": 4,
   "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",
    "    for i,e in enumerate(split):\n",
    "        if e !=0:\n",
    "            yield line[i]*hook_line[i]\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]*nums[1] == param)\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "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 11.53 seconds\n"
     ]
    },
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAARgAAAEYCAYAAACHjumMAAAAOXRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjUuMSwgaHR0cHM6Ly9tYXRwbG90bGliLm9yZy/YYfK9AAAACXBIWXMAAAsTAAALEwEAmpwYAAAmuklEQVR4nO3de3QUZZ438F89VdWX6k46l4aQkA4kIa2EcIkhwXWIDMNFHBcxLzNRJgqj4znvuHLOjLsyMjtZWR0kjEtUcJgbjsrOKkdAdEAcddQVQZegEeQSIRBIJ5iEdK7dnXSluy7vH7uZ43GTOO9Qz1Ox+vf5y057nu/z1Gm/VnVS9XC6rgNCCNFAzJ4AQsi6sGAQQtRgwSCEqMGCQQhRgwWDEKJGGOtN+7z5DawmMkxpaszkfVOAs9nbrZyZaLm4VuvmAgAM1R0pHOnnYxYMAEDq5l8eNn46owt+d2kl61wzMhMtF9dq3dze9WvLR3sPL5EQQtRgwSCEqMGCQQhRgwWDEKIGCwYhRA0WDEKIGiwYhBA1WDAIIWqwYBBC1HzlX/IiBAAQO1mfEnqqZr7adtlLJJcsVd1z1LWyqtmquWaw4lrxDAZ9JT0e4/ofeegmW3FpYOJrh3e6f/jj9yO/3fqt2JlPPVbMNYNV14oFg75S/PSJFC0SciXdv+4UJ4i6c+nyNiEntyO6f0+BFXPNYNW1YsGgr6TrOjfCTznlciDNirlmsOpasWDQV7LNmNPHSe5oeNvm2frQEIm+/mq20tyUCbEY1e/wzMo1g1XX+rWePGKDs9s1T/WmN8O/fPwbwYqFc/jJvqA4s7iJE0XNirlmsOpasWDQX8Vecn2P/bl9B4Zfd61escJevqjRqrlmsOJa8RIJ/VWG6o+maYMDvBYOCaGtNbO0cEhy3XnvOavmmsGKa8UzGPRXib62r6Cv+oHpoKlEmJLXnrpp20HilKifvpuVawYrrhULBv1VUjY8XgcAdYmSawYrrhUvkRBC1GDBIISowYJBCFGDBYMQogYLBiFEDRYMQogaLBiEEDVYMAghajhd10d9k/dO7GU4FwAA0CJhCUAXiDs5ZOXMRMvFtVo3FwBA7epMHennY/4l7yxfmM5sxtDSEhfc7slACLuTq66hqJCWlsY0M9Fyca1scody/QD8+LkwGbNgRBvXXlOTeZjVZAAAbq8MVBJCYM2aNbtZZdbW1jLPTLRcXCubXOAJpD2xg2lu7/q15aO9N36qDiFkOVgwCCFqsGAQQtRgwSCEqMGCQQhRgwWDEKIGCwYhRA0WDEKIGsOfyXv+/JC7dkuwvLU1nsELoM6e5bz48IaMD0WRG/2ehKu0cePGe774WlVV3u/3N6xateoDK2UmmkQ6xlZdq+EFU7slWJ6URKJ79k75Q0+PYlv3YPstz+zomXHfP6SfNjprWHV19bPD/xyNRoXa2trVRUVFTbTyzMpMNIl0jK26VsMvkXp71aQbF7ibJImo2dm26PRCR2tLa2zEG6FoqKury7Pb7dGioqIOK2cmmkQ6xlZaq+EFs3iJ+9Sh9yLTImFVCDTHpIYzcs7cuVKr0TmjaWho8BcUFDRy3Ah7iVsoM9Ek0jG20loNL5h586T2jg4ltaIicPcPfnD5Tp9PDFZUJDcbnTOSjo4OdzAYzCwrK2O23aYZmYkmkY6x1dZqaMGoqg4bHr7y7eLrnJf2H5j6+xde9O0cHNTtj23snGdkzmiOHTtW4PV6O7Kyspg9Z8KMzESTSMfYams1tGCCQcURDmvuu+9OPeN0Ei0jQxxatNh97swZOcfInNE0Njb6CwsLmTa/GZmJJpGOsdXWamjBTJokyh4PCe/c2VsYj+tcd7die/ediD8rS+w2MmckDQ0NGbIsu8rKyi7SzjIzM9Ek0jG24loN/zX1+p9OfOs3v+6+4bYVzXMIAS0vz9b24LoJHxqd82XHjx/3+3y+Sy6XK047y8zMRJNIx9iKazW8YEpLpe7SUumA0eN+laqqKqZP3jMrM9Ek0jG24lrxVgGEEDVYMAgharBgEELUYMEghKjBgkEIUYMFgxCiBgsGIUQNFgxCiBosGIQQNZyuj/4kS69X6GU4FwAAiEQ0SVV5weFwhFhlyrIsAQDTzETLxbWyyVV4XiDuZKa5AABqV+eID5Ub81YBn0+kM5sxtLTEhQJpBhDC7uTqQndAyEv1Mc1MtNxEW6sz3c18rV1dXcJQrh+AHz8XJmMWjGjj2mtqMpneH3F7ZaCSEAK7V23dzSpz7vYK5pmJlpuIa12zZg3TtdbW1lYCTyDtiR1Mc3vXry0f7b3xU3UIIcvBgkEIUYMFgxCiBgsGIUQNFgxCiBosGIQQNVgwCCFqsGAQQtQY/tDvRLP96Av5z9XvLemJhtzJdtfgo4t/9N6t0xdR31PYrFwzJMIx3rhx4z1ffK2qKu/3+xtWrVr1AY28L4qdrE8JPVUzX2277CWSS5aq7jnqWlnVbMTYWDBX4aWTByf/9tiueb9Y9pO3l077RmdTT6tk5VwzJMoxrq6ufnb4n6PRqFBbW7u6qKioiWYmAIAej3H9jzx0k/2bSxqSfrfroPzuG5mhLT9fJl5b9LJtxuz+qx0fC+YqbD/6wty75txWf7P/xk4AAL936qCVc82QiMe4rq4uz263R4uKiqifpcVPn0jRIiFX0v3rTnGEgHPp8rbB3f/REd2/p8A2Y/bHVzs+FszfKK4qXEtf24TuaF+g+OkVd8Q1hS/Nntm89e+rjybb3arVcs2QqMe4oaHBX1BQ0MhxHO0o0HV9hBCdUy4H0owYH7/k/Rs1933uVHWNHL70Ud7e7z29/0/ff+bliz2t3p+99eR1Vsw1QyIe446ODncwGMwsKytjsj+1bcacPk5yR8PbNs/Wh4ZI9PVXs5XmpkyIxQw5+cCC+Ru5bZICAPCdomWn89NzBn2eTLlqzq0nP758KseKuWZIxGN87NixAq/X25GVlRWmnQUAwNntmqd605uxTz/OCVYsvGvwlV2zxJnFTSQ1bcCI8fES6W+UmTQhluJIGuA4bvQndlko1wyJeIwbGxv9JSUlJ1hm2kuu77E/t+8v2z13rV6xwl6+yJAzKDyDuQqL8m84t+f0G0WB3s8d7eGg7cUTB2aW+WYFrJprhkQ6xg0NDRmyLLvKysou0sz5sqH6o2na4ACvhUNCaGvNLC0cklx33nvOiLHxDOYqbF724Cc/fPVhx+Jnv3+HSAT173KKmx5b8o/HrZprhkQ6xsePH/f7fL5LLpcrTjPny6Kv7Svoq35gOmgqEabktadu2naQOCXNiLGxYK6CQ7Brz3/nF0cA4Egi5JohkY5xVVUV06dHDkvZ8HgdANTRGBsvkRBC1GDBIISowYJBCFGDBYMQogYLBiFEDRYMQogaLBiEEDVYMAghajhdH/12C69X6GU4FwAAiEQ0iVNtgsfhZraBd78ckQCAaWai5SbaWhVQBYfDwXStsixLCs8LxJ3MNBcAQO3qTB3p52P+Ja/PJ9KZzRhaWuKCh7iA0H8Uxl8MKiD4OQK8GmUXCgAXdUUYzLdDhJeZ5sbbFOEGD4BA+phlftalCb0phdBHeGaZAADx7lahNDWH6Ub0F7oDgjPdzTQTAKCrq0sYyvUD8OPnwmTMghFtXHtNTSbTP1++vTJQSTgO7lt4PbMNvB/d/3YlDxw8n5PDdNPwBRfOV3I8B7kP5TLNPfvjs5UC0eHdNS5muZNrw5VAeJi0ahPTtbZuX11JCIHdq7Yyy527vaKSEAJr1qxhutba2tpK4AmkPbGDaW7v+rXlo703fqoOIWQ5WDAIIWqwYBBC1GDBIISowYJBCFGDBYMQogYLBiFEDRYMQogaw5/Je/78kLt2S7C8tTWewQugzp7lvPjwhowPRdG622yciEaTV7cEvlvslC7uzMn5T7PnYyU97/5+RrTxw2uUUDDNkTPzQsYdj71n9pysJnayPiX0VM18te2yl0guWaq656hrZVWzEWMbfgZTuyVYnpREonv2TvnDr341ee+FC0OZz+zomWF0znjyyJWO+T6bLWj2PKxISEofSJq74hNn7nVnzZ6LFenxGNf/yEM32YpLAxNfO7zT/cMfvx/57dZvxc586jFifMMLprdXTbpxgbtJkoianW2LTi90tLa0xka8EcoKnunuzpcIic12OD43ey5WlFx6W3Py3FubicM9ZPZcrCh++kSKFgm5ku5fd4oTRN25dHmbkJPbEd2/p8CI8Q0vmMVL3KcOvReZFgmrQqA5JjWckXPmzpVajc4ZD7oVRfz33p65GzIy/svsuSD0t9B1fYTbinVOuRxIM2J8wwtm3jypvaNDSa2oCNz9gx9cvtPnE4MVFcnNRueMB/96paN0kTvprN/uMGQfX4RYs82Y08dJ7mh42+bZ+tAQib7+arbS3JQJsZgh388aWjCqqsOGh698u/g656X9B6b+/oUXfTsHB3X7Yxs75xmZMx4cGYikn5blyT+ZOPGU2XNB6G/F2e2ap3rTm7FPP84JViy8a/CVXbPEmcVNJDXNkP9pGvpbpGBQcYTDmvvuu1PPOJ1EczrJ0KLF7nO7X+orBUo7x5nl/chAVo+qJi1oulAFABDTdVHTdW5JU1Pqn/Pz95k9P4T+WvaS63vsz+07MPy6a/WKFfbyRY1GjG1owUyaJMoeDwnv3NlbuHat99NQSBXffSfiz8oSu43MGQ/Wer2ffS819cLw66eCwdmdipL0eCbb5+dYna7EOV2NE13XOF3XOG1okOd4UeME0bJ/9sDaUP3RNHH6zH5QVS7y7PZCLRySXHfee86IsQ3/O5j1P5341m9+3X3DbSua5xACWl6ere3BdRM+NDrHbMk8ryTzvDL8WiJcXOQ4JdtmY/t4OovrfvOX1w2cfqdk+HXrU5UFrqJF9d5bHqg3c15WEn1tX0Ff9QPTQVOJMCWvPXXTtoPEKWlGjG14wZSWSt2lpdKBr/43rWVTZhZ+4Cnw3vIAlgllKRserwNKX2HgrQIIIWqwYBBC1GDBIISowYJBCFGDBYMQogYLBiFEDRYMQogaLBiEEDVYMAghajhdH/2WDq9X6GU4FwAAiEQ0SVM4wSmKIVaZ0XhcIpouJBPCLBMAIKxp0pAAAu/imeaqg6rk0HQh1cExy+2TdWkQbAJxuJmuVZMjkgM4wcMwt1+OSAqogsPhYLpWWZYlhecF4k5mmgsAoHZ1jvhQuTFvFfD5RDqzGUNLS1zwEA8QboTn4FDSGY4Ifo4AD+wyAQAuxoYEkmsHjmebK7fJwlwPgMDw/PWzLk0oSVNBIP3sQv8nd0rKLCCE3WIvdAcEZ7qbaSYAQFdXlzCU6wfgx8+FyZgFI9q49poatncH314ZqCQcB/ctvH43q8xH979dyQMHz+fkMMsEAFhw4Xwlx3OQ+1Au09yzPz5bKRAd3l3jYpY7uTZcKRBgmjmcSwiB3au2Msudu72ikhACa9asYbrW2traSuAJpD2xg2lu7/q15aO9N36qDiFkOVgwCCFqsGAQQtRgwSCEqMGCQQhRgwWDEKIGCwYhRA0WDEKIGsMf+n3+/JC7dkuwvLU1nsELoM6e5bz48IaMD0WRo7rNxL+9cWh5MDwwkeP+O0eyiQMbbl38Es3MYSei0eTVLYHvFjuliztzcv6Tdt6lzZcWRgPRybqii7zED6bemPppxsoMapvDR2I6+T8vDZZ/0q5NjsR0+yQ3F/ppuf3Y/y2xUd0S2KzcRBM7WZ8Seqpmvtp22UsklyxV3XPUtbKq2YixDS+Y2i3B8qQkEt2zd8ofenoU27oH2295ZkfPjPv+If200VlftvDa/A9unnkNtf/QRvPIlY75PpstyCpvwooJJ6Rc6RBxEG2gcSAl8GRguZQvdSXNSeqikRdTgWQlkcjmxY79szJI5Hf18Zwf/UleXJrF77kuk4/QyDQzN5Ho8RjX/8hDN9m/uaQh6Xe7DsrvvpEZ2vLzZeK1RS/bZsy+6vs6DL9E6u1Vk25c4G6SJKJmZ9ui0wsdrS2tsRFvhLKCZ7q78yVCYrMdjs9ZZbqnu3uJg/z3vjUc6ACgy21yMq28NCenPH+bs/66TD4iEA7+odTWMtHFhd9rVibQyjQzN5HET59I0SIhV9L9605xgqg7ly5vE3JyO6L79xQYMb7hZzCLl7hPHXovMm3hN13t3d2qreGMnPPdypSPjM4ZyZHzl8oOn79U5nE6+hcXFhwrmTK5nWZet6KI/97bM/cZn++153t6rqWZ9WWBJwPzI6cjfl3VBdErdqWWp7awyj7frTnbI7qnNItnere9WblWpuv6CHfa6pxyOZBmxPiGF8y8eVL7ofcGpldUBO7WdeCKix2NFRXJzUbnfNnNRdfUTfWm9ooCrx46d3Hano9OLpvgdr2ck55C7db1f73SUbrInXTWb3cYslH4/48pD0w5oiv6B6H6UEbkTCST2IkhO/F9lWhcJyt3D35rSZ7QWD5F6GORaWau1dlmzOnjJHc0vG3z7KT7/umU/M6fspTmpkwhd1qbEeMbeomkqjpsePjKt4uvc17af2Dq71940bdzcFC3P7axc56ROSMpyp7U6XbY43ZB0JbO8DdOTHZfOdHa5qOVd2Qgkn5alif/ZOLEU7QyvgoncLpnnqcj3hd3X9l7pZB2nqLpsPQ/BhcKBLSXK50f0M4zOzcRcHa75qne9Gbs049zghUL7xp8ZdcscWZxE0lNM+R/moaewQSDiiMc1tx33516xukkmtNJhhYtdp/b/VJfKVDamnIMug70HvDyfmQgq0dVkxY0XagCAIjpuqjpOrekqSn1z/n5+2jljkgDLtYVo/YdDACAputw838MLuiN6s4P7nH9ySlyTM6YzMpNJPaS63vsz+37y3bPXatXrLCXL2o0YmxDz2AmTRJlj4eEd+7sLYzHda67W7G9+07En5UldhuZ82X9UdlWd7ElW44rvKJq3NsNF6ZdCYUzZ2VPovbrzLVe72d/nJq7a/eUqXt3T5m695sud0ORw9nynM/3Oq1MAIBYZ8wRPBjMV8KKoCs613OoJ3vg7MA093Q31S+Zl78YLW/u11Pf+770hsfBqTSzxkNuIhmqP5qmDQ7wWjgkhLbWzNLCIcl1573njBjb8O9g1v904lu/+XX3DbetaJ5DCGh5eba2B9dN+NDonC9SVI2881lT6SufnEnhONA9TkffypKZb+Z606g9Pi2Z55VknleGX0uEi4scp2TbbDKtTAAA4AD6Pugr7PxjZznowPFJfNi7zPth+pL0AK3IEx2q+/ULynSBgJr9RGT18M//ZYH9/Z+V2y9YLTfRRF/bV9BX/cB00FQiTMlrT9207SBxSoacKRpeMKWlUndpqXTgq/9N46S7Jfmfb1n4CsvML9uUmVXPIsc2wSYXbCpgenznTOIj+obk37HMNDM30aRseLwOKH2FgbcKIISowYJBCFGDBYMQogYLBiFEDRYMQogaLBiEEDVYMAgharBgEELUcLo++oPmvF6B+W3xkYgmaQonOEWR2Qbe0XhcIpouJBPCdNPwsKZJQwIIvItnmqsOqpJD04VUB8cst0/WJR2AaeZwrgZ2weNwM8vtlyOSAqrgcDiYrlWWZUnheYG4k5nmAgCoXZ0jPvNpzL/k9flEOrMZQ0tLXPAQDxCO3YbwneGI4OcI8PTujRzRxdiQQHLtwPFsc+U2WeAy7NDPMHeoTRbsjDOHc+cmXct0I/oL3QHBme5mmgkA0NXVJQzl+gH48XNhMmbBiDauvaYm8zCryQAA3F4ZqCQcB/ctvJ7ZBt6P7n+7kgcOns/JYbpp+IIL5ys5noPch3KZ5p798VnmuWZkDucSQmD3qq3Mcudur6gkhMCaNWuYrrW2trYSeAJpT+xgmtu7fm35aO+Nn6pDCFkOFgxCiBosGIQQNVgwCCFqsGAQQtRgwSCEqMGCQQhRgwWDEKIGCwYhRI3hD/02y7+9cWh5MDwwkeM4HQBAsokDG25d/JLZ86Lh0uZLC6OB6GRd0UVe4gdTb0z9NGNlxlmz50WDmWvdfvSF/Ofq95b0REPuZLtr8NHFP3rv1umLOmhkbdy48Z4vvlZVlff7/Q2rVq36Wm80Z5mCAQBYeG3+BzfPvMaS/6F90YQVE05IudIh4iDaQONASuDJwHIpX+pKmpPUZfbcjGbWWl86eXDyb4/tmveLZT95e+m0b3Q29bRKNPOqq6ufHf7naDQq1NbWri4qKmqimckCXiJ9Dbmnu3uJ43/2ouZABwBdbpOp7uxoFrPWuv3oC3PvmnNb/c3+Gzt5woPfO3XQ7506SDsXAKCuri7PbrdHi4qKqJwtsWSpM5gj5y+VHT5/qczjdPQvLiw4VjJlcrvZc6Il8GRgfuR0xK+ruiB6xa7U8tQWs+dEC+u1xlWFa+lrm9Ad7QsUP73ijrim8KXZM5u3/n310WS7m/rukg0NDf6CgoJGjuETBWixTMHcXHRN3VRvaq8o8Oqhcxen7fno5LIJbtfLOekpzJ+NwcKUB6Yc0RX9g1B9KCNyJpJJ7MSyezazXmtz3+dOVdfI4Usf5e393tP7bYKo3bn7wZt+9taT1z29/F8+opnd0dHhDgaDmbfddtshmjmsWOYSqSh7UqfbYY/bBUFbOsPfODHZfeVEa5vP7HnRxAmc7pnn6Yj3xd1X9l4pNHs+NLFcq9smKQAA3yladjo/PWfQ58mUq+bcevLjy6dyaOYCABw7dqzA6/V2ZGVlhWlnsWCZghmBrgPjJ0iZRQMu1hWz5Hcw/wuDtWYmTYilOJIGhn8jyVJjY6O/sLCwkXUuLZYomP6obKu72JItxxVeUTXu7YYL066Ewpmzsie1mj03o8U6Y47gwWC+ElYEXdG5nkM92QNnB6a5p7s/N3tuRjNzrYvybzi35/QbRYHezx3t4aDtxRMHZpb5ZgVoZjY0NGTIsuwqKyu7SDOHJUt8B6OoGnnns6bSVz45k8JxoHucjr6VJTPfzPWm9Zs9N8NxAH0f9BV2/rGzHHTg+CQ+7F3m/TB9STrVD78pTFzr5mUPfvLDVx92LH72+3eIRFD/Lqe46bEl/3icZubx48f9Pp/vksvlitPMYckSBZPuluR/vmXhK2bPgwXbBJtcsKnggNnzYMHMtToEu/b8d35xBACOsMqsqqpi+nhaFixxiYQQGp+wYBBC1GDBIISowYJBCFGDBYMQogYLBiFEDRYMQogaLBiEEDWcro9+u4XXK/QynAsAAEQimqQpnOAURWZ3QUfjcYloupBMCNM7r8OaJg0JIPAunmmuOqhKoLPNNSNzONeu2QSPw80st1+OSAqogsPhYLpWWZYlhecF4k5m/gQBtaszdaSfj/mXvD6fSGc2Y2hpiQse4gHC8FkYneGI4OcI8IzvjbwYGxJmCDbghxjnqkPCFBvbXDMyh3PzM68FQtidrF/oDgjOdDfTTACArq4uYSjXD8CPnwuTMQtGtHHtNTWZTP98+fbKQCXhOLhv4fW7WWU+uv/tSh44eD4nh1kmAMCCC+cTJtfMtRJCYPeqrcxy526vqCSEwJo1a5iutba2thJ4AmlP7GCa27t+bflo742fqkMIWQ4WDEKIGiwYhBA1WDAIIWqwYBBC1GDBIISowYJBCFGDBYMQosYSz+RNVCei0eTVLYHvFjuliztzcv7T7PnQZPW1bty48Z4vvlZVlff7/Q2rVq36gHZ27GR9Suipmvlq22UvkVyyVHXPUdfKqmYjxsaC+Rp75ErHfJ/NFjR7HixYfa3V1dXPDv9zNBoVamtrVxcVFTXRztXjMa7/kYdusn9zSUPS73YdlN99IzO05efLxGuLXrbNmH3Vu3LgJdLX1DPd3fkSIbHZDofl9kP6skRaKwBAXV1dnt1ujxYVFXXQzoqfPpGiRUKupPvXneIEUXcuXd4m5OR2RPfvKTBifCyYr6FuRRH/vbdn7oaMjP8yey60JdJahzU0NPgLCgoaOQY3/Oq6PkKIzimXA2lGjI8F8zX0r1c6She5k8767Y4Bs+dCWyKtFQCgo6PDHQwGM8vKyphsH2ubMaePk9zR8LbNs/WhIRJ9/dVspbkpE2IxQ74+we9gvmaODETST8vy5Ndz8142ey60JdJahx07dqzA6/V2ZGVlhVnkcXa75qne9Gb4l49/I1ixcA4/2RcUZxY3caKoGTE+FszXzPuRgaweVU1a0HShCgAgpuuipuvckqam1D/n5+8ze35GSqS1DmtsbPSXlJScYJlpL7m+x/7cvr/soNm1esUKe/kiQ86gsGC+ZtZ6vZ99LzX1wvDrp4LB2Z2KkvR4Jtvn9rCQSGsFAGhoaMiQZdlVVlZ2kWXuUP3RNHH6zH5QVS7y7PZCLRySXHfee86IsbFgvmaSeV5J5nll+LVEuLjIcUq2zSabOS8aEmmtAADHjx/3+3y+Sy6XK84yN/ravoK+6gemg6YSYUpee+qmbQeJU8JLJASwKTOr3uw5sGL1tVZVVZlyZpay4fE6AKijMTb+FgkhRA0WDEKIGiwYhBA1WDAIIWqwYBBC1GDBIISowYJBCFGDBYMQogYLBiFEDafr+qhver1CL8O5AABAJKJJmsIJTlEMscqMxuMS0XQhmRBmmQAAYU2TdICEyDVzrcDbBI/DzSy3X45ICqiCw+FgulZZliWF5wXiTmaaCwCgdnWmjvTzMW8V8PlEOrMZQ0tLXPAQDxAGD9sZ1hmOCF63i2kmAICcQLlmrrXQey0Qwu5k/UJ3QHCmu5lmAgB0dXUJQ7l+AH78XJiMWTCijWuvqWF75+rtlYFKwnFw38Lrd7PKfHT/28wzEy3X1LUSArtXbWWWO3d7RSUhBNasWcN0rbW1tZXAE0h7YgfT3N71a8tHe2/8VB1CyHKwYBBC1GDBIISowYJBCFGDBYMQogYLBiFEDRYMQogaLBiEEDWWeej3v71xaHkwPDCR4zgdAECyiQMbbl38ktnzosGMtSbS8R22/egL+c/V7y3piYbcyXbX4KOLf/TerdMXUd8vmrXYyfqU0FM189W2y14iuWSp6p6jrpVVzUaMbZmCAQBYeG3+BzfPvOas2fNgwYy1JtLxfenkwcm/PbZr3i+W/eTtpdO+0dnU0yqZPSca9HiM63/koZvs31zSkPS7XQfld9/IDG35+TLx2qKXbTNm91/t+HiJhNAIth99Ye5dc26rv9l/YydPePB7pw76vVMHzZ6X0eKnT6RokZAr6f51pzhB1J1Ll7cJObkd0f17CowY31JnMEfOXyo7fP5Smcfp6F9cWHCsZMrkdrPnRIsZa02U4xtXFa6lr21Cd7QvUPz0ijvimsKXZs9s3vr31UeT7W7V7PkZSdf1Ee4+1TnlciDNiPEtUzA3F11TN9Wb2isKvHro3MVpez46uWyC2/VyTnoK81vXaTNjrYl0fJv7PnequkYOX/oob+/3nt5vE0Ttzt0P3vSzt5687unl//KR2fMzkm3GnD5OckfD2zbPTrrvn07J7/wpS2luyhRyp7UZMb5lLpGKsid1uh32uF0QtKUz/I0Tk91XTrS2+cyeFw1mrDWRjq/bJikAAN8pWnY6Pz1n0OfJlKvm3Hry48uncsyem9E4u13zVG96M/bpxznBioV3Db6ya5Y4s7iJpKYNGDG+Zc5gRqDrAGwfPmIeM9Zq2eObmTQhluJIGhj+jZnV2Uuu77E/t+/A8Ouu1StW2MsXNRoxtiXOYPqjsq3uYku2HFd4RdW4txsuTLsSCmfOyp7UavbcjGbGWhPp+A5blH/DuT2n3ygK9H7uaA8HbS+eODCzzDcrYPa8aBiqP5qmDQ7wWjgkhLbWzNLCIcl1573njBjbEmcwiqqRdz5rKn3lkzMpHAe6x+noW1ky881cb9pV/5ptvDFjrYl0fIdtXvbgJz989WHH4me/f4dIBPXvcoqbHlvyj8fNnhcN0df2FfRVPzAdNJUIU/LaUzdtO0ickmbE2JYomHS3JP/zLQtfMXseLJix1kQ6vsMcgl17/ju/OAIAR8yeC20pGx6vA4A6GmNb4hIJITQ+YcEghKjBgkEIUYMFgxCiBgsGIUQNFgxCiBosGIQQNVgwCCFqOF0f/XYLr1foZTgXAACIRDRJUzjBKYrM7tKNxuMSADDNTLRcM9fKc6LgcbiZ5fbLEUkBVXA4HEzXKsuypPC8QNzJzO9wV7s6U0f6+Zh/yevziXRmM4aWlrgwebIAPM/uPrqWFo55ZqLlmrtWAJ435Obgv0q8RfmftSrMMgEAWlp0ITx5BgA/fi5MxiwY0ca119RkHmY1GQCA2ysDlTzPwZbaLGYbeJuRmWi5uFY2ucATSHtiB9Pc3vVry0d7b/xUHULIcrBgEELUYMEghKjBgkEIUYMFgxCiBgsGIUQNFgxCiBosGIQQNZZ4Ji8AwPnzQ+7aLcHy1tZ4Bi+AOnuW8+LDGzI+FEV6W0+YkWlmbiJJpM9T7GR9Suipmvlq22UvkVyyVHXPUdfKqmYjxrbMGUztlmB5UhKJ7tk75Q+/+tXkvRcuDGU+s6NnhtUyzcxNJInyedLjMa7/kYdushWXBia+dnin+4c/fj/y263fip351GPE+JYpmN5eNenGBe4mSSJqdrYtOr3Q0drSGhvxBqyvc6aZuYkkUT5P8dMnUrRIyJV0/7pTnCDqzqXL24Sc3I7o/j0FRoxvmYJZvMR96tB7kWmRsCoEmmNSwxk5Z+5cierGYGZkmpmbSBLl86Tr+gh3n+qccjmQZsT4lvkOZt48qf3QewPTKyoCd+s6cMXFjsaKiuRmq2WamZtIEuXzZJsxp4+T3NHwts2zk+77p1PyO3/KUpqbMoXcaW1GjG+JMxhV1WHDw1e+XXyd89L+A1N//8KLvp2Dg7r9sY2d86yUaWZuIkmkzxNnt2ue6k1vxj79OCdYsfCuwVd2zRJnFjeR1DRDnm9hiYIJBhVHOKy577479YzTSbSMDHFo0WL3uTNn5BwrZZqZm0gS6fMEAGAvub7H+9y+AxNf/3Bn+o6XXte6g8lCwfROI8a2RMFMmiTKHg8J79zZWxiP61x3t2J7952IPytL7LZSppm5iSSRPk8AAEP1R9O0wQFeC4eE0NaaWVo4JLnuvPecEWNb5juY9T+d+NZvft19w20rmucQAlpenq3twXUTPrRappm5iSSRPk/R1/YV9FU/MB00lQhT8tpTN207SJySZsTYlimY0lKpu7RUOmD1TDNzE0kifZ5SNjxeBwB1NMa2xCUSQmh8woJBCFGDBYMQogYLBiFEDRYMQogaLBiEEDVYMAgharBgEELUYMEghKjhdH30p/GVzZMaGM4FAAAuNsUyfT4RRBvXbuXMRMvFtbLJDfmKgbPZmeYCAAzVHSkc6edjFgxCCF0NvERCCFGDBYMQogYLBiFEDRYMQogaLBiEEDVYMAghav4f02X/2NEMwMEAAAAASUVORK5CYII=\n",
      "text/plain": [
       "<Figure size 288x288 with 1 Axes>"
      ]
     },
     "metadata": {
      "needs_background": "light"
     },
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Took 36.2231 seconds\n",
      "[9. 2. 2. 3. 4. 8. 2. 1. 1. 3. 1.]\n",
      "solution is 20,736\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",
    "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\")\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {
    "id": "Z5uTHO2BT1W_"
   },
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "### Hooks #3\n",
       "\n",
       "Many solvers were able to find the unique filling of this grid that has all the\n",
       "filled squares connected, and also satisfies the edge product and hook placement\n",
       "conditions. (Shown to the left.) The product of the areas of the regions of\n",
       "empty squares is\n",
       "20736"
      ],
      "text/plain": [
       "<IPython.core.display.Markdown object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "url='https://www.janestreet.com/puzzles/hooks-3-solution/'\n",
    "res = requests.get(url)\n",
    "soup = BeautifulSoup(res.content, 'html.parser')\n",
    "y =[text for text in soup.body.stripped_strings]\n",
    "#display([(i,j) for i,j in enumerate(y)])\n",
    "display(Markdown(\"### \"+y[8]+\"\\n\\n\"+str(\"\\n\".join(y[11:13]))))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "id": "ld_NFUIfT1W9",
    "tags": []
   },
   "source": [
    "### Puzzle solution\n",
    "<img src=\"https://www.janestreet.com/puzzles/20180228_hooks_3_ans.png\" width=\"300\" height=\"400\">"
   ]
  },
  {
   "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
}