Created
October 16, 2022 14:00
-
-
Save ruoyu0088/5671d206f8a988185289131e6478e01c to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| { | |
| "cells": [ | |
| { | |
| "cell_type": "code", | |
| "execution_count": 1, | |
| "metadata": {}, | |
| "outputs": [], | |
| "source": [ | |
| "import numpy as np\n", | |
| "import itertools\n", | |
| "from collections import defaultdict\n", | |
| "from IPython.display import display_html\n", | |
| "from z3 import *" | |
| ] | |
| }, | |
| { | |
| "attachments": { | |
| "image.png": { | |
| "image/png": "iVBORw0KGgoAAAANSUhEUgAAAHAAAABwCAYAAADG4PRLAAAHFklEQVR4Ae1dP1LzOhDfvHk1FT1kaCg4BOmSoeYEULwDmEO8yVe+MrnB11CR4psxh6CgYUgOwBn0RrHXjmNJlq2Vo4VlJmNbkXbXv9/qn7NeJkopBfLHFoG/2Fouhu8REAKZO4IQKAQyR4C5+dIDvyuB2+0W7u/v4e7uDvQ59Z/IdyPqjY/eRpj+ZrOZ3l7sP9Pp1FQlqEzku+Hzxcc6hB72uq+vL7e7DPhW5LtB88bH5gd5nqvz83N1dnamnp+fbdUGl4t8N3S++Ey0GLcvyLcpI2AdQlM2WmyrERACayxYnjEh8BWeJhOYHHwW6x0h4DtYL5ryn14JxccU5Z5KE/g2z6rtDG5rquN8pbbBJm7Val5slyq55fYpy4OFRxcA0TUEKajBbYKZq4wI5O1qXjjIoTNUTpOp1DlMm8DtSs01UU32CpcoQZ6vQvogOkibKCTWpDrIJ4kbpz0HXjzAi1KglrftWWR6DfN2ac+ST3jfAMD8GqZHLS+ubvYlbx+Uc+2REoLLtAl03ODuz2/Q2N9cXThqdXy1+4A3XeXmClpSSgfZvH92CDnt1zwJ3K3hn8cNQJaDqXP2hXR+fdz/AODiCoo+2FfauPX5Ebhbw+LyETaQQU7B3rh4k2vjReAheWoJhplxEEDGYRKH10ESx2vEhsDdegET3fPmK9hSkYfD5NsHtJYqn+/7OdY4vI7HT6cmFgRq8i7LOU+9PLQXHJ23aaswhWu9lN28w/FSZfexX96ELZJsainLibcl5OJwP2bcCxJoq+TLRp4AzWMRuJEvn7ocP+rS12Ebea0QN/Ptx2mpb+K19WkPoeU8RDnitGVdwMPLFlZHTwWyXJFsUdr6aEvkB11aPEeXlnYPHB0OfgqFQH6cNSy2Eugdl9gQ538h8t1YeeNzvPDDa9+4RKzf9yjy3Yj54uPsgegjEheKSNRH77jNukmvM2/5Nj/wjUu0te8qF/luhHzxkW1Er36RXmXrEJqeqWKRCQEh0IQKozIiAmPHbTJCtMvU1yeYTJ6AKuw0nMC9QTP4dWT45vESJot1+3e2o3o/6lL/ID07RioMgUACd7D+tzBIP/zV78kUnxwybdfmEf6jcrWw+zx9a+3o+1AQWlPCCNz9gd86NKwVXHQLy3xPIaQelkcLp0laOb3se14GWQGLqeKgsjACo8dtDrqnJBsVI9QS7oit+5tYXiUO4zazkLjNShrnk1tYRnwFM6wH2nAljtu0qZFyAHoCD0P/JG4zuo/REnhIHlXoX3QIeCsgIzBK3CZvbEexnmQR04jblGFzFOJQSXAPFPIQytMcwwjE1aa2/des8Q47vs9O+y77aUBKWWsYgaPEbaYM3+ltkx90T89BkAVhPTBItTSmQEAIpEDxhDKsBHrHJQ40XuS7gfPGxxYb5RuXaGvfVS7y3Qj54uPsgegjEheKSNRH77jNukmvM2/5Nj/wjUu0te8qF/luhHzxkW1Er36RXmXrEJqeqWKRCQEh0IQKozIiAttxoWzybY5CVhsfsmfE7qnU41tHIoLwBAQe+lOvUqWubCdRgMPMGAPvIzjdZJ4VhjXIqkhtp3EcaCfTZnUGjGbGC7p8p4EEloYYPKkg9ocTiI7cZK9wRpJ8p0UkNb1347BhIJZeGVOJJbmNkWvArRAtYoqVwOtTmThcRyHrnGakabFGWW2MpgTjZoPynWprB5BuaVKP95hRKdS7LIr4F7uG1p53R0jgoWa6SfpQ6rc4R/KAZn0QiUCdgsyRsPxbMDHgJhATIvK0BaRzYGMCwVycjcKfexEtbnaAH9VN0KMiLpNrZXzPqpSWJpwCbytwCK0XLo0FCxILcxX0bx0Cby6F5jHJ0/cXSKBSCvd8hpyeDVJTQHNsGypHNjxGK/EKxSh8DrxdglLlK9UHU5x+ofHlofXfGA5q/IDTEeJm5Qdd5n4U3gOZA8DdfCGQOYNWAr3jEgcCIPLdwHnjY1uY+cYl2tp3lYt8N0K++Dh7IPqIxIUiEvXRO26zbtLrzFu+zQ984xJt7bvKRb4bIV98ZBvRq1+kV9k6hKZnqlhkQkAINKHCqIwfgcT5NltcxZbfUhhWwIvACPk2G/DFlt9QRnNBkieGxpQOKbpnECdLbWiMLb+hjO6CQQ+Mm28TILZ8OrJMkhgQWJgdK98mghJbPuqhPjIYQuPm2wSILZ+asqY8Nj2wabZcIQJCICLB9CgEMiUOzRYCEQmmRyGQKXFothCISDA9CoFMiUOzhUBEgulRftBlShyaLT0QkWB6FAKZEodmWwn0jktEST2PIt8NmDc+ttgo37hEW/uucpHvRsgXH2cPRB+RuFBEoj56x23WTXqdecu3+YFvXKKtfVe5yHcj5IuPbCN69Yv0KluH0PRMFYtMCAiBJlQYlQmBjMgymSoEmlBhVCYEMiLLZOr/xwbImyfTRT4AAAAASUVORK5CYII=" | |
| } | |
| }, | |
| "cell_type": "markdown", | |
| "metadata": {}, | |
| "source": [ | |
| "" | |
| ] | |
| }, | |
| { | |
| "attachments": { | |
| "image.png": { | |
| "image/png": "iVBORw0KGgoAAAANSUhEUgAAAfgAAAH4CAYAAACmKP9/AAAgAElEQVR4Ae2dT2gVS9q4K7979zobAxPREQZdCCYi+GcW/t0NxLXOWi8RFITrMkJEYTaR6+IDJbr+4sJVAt8uSgQ1KkoEXSRMxjmSUeIquhoEOT/e3DltV6VPn+5TXV3V3U9BSFdX1VtvPW9Vv6erqrsH2u12WxEgAAEIQAACEKgVgf9Xq9bQGAhAAAIQgAAENgjg4OkIEIAABCAAgRoSwMHX0Kg0CQIQgAAEIICDpw9AAAIQgAAEakgAB19Do9IkCEAAAhCAAA6ePgABCEAAAhCoIQEcfA2NSpMgAAEIQAACP01MTExkwSCPy799+1a9ePFCffv2TQ0ODmYpFkwe9PdrCvjD34YA/ceGnn1Z+NsztJHQN3950U2vsLKy0j569Ki8ECf6O378eFvOVyGgv18rwR/+NgToPzb07MvC356hjQQb/qpXxd+/f2/v27cvcuxxJz8yMtKW9JAD+vu1Dvzhb0OA/mNDz74s/O0Z2kiw5d/TwT9//jzRuXcc/cuXL230d14W/Z0jTq0A/ql4nCfC3zni1Argn4rHeWLT+ffcZPfx48fUpYPV1dXUdN+J6O/XAvCHvw0B+o8NPfuy8LdnaCPBln9PBz80NJSq3/bt21PTfSeiv18LwB/+NgToPzb07MvC356hjQRr/r3mSGQNYHh4OHGavipr8Ojfy8ru0uk/7thmkQz/LJTc5YG/O7ZZJDedf881eIEou/hk13xn3V3+V20XPfpnGQ5u8tB/3HDNKhX+WUm5yQd/N1yzSm0y/wGBlHUK4d27d+r9+/dq165dau/evVmLBZMP/f2aAv7wtyFA/7GhZ18W/vYMbST0wz+Xg7dRjrIQgAAEIAABCJRHoOcmu/JUoSYIQAACEIAABIoigIMviiRyIAABCEAAAgERwMEHZAxUgQAEIAABCBRFAAdvSXJhYUHdvHlTDQwMRH9Xr15Vs7Oz6suXL5bSKd6LwPLy8gZr0wZiD7HD/fv3leSpWrhw4ULUn6qmu+iL/lW0Wvk6c/10zDzrowbk0wksLi62R0dHtUcH448Rdo5nZmb0gsQKIdBqtdpjY2M9+XfsIHmXlpYKqdu1kLm5Oa1drusrWj76F020fvK4fpZjU3bR9/ED6s2bN2pkZCRzyfHxcXX9+vXM+cmYTiAv/7i0xcVFNTw8HD8V1HFS23I8yeq9Lejv3QTBK5DUR9KU5vqZRic9jSn6dD6bUmW6N49zFwE3btxQd+/e3SSLE/kJ5L04mDWI7URGiOHDhw8bywoh6pZFJ/TPQqnZebh+lmz/ciYK6lOLOS0s0/QyJbm+vh41UqafzHwyVSzTygQ7AknLItPT05um38UeYofJyUltulvsIDJCC6JrZznB/B+arkn6oH8SFc6ZBMzrItdPk1Cx8Uyvqi22yupKMy9i0jnX1ta6NsjszOKICP0TePbsmeYEe/Hv1GSWEwcqP8pCCbJPw3Tq8XgoenbTA/27keF8nADXzziNco6Zos8xY/LixQst9+XLl9W2bdu0c/HI2NhYPKrm5+e1OJF8BJ48eaIVkH0Nafw7mQ8fPqymp6c70Y3/jx490uI+IjKlLbvNT58+HVU/OjoaHYd+gP6hWygs/bh+erBHOb8j6lGL3DHG76zi0/LdWhjPL8eE/gnYsJSZFpvy/WudXDJp6UBmfELTM1n7duLSB/p3o8V5IcD1s/x+wC56xz+q5HnseKjSjui43nU4DskWpi5TU1Pq/PnzG5jNtBD7jKkj+tdhhITXBrOfhTgWwqP2QyOm6H+wcH4kj3sQwiAQylS4LOO0Wq3IuYdBJ7sW6J+dFTntCHD9zM/v5/xFKJGVgPk41okTJ7IWJV/BBExb+Hbw4hjlL+Rn8tNMgP5pdEgrgoA5Zrl+5qeKg8/PLFOJz58/a880i0M5efJkprJkKp7AgwcPNKEHDx7U4mVHbt++XXaVhdaH/oXiRJhBgOunAaTPKA6+T3Ddisn751+9eqVu3bq18Y50ySfO/d69e92KcN4xgYcPH268bKhTjdijqnfOnTbwHwJ1JMD1s1irssmuIJ7iRE6dOrVJmqwbXbp0KdPjXJsKc8KagEzzmW8eXFpaUrt377aW7UpA1TcWob+rnlFfuVw/3diWTXZuuEZSt27dqj59+hTFOSiPQJJzl+fhQ3bu5dGhJgiET4Drp52NuIO34xeVlnfNf/36Ve3fv1+trKyo169fqzt37kTpsinp2rVr3MlHRNweJDn3qny0gjtgt32jl/Sq8+/VvhDTuX66sQoO3g3XDanypq+LFy9Ga/FyMvTpYYc4ShMt34A/e/asVl9VnLsoXXUHg/5a1yPSJwGun32CixVjij4Go+jDHTt2bGyuiz+SdeXKlaKrQV6MQNWde6wpHEKg0QS4ftqbHwdvzzBVgrwrXd5Z3wmzs7PaHX3nPP/tCVy9enXTnbusucs76wkQgED1CHD9tLMZDt6OX6bSBw4c0PKZH13QEonkJiBTefLBlhs3bmhlxbmfOXNGO0cEAhCoFgGun/3bizX4/tnlKln1dclcjS0x88LCgjpy5MimGhcXFyv7rHvV+wr6b+qOnLAkUPU+Zdn8votzB983Ogr6JiDr7aZzl/0Oa2trlXXuvplSPwQgUB8COPgctpRpYPkl2fmTty5lCcvLy1q2+KY7LYFIZgJJm+kmJyfVzMwMjyJmpkhGCJRHgOtneaw7NeHgOyQy/D927JiW6/Hjx1q8W0Q21sUDDj5OI/+xvPXKfAxOHPuvv/6aXxglIACBUghw/SwFs1YJa/AajvRI0stTZDpYdnp2C0llqrw+3K2dZZ2XDXU7d+7Uqqsbz6qvN6K/1j2J/JdA0rWQ66fb7sEdfA6+8oES8+773LlzSu4o5etH8SDT8vJ2JvM96PLCFT50EieV71iYxkPdnHu8bRxDoE4EuH6Wb03u4HMyF8e9Z8+enKV+zy4/DuSrcml3/H0JbkihpLt3m6a3222b4s7KcgfsDG0mwVXnn6mRnjJx/SwXPHfwOXnLh0rkrjFvwLnnJbY5/9OnTzef5AwEIFAZAlw/yzUVDr4P3jLV1Gq1lHxAJkuYmppid3cWUD3yzM/P98hBMgQgEDoBrp/lWYgpekvWsnFE3kxnfj1OHtmSX6uHDh1iSt6Scae4OXXaOd/vf6bo+yWXXs60U6icu7Wi6vp3a1eI57l+urUKDt4tX6RDAAIQgAAEvBBgit4LdiqFAAQgAAEIuCWAg3fLF+kQgAAEIAABLwRw8F6wUykEIAABCEDALQEcvFu+SIcABCAAAQh4IfDTxMTERJaaZSfs27dvN3aMf/v2TQ0ODmYpFkwe9PdrCvjD34YA/ceGnn1Z+NsztJHQN/92hrCystI+evSovPYr+jt+/HhbzlchoL9fK8Ef/jYE6D829OzLwt+eoY0EG/6qV8Xfv39v79u3L3LscSc/MjLSlvSQA/r7tQ784W9DgP5jQ8++LPztGdpIsOXf08E/f/480bl3HP3Lly9t9HdeFv2dI06tAP6peJwnwt854tQK4J+Kx3li0/n33GT38ePH1KWD1dXV1HTfiejv1wLwh78NAfqPDT37svC3Z2gjwZZ/Twc/NDSUqt/27dtT030nor9fC8Af/jYE6D829OzLwt+eoY0Ea/695khkDWB4eDhxmr4qa/Do38vK7tLpP+7YZpEM/yyU3OWBvzu2WSQ3nX/PNXiBKLv4ZNd8Z91d/ldtFz36ZxkObvLQf9xwzSoV/llJuckHfzdcs0ptMv9cH5t59+6dev/+vdq1a5fau3evzcyDl7Lo7wV7VCn8IxReDuDvBXtUKfwjFF4Omsg/l4P3YhUqhQAEIAABCEAgN4Gem+xyS6QABCAAAQhAAALeCeDgvZsABSAAAQhAAALFE8DBF88UiRCAAAQgAAHvBLw7+IWFBXXz5k01MDAQ/V29elXNzs6qL1++eAfUVAUuXLgQ2aOpDGg3BKpKgPHr13Kh8Pe2ye7Nmzeq48jTTDEzM6NGR0fTspBWMIGHDx+qU6dORVLlS0YECECgGgQYv37tFBJ/Lw5enPvIyEhmK4yPj6vr169nzk/G/gkk2QYH3z9PSkKgTAKM3zJpb64rNP6lT9EvLy/ncu6C8MaNG+ru3bubaXKmUAIfPnzYmFUpVCjCIACBUggwfkvB3LWSEPmX7uB/++03DZBMv8/Nzan19XV5q97G3+LiohobG9Py/fLLL0oAEtwQkF+eO3fu3Nj74KYGpEIAAq4IMH5dkc0mN1T+pTp4gXDnzp2ImDj3e/fuqZMnT6otW7ZE54eHh9Xt27c3OfmnT59GeTgojoBsaMyzZFJczUiCAARsCTB+bQnalQ+Zf6kO/sWLFxrJy5cvq23btmnn4hHzLn5+fj6ezLElAZkRkd2ep0+fjiSxoTFCwQEEgibA+PVrnkrwz/rC/iLyjY6Oah+sWV9f7yk2/oEbOSYUQ2ByclKzhbAdGxtrr62tbTpfTI1IgQAEiiLA+C2KZH9yqsLfyy76PL+75Pn4eGBHd5xG/8cm16mpKXX+/PkNgWYazPvnTEkIuCBgjlHGrwvK3WVWhX+pU/TdcWVLkcflCMUSkGWQVqsVOfdipSMNAhBwSYDx65Jub9mh8/+5dxP85ZBNefFw4sSJeJRjCwLSMeVPNjQSIACBahFg/Pq1V1X4BztF//nzZ3Xu3LnosS3Z/CVvtSO4J2BOPzFF7545NUCgKAKM36JI9icnJP7B3cHL++dfvXqlbt26pTl3eZyOAAEIQAACEIBANgLBOHjz/b0d9WXd/dKlS6mP03Xy8h8CEIAABCAAgd8JBL/JbuvWrerTp0/YCwIQgAAEIACBHASCWYOXd81//fpV7d+/X62srKjXr19rb72TTQ3Xrl3jTj6HcfvNGtIaUr9toBwEmkqA8evX8iHxD8bBJ5lE3hR08eLFaC1e8iwtLandu3cnZedcQQRC6qAFNQkxEGgMAcavX1OHxD/oKfodO3ZsvKs+/vrUK1eu+LUetUMAAhCAAAQqQCBoBy/85F318s76TpAX+8sfAQIQgAAEIACB7gSCd/Ci+oEDB7QWmB+t0RKJQAACEIAABCCggl6Dj9snpHWNuF51PIZ1Ha1Km5pCgPHr19Ih8a/EHbxfc1E7BCAAAQhAoHoESnXw8t1x+XXT+ZO31mUJy8vLWrb4pjstgQgEIAABCEAAAhsESnXwx44d07A/fvxYi3eLmJvqcPDdSHEeAhCAAAQg8DuBUtfg5etwIyMjGvu1tbXUl9cklVlcXOQraBrFYiMhrSEV2zKkQaD+BBi/fm0cEv9S7+Dl06Tm3bd8MU7eQy9fj4sHmZaXt9uZPwjk3fR84jROimMIQAACEIDAZgKl3sFL9eK49+zZs1mTDGfkx4F8VU6ejSe4IxDSL1B3rUQyBOpJgPHr164h8S/1Dl6wy2tmZYo9b8C55yVGfghAAAIQaDKB0h28wJYp9larpeQDMlnC1NSUmpmZ4c49CyzyQAACEIAABJTy/6Ib2UQnb6Yzvx43OTm5cbd/6NAhHHvJXTWkKaaSm051EKg8AcavXxOGxL/0NXi/6KkdAhCAAAQg0AwCXqbom4GWVkIAAhCAAAT8EcDB+2NPzRCAAAQgAAFnBHDwztAiGAIQgAAEIOCPAA7eH3tqhgAEIAABCDgj8NPExMREFuntdlu9fft2Y8f7t2/f1ODgYJZiweRBf7+mgD/8bQjQf2zo2ZeFvz1DGwl9829nCCsrK+2jR4+2lVLR3/Hjx9tyvgoB/f1aCf7wtyFA/7GhZ18W/vYMbSTY8Fe9Kv7+/Xt73759kWOPO/mRkZG2pIcc0N+vdeAPfxsC9B8bevZl4W/P0EaCLf+eDv758+eJzr3j6F++fGmjv/Oy6O8ccWoF8E/F4zwR/s4Rp1YA/1Q8zhObzr/nJruPHz+mLh2srq6mpvtORH+/FoA//G0I0H9s6NmXhb89QxsJtvx7OvihoaFU/bZv356a7jsR/f1aAP7wtyFA/7GhZ18W/vYMbSRY8+81RyJrAMPDw4nT9FVZg0f/XlZ2l07/ccc2i2T4Z6HkLg/83bHNIrnp/HuuwQtE2cUnu+Y76+7yv2q76NE/y3Bwk4f+44ZrVqnwz0rKTT74u+GaVWqT+ef62My7d+/U+/fv1a5du9TevXttZh68lEV/L9ijSuEfofByAH8v2KNK4R+h8HLQRP65HLwXq1ApBCAAAQhAAAK5CfTcZJdbIgUgAAEIQAACEPBOAAfv3QQoAAEIQAACECieAA6+eKZIhAAEIAABCHgngIO3NMGHDx/U/fv31dWrV9XAwED0J/HZ2Vn1+fNnyxrcFl9eXt7Q8+bNm5HunXZIG6RtkifUUHX+oXJtil5V7z+M36b01D7bmfVRA/JtJjA5Oak9Ohh/jDB+LPlCC61Wqz02NpZJf2mL5F1aWgqqGVXmHxTIhipT5f7D+G1op83Z7EzPweeU2Yjs4+PjmZ2jOEjJH0pYXFzMpXv8x4qUDSFUmX8I/JquQ5X7D+O36b03e/tx8NlZRTmnpqb6cpBSznewuTh0HL1vJ19l/r7tT/3tdpX7D+OXHpyHAA4+D612uy1TYx1H1/k/OjraNp2exOV8J0/n//r6es4ai82epNP09PSm6XfRU9qQNI0pMnyFqvP3xY16fydQ9f7D+PV7/azaOMLB57SYOMOOs5b/vabezQE5MzOTs8bisj979kzTXXRbW1vrWYFZTto9NzfXs5yLDFXm74IHMvMRqHL/Mcch4zef7ZuYm130OTcn/u///q9W4vz581rcjPzP//yPdur//u//tHiZkSdPnmjVXb9+XW3btk07lxQ5fPiwmp6e1pIePXqkxcuKVJl/WYyopzuBKvcfxq9SPq+f3XtVwClN/FXTb5vN6b1ed++deszd6lnumjtli/wfn3mQ4zxBdLYpn6eubnmrzr9buzhfDoGq9x+b8cf4LaePhVYLd/A5fnz94x//0HIfPHhQi3eL/PWvf9WS/vnPf2rxsiLtdlu8evSXp94sd/p55PWTt+r8+2kzZYojUPX+Ex+7cpwnMH7z0KpPXhx8DluaL63ZsWNHptJmvn/961+ZyoWcaXR0tHT14F868lpVSP/5YU7G7w8WdT7Cweew7r///W8t9x/+8Act3i1i5jPldCsX0vk3b95o6vi4QJjcTK6agrGImc+UE8vKYY0JmHY3+0W3ppv5TDndyoV0nvEbkjXK0wUHn4P1+vq6lnvLli1avFvEzGdOFXYrF9L5Bw8eaOpkXZ7QCllGmszfEh3FlVJN7j+M32YOAb4Hn8Pu8o72eMizDmZTNl6nj+OHDx+qU6dORVXL3fvMzEwUL+vAhqFN2bLaRz1uCdj0AZuyblvVWzrjtzejuubAweewrM0gtymbQ8XCs8rU3sjIiCZ3aWlJ7d69WztXRsSGoU3ZMtpGHe4J2PQBm7LuW9a9BsZvdzZNSGGKvglW7rONSRcHeR7eh3PvswkUg0BjCTB+G2v6qOE4+AgFB3ECSReH8fFxdebMmXg2jiEAgQAJMH4DNIoHlXDwHqCHXqV8A96clhfnLm++I0AAAmETYPyGbZ8ytcPBl0m7AnXJxeHs2bOapjh3DQcRCARLgPEbrGm8KIaDz4FdHF08fPnyJR7temzmM+V0LVhywtWrVzc5d1lzD+XO3eRmcu2Gy8xnyulWjvP1ImDa3ewX3Vpr5jPldCtX9nnGb9nEw68PB5/DRlu3btVymwNfS4xFzHymnFhWL4cfPnxQp0+fVjdu3NDqF+ce0pq7yc3kqikfi5j5TDmxrBzWmIBpd7NfdGu6mc+U061cWecZv2WRrl49P1dPZX8aDw0NaZX/5z//0eLdImY+U063cmWcX1hYUEeOHNlU1eLiohoeHt503ucJk5vJtZtuZj5TTrdynK8XAdPuZr/o1loznymnW7kyzjN+y6Bc3Tq4g89huz/96U9a7tXVVS3eLSLPjcdDCB9+EH1kvc507vISm7W1teCcu+hbN/7xPsGxewJ16z+MX/d9puo14OBzWPCPf/yjljvrN9FfvHihlfvzn/+sxX1EkjbjTE5ObryhLpQfICaXOvE320bcPYE69R/Gr/v+UosaQvt+bej6jI6Oat9Fl29MpwXzG9RS3neYm5vT2iDfmZ6ZmfGtVqb668A/U0PJ5IRAHfoP49dJ16ilUO7gc/5M+9vf/qaV+Pvf/67MTTidDHJe0uPBLB9PK+NYNuTE3ysvdcp6u4+vw/XTXpNf1fj302bKFEeg6v2H8atff4vrGTWVVMufLQ4bZd6Ry92v3BUsLi5qtUrcvFuQvL3u+DUhDiLj4+Pa3bupt4MqCxVZdf6FwkBYbgJV7z+M3/QZ09wdouYFVM3b56R5k5OTmpMUx53lb2pqyok+WYUmXdyy6N0tT9Z6i85XVf5Fc0BefwSq2n8Yv36vn/31Nr+lcPB98F9fX0+8O+/mCOW8/PL2HaanpzP9EElrRzzNV3uqyt8XL+rVCVS1/zB+dTsS600AB9+bUWIOuUhkvROQfCGEsbGxWjh4YVlF/iH0AXT4nUAV+w/jl96blwDfg7fcWyGbXp4+farevXunvQlOXme5d+9e9Ze//EXt2LHDspZiipvftLaV2m7L7wW/oUr8/ZKi9iQCVeo/jN8kC3IujQAOPo0OaRCAAAQgAIGKEuAxuYoaDrUhAAEIQAACaQRw8Gl0SIMABCAAAQhUlAAOvqKGQ20IQAACEIBAGgEcfBod0iAAAQhAAAIVJfDTxMTERBbdZcf027dvlXw45du3b2pwcDBLsWDyoL9fU8Af/jYE6D829OzLwt+eoY2Evvlnea5uZWWlffToUe0Z6uPHj7flfBUC+vu1Evzhb0OA/mNDz74s/O0Z2kiw4d/zRTffv39v79u3T3PunbeZjYyMtCU95ID+fq0Df/jbEKD/2NCzLwt/e4Y2Emz593Twz58/T3TuHSf/8uVLG/2dl0V/54hTK4B/Kh7nifB3jji1Avin4nGe2HT+PTfZffz4MXXpYHV1NTXddyL6+7UA/OFvQ4D+Y0PPviz87RnaSLDl39PBDw0Npeq3ffv21HTfiejv1wLwh78NAfqPDT37svC3Z2gjwZp/rzkSWQMYHh5OnKavyho8+veysrt0+o87tlkkwz8LJXd54O+ObRbJTeffcw1eIMouPtk131l3l/9V20WP/lmGg5s89B83XLNKhX9WUm7ywd8N16xSm8w/18dm5Itp79+/V7t27dr4UprN1IOPsujvg/qPOuH/g4WPI/j7oP6jTvj/YOHjqIn8czl4H0ahTghAAAIQgAAE8hPouckuv0hKQAACEIAABCDgmwAO3rcFqB8CEIAABCDggAAO3gFUREIAAhCAAAR8EwjWwV+4cEENDAxs/PmGVOf6FxYW1M2bNyPWwvzq1atqdnZWffnypc5ND7ptVe//Vdc/6M4RU47xG4MR0GEw/T/rowZl5pubm9MeySuz7qbUtbi42B4dHdU4xx+D7BzPzMw0BUkw7ax6/6+6/sF0hBRFGL8pcDwnhdT/g9tF/+bNGzUyMqL9FpNP5RGKI5DEOE36+Pi4un79eloW0goikGSbKvX/qutfkBmdiklinFYh4zeNTrFpSbbxOX6DmqL/8OHDxvRwsciRFiewvLy86QdUPD3p+MaNG+ru3btJSZwrkEDV+3/V9S/QlM5EMX6dobUWHGT/9zybEVUvU06daWHzf5SJA2sCY2NjGmeZppcppfX19Ui22MLMJzZptVpRHg6KJVD1/l91/Yu1pjtp5rhk/LpjnUdyqP0/06tq8zS0n7yyzms69Xi8H5mU2UzA7IRycVhbW9uc8b9nzIvJ9PR017wk9E+g6v2/6vr3b7lySzJ+y+WdtbaQ+7/XKXqZ0pDdhqdPn46mR0ZHR6NjDool8OLFC03g5cuX1bZt27Rz8cjY2Fg8qubn57U4ETsCVe//Vdffznrll2b8ls88rcZK9P+sv1KKzjc5Obnprl3uGOWOMn73LseEYgiYu+bj0/LdasAW3cjYna96/6+6/nbW81Oa8euHe1KtVen/3nbRy/PW8TA1NaXOnz+/ccpM87kLMa5jE4+xhRurm1yr1v+rrr8bq4Yn1bQT19JibGRyDXX8ep2iF9QyDdxqtSLnXgx+pLggII/bEIolUPX+X3X9i7Vm2NIYv8XbJ/T+/3PxTc4mUcDI3/DwcLYC5CqdgDzTGQ8nTpyIRzm2IFD1/l91/S1MV5mijF93pqpK//c2RZ+G3pz+YFopjZabtM+fP6tz585tvLJWapDNjzMzM24qQ6pGoOr9v+r6a8aoaITx689wIfV/b3fw/vBTcxoBef/8q1ev1K1btzTnfu/evbRipEEAAgEQYPwGYISAVMDBB2QMn6o8fPhQnTp1apMKsm536dKl1MfpNhXiBAQgUCoBxm+puCtTmfdNdpUh1VBFt27dqj59+tTQ1tNsCFSbAOO32vaz1Z41eFuCNSkv75r/+vWr2r9/v1pZWVGvX79Wd+7ciVonm0quXbvGnXxExN1BSGt4/bSy6vr302bfZRi/vi3wo/6Q+j8O/oddODIIyJuaLl68GK3FS/LS0pLavXu3kZNokQRCukD0066q699Pm0Msw/j1Y5WQ+j9T9H76QCVq3bFjh5LNdfHXB1+5cqUSuqMkBJpOgPHb9B6gFA6ePpBKQN5VL++s74TZ2Vntjr5znv8QgEB4BBi/4dmkTI1w8GXSrmhdBw4c0DQ3P3qhJRKBAASCIsD4DcocpSrDGnypuKtbWUjrStWlmE3zqrOuuv7ZrFStXNikPHuFxJo7+PLsTk0QgAAEIACB0gjg4EtD7b+i06dPK/l12fmTt15lCcvLy1q2+KY7LYEIBCDgjADj1xna2grGwdfWtJsbduzYMe3k48ePtXi3iGysiwccfJwGxxAohwDjtxzOdaqFNfg6WYJA7nYAACAASURBVLNHW+TrUiMjI1qutbW11JfXJJVZXFzkK4AaxWIjIa3h9dOyquvfT5vLKJM0Fhm/ZZDPV0dI/Z87+Hy2q3Ru+TSvefctX4yT91jL16fiQabl5e1Y5g8CeTc9n/iNk+IYAuUQYPyWw7lOtXAHXydrZmiLOO49e/ZkyLk5i/w4kBffyLO1BHcEQroD6KeVVde/nzaXVYbxWxbp/usJqf9zB9+/HStZUl4zK1PseQPOPS8x8kOgeAKM3+KZ1lkiDr7O1u3SNpnqa7VaSj4gkyVMTU2pmZkZ7tyzwCIPBBwTYPw6Blwj8UzR18iY/TRFNu7Im+nMr8dNTk5ufFTm0KFDOPZ+wFqUCWmKr59mVF3/ftrsqwzj1xf57vWG1P+DdPDd0ZECAQhAAAIQgEAWAkzRZ6FEHghAAAIQgEDFCODgK2Yw1IUABCAAAQhkIYCDz0KJPBCAAAQgAIGKEcDBV8xgqAsBCEAAAhDIQuCniYmJiSwZ2+22evv27caO62/fvqnBwcEsxYLJg/5+TQF/+NsQoP/Y0LMvC397hjYS+ubfzhBWVlbaR48ebSulor/jx4+35XwVAvr7tRL84W9DgP5jQ8++LPztGdpIsOGvelX8/fv39r59+yLHHnfyIyMjbUkPOaC/X+vAH/42BOg/NvTsy8LfnqGNBFv+PR388+fPE517x9G/fPnSRn/nZdHfOeLUCuCfisd5IvydI06tAP6peJwnNp1/z012Hz9+TF06WF1dTU33nYj+fi0Af/jbEKD/2NCzLwt/e4Y2Emz593TwQ0NDqfpt3749Nd13Ivr7tQD84W9DgP5jQ8++LPztGdpIsObfa45E1gCGh4cTp+mrsgaP/r2s7C6d/uOObRbJ8M9CyV0e+Ltjm0Vy0/n3XIMXiLKLT3bNd9bd5X/VdtGjf5bh4CYP/ccN16xS4Z+VlJt88HfDNavUJvPP9bGZd+/eqffv36tdu3apvXv32sw8eCmL/l6wR5XCP0Lh5QD+XrBHlcI/QuHloIn8czl4L1ahUghAAAIQgAAEchPouckut0QKQAACEIAABCDgnQAO3rsJUAACEIAABCBQPAEcfPFMkQgBCEAAAhDwTsC7g19eXlazs7Pq5s2bamBgQPu7evWqun//vpI8BAgkEVhYWNjUd6TfSJ/68uVLUhHOQSAiwPUnQsFBgQQuXLgQ+bICxeYXlfVRg6LztVqt9tjYmPboXfwxPPNY8i4tLRWtBvIqSmBxcbE9Ojras//MzMxUtIWo7ZIA1x+XdJste25uTrsu+aThZRf9mzdv1MjISP5fI0qpxcVFNTw83FdZCtWDQN7+Mz4+rq5fv16PxtMKawJ5+0+8Qq4/cRocmwSS+pZ86tVXKH2KPglAnsbLDwORQWgmAZlSzfvj8MaNG+ru3bvNBEarNQJcfzQcRAok8OHDByXLgyGF0h18EoDp6Wm1tLQkb9WL/tbX1zfu1icnJzfxSpKxKRMnakngt99+09o1Ojqq5ubmlPSXTv+Ru6yxsTEt3y+//KJkABKaTSDp2sH1p9l9oojWyw/HnTt3buz9KUJeYTLKXB949uyZtjYha6hra2s9VTDLyfq8rHMQmkVA1t3jezN69R9zj8f09HSzgNFajYB5HenVfzqFzXJcfzpk+C8EZJ9P/LpkHvukVOod/JMnT7QfJrIuum3bNu1cUuTw4cNKfmXHw6NHj+JRjhtA4MWLF1orL1++nNp/zLv4+fl5rTyRZhHg+tMse7turcwIym7506dPR1XJjGJIodRNdvIYXDzk2Xzw+fNnNTg4GC++MSWrnSBSawIykOTxt06QafktW7Z0oon/bfpcokBOVpaATV/g+lNZsztRXB7rvnLliiZbbiiuXbsWlJ8q1cFrNPqI2AzQPqqjSA0I0GdqYMRAmkBfCsQQAahh9oWpqSl1/vz5Dc3MtDw3skU3rdQp+iKVD20qpMi2IcsNAXlcjgCBIghw/SmCYvVlyF17q9WKnHtoLfo5NIW66WM+GscA60aK8x0CZp85ceJEJ4n/EMhFwOxLXH9y4atdZnHs8hf6O1kq4+AfPHigdZKDBw9qcSIQiBOQNdP4I1FyQT558mQ8C8cQyEyA609mVI3IePv27Uq0sxJr8A8fPlSnTp2KgMrFemZmJopzAIEOAXn//KtXr9StW7eiDXnSX+7du5e6475Tnv8QMAlw/TGJEE8jENIafPAOXqbGzDeXyUtxdu/encaYtIYRMC/CnebLuvulS5dw7h0g/M9FgOtPLlxkVmrjIzNxEGyyi9OIHScNLnkeHuceg8RhKoGtW7eqT58+peYhEQJJBLj+JFHhXJUIBHsHnzS4+GhIlbpWubrKu+a/fv2q9u/fr1ZWVtTr16/VnTt3IiU6z6hmebFSVIiDxhLg+tNY01s3nCn6HgjlG/Bnz57VcuHcNRxEMhCQN01dvHgxWouXIizvZADX8CxcfxreASybH5KDD+45eAaXZe+ieERgx44dG5vr4o80mW+fijJzAAGlFNcfukGdCAQ1RS+PNcmnPeNB1tzPnDkTP8UxBHIRMDfgyRMYcaefSxiZa0uA609tTVtqw7iDN3DLVKq8ZxznboAhWgiBAwcOaHLMj9ZoiUQaR4DrT+NM3pgGe7+DX1hYUEeOHNkEXL7pHfpbgjYpzYlgCYT0qzpYSA1UjOtPA43uuMkhXWu8rsHLepfp3GXqdG1tDefuuBMiHgJNJ8D1p+k9oP7t9+bgkzazTE5ObryhjkeZ6t/x+mmhLOPIr+POn7y1LktYXl7WsrH+ruFoZITrTyPN3rhGe3HwsunJfAxONj79+uuvjTMADc5O4NixY1rmx48fa/Fukfg35CUPDr4bqWac5/rTDDvTSqVKX4OXDS07d+7U2LPeruEg0oVA0stHZDknbcYnqQz9rQvgBpzm+tMAI3tuYqPX4OWNY/HAxTZOg+M0ArLp0rz7PnfunJI7Mvl6XDzItLz0NfM7BvLCJDZvxkk165jrT7Ps3fTWlnoHn/Tr2cYAPl/ib6M3ZfsnII57z549fQmQHwd8Va4vdLUoxPWnFmYMvhGNvYN/+vRp8MZBwbAJyIeGZNYnb8C55yVWv/xcf+pnU1qUTqDUTXbz8/Pp2pAKgQwEZIq91Wop+YBMljA1NcXTGVlA1TwP15+aG5jmbSJQ6hS9OXWxSZucJ5iizwmshtllE528mc78epw8cil3+4cOHUrdhFdDJDSpCwGuP13AcLpQAmY/8+mnSnXwhVJEGAQgAAEIQAACXQmUOkXfVQsSIAABCEAAAhAolAAOvlCcCIMABCAAAQiEQQAHH4Yd0AICEIAABCBQKAEcfKE4EQYBCEAAAhAIg8BPExMTE1lUkZ2Ab9++3dix/O3bNzU4OJilWDB50N+vKeAPfxsC9B8bevZl4W/P0EZC3/zbGcLKykr76NGjbaVU9Hf8+PG2nK9CQH+/VoI//G0I0H9s6NmXhb89QxsJNvxVr4q/f//e3rdvX+TY405+ZGSkLekhB/T3ax34w9+GAP3Hhp59WfjbM7SRYMu/p4N//vx5onPvOPqXL1/a6O+8LPo7R5xaAfxT8ThPhL9zxKkVwD8Vj/PEpvPvucnu48ePqUsHq6urqem+E9HfrwXgD38bAvQfG3r2ZeFvz9BGgi3/ng5+aGgoVb/t27enpvtORH+/FoA//G0I0H9s6NmXhb89QxsJ1vx7zZHIGsDw8HDiNH1V1uDRv5eV3aXTf9yxzSIZ/lkoucsDf3dss0huOv+ea/ACUXbxya75zrq7/K/aLnr0zzIc3OSh/7jhmlUq/LOScpMP/m64ZpXaZP65Pjbz7t079f79e7Vr1y61d+9em5kHL2XR3wv2qFL4Ryi8HMDfC/aoUvhHKLwcNJF/LgfvxSpUCgEIQAACEIBAbgI9N9nllkgBCEAAAhCAAAS8E8DBezcBCkAAAhCAAASKJ4CDL54pEiEAAQhAAALeCXh38MvLy2p2dlbdvHlTDQwMaH9Xr15V9+/fV5KHAIEkAgsLC5v6jvQb6VNfvnxJKsI5CEQEuP5EKDgokMCFCxciX1ag2Pyisj5qUHS+VqvVHhsb0x69iz+GZx5L3qWlpaLVQF5FCSwuLrZHR0d79p+ZmZmKthC1XRLg+uOSbrNlz83NadclnzS87KJ/8+aNGhkZyf9rRCm1uLiohoeH+ypLoXoQyNt/xsfH1fXr1+vReFphTSBv/4lXyPUnToNjk0BS35JPvfoKpU/RJwHI03j5YSAyCM0kIFOqeX8c3rhxQ929e7eZwGi1RoDrj4aDSIEEPnz4oGR5MKRQuoNPAjA9Pa2WlpbkrXrR3/r6+sbd+uTk5CZeSTI2ZeJELQn89ttvWrtGR0fV3Nyckv7S6T9ylzU2Nqbl++WXX5QMQEKzCSRdO7j+NLtPFNF6+eG4c+fOjb0/RcgrTEaZ6wPPnj3T1iZkDXVtba2nCmY5WZ+XdQ5CswjIunt8b0av/mPu8Zienm4WMFqrETCvI736T6ewWY7rT4cM/4WA7POJX5fMY5+USr2Df/LkifbDRNZFt23bpp1Lihw+fFjJr+x4ePToUTzKcQMIvHjxQmvl5cuXU/uPeRc/Pz+vlSfSLAJcf5plb9etlRlB2S1/+vTpqCqZUQwplLrJTh6Di4c8mw8+f/6sBgcH48U3pmS1E0RqTUAGkjz+1gkyLb9ly5ZONPG/TZ9LFMjJyhKw6QtcfyprdieKy2PdV65c0WTLDcW1a9eC8lOlOniNRh8RmwHaR3UUqQEB+kwNjBhIE+hLgRgiADXMvjA1NaXOnz+/oZmZludGtuimlTpFX6TyoU2FFNk2ZLkhII/LESBQBAGuP0VQrL4MuWtvtVqRcw+tRT+HplA3fcxH4xhg3UhxvkPA7DMnTpzoJPEfArkImH2J608ufLXLLI5d/kJ/J0tlHPyDBw+0TnLw4EEtTgQCcQKyZhp/JEouyCdPnoxn4RgCmQlw/cmMqhEZb9++XYl2VmIN/uHDh+rUqVMRULlYz8zMRHEOINAhIO+ff/Xqlbp161a0IU/6y71791J33HfK8x8CJgGuPyYR4mkEQlqDD97By9SY+eYyeSnO7t270xiT1jAC5kW403xZd7906RLOvQOE/7kIcP3JhYvMSm18ZCYOgk12cRqx46TBJc/D49xjkDhMJbB161b16dOn1DwkQiCJANefJCqcqxKBYO/gkwYXHw2pUtcqV1d51/zXr1/V/v371crKinr9+rW6c+dOpETnGdUsL1aKCnHQWAJcfxpreuuGM0XfA6F8A/7s2bNaLpy7hoNIBgLypqmLFy9Ga/FShOWdDOAanoXrT8M7gGXzQ3LwwT0Hz+Cy7F0Ujwjs2LFjY3Nd/JEm8+1TUWYOIKCU4vpDN6gTgaCm6OWxJvm0ZzzImvuZM2fipziGQC4C5gY8eQIj7vRzCSNzbQlw/amtaUttGHfwBm6ZSpX3jOPcDTBECyFw4MABTY750RotkUjjCHD9aZzJG9Ng73fwCwsL6siRI5uAyze9Q39L0CalOREsgZB+VQcLqYGKcf1poNEdNzmka43XNXhZ7zKdu0ydrq2t4dwdd0LEQ6DpBLj+NL0H1L/93hx80maWycnJjTfU8ShT/TtePy2UZRz5ddz5k7fWZQnLy8taNtbfNRyNjHD9aaTZG9doLw5eNj2Zj8HJxqdff/21cQagwdkJHDt2TMv8+PFjLd4tEv+GvOTBwXcj1YzzXH+aYWdaqVTpa/CyoWXnzp0ae9bbNRxEuhBIevmILOekzfgklaG/dQHcgNNcfxpgZM9NbPQavLxxLB642MZpcJxGQDZdmnff586dU3JHJl+PiweZlpe+Zn7HQF6YxObNOKlmHXP9aZa9m97aUu/gk3492xjA50v8bfSmbP8ExHHv2bOnLwHy44CvyvWFrhaFuP7UwozBN6Kxd/BPnz4N3jgoGDYB+dCQzPrkDTj3vMTql5/rT/1sSovSCZS6yW5+fj5dG1IhkIGATLG3Wi0lH5DJEqampng6Iwuomufh+lNzA9O8TQRKnaI3py42aZPzBFP0OYHVMLtsopM305lfj5NHLuVu/9ChQ6mb8GqIhCZ1IcD1pwsYThdKwOxnPv1UqQ6+UIoIgwAEIAABCECgK4FSp+i7akECBCAAAQhAAAKFEsDBF4oTYRCAAAQgAIEwCODgw7ADWkAAAhCAAAQKJYCDLxQnwiAAAQhAAAJhEPhpYmJiIosqshPw7du3GzuWv337pgYHB7MUCyYP+vs1Bfzhb0OA/mNDz74s/O0Z2kjom387Q1hZWWkfPXq0rZSK/o4fP96W81UI6O/XSvCHvw0B+o8NPfuy8LdnaCPBhr/qVfH379/b+/btixx73MmPjIy0JT3kgP5+rQN/+NsQoP/Y0LMvC397hjYSbPn3dPDPnz9PdO4dR//y5Usb/Z2XRX/niFMrgH8qHueJ8HeOOLUC+KficZ7YdP49N9l9/PgxdelgdXU1Nd13Ivr7tQD84W9DgP5jQ8++LPztGdpIsOXf08EPDQ2l6rd9+/bUdN+J6O/XAvCHvw0B+o8NPfuy8LdnaCPBmn+vORJZAxgeHk6cpq/KGjz697Kyu3T6jzu2WSTDPwsld3ng745tFslN599zDV4gyi4+2TXfWXeX/1XbRY/+WYaDmzz0Hzdcs0qFf1ZSbvLB3w3XrFKbzD/Xx2bevXun3r9/r3bt2qX27t1rM/PgpSz6e8EeVQr/CIWXA/h7wR5VCv8IhZeDJvLP5eC9WIVKIQABCEAAAhDITaDnJrvcEikAAQhAAAIQgIB3Ajh47yZAAQhAAAIQgEDxBHDwxTNFIgQgAAEIQMA7gWAd/IULF9TAwMDGn3dKNVZgeXlZzc7Oqps3b0a8O9yvXr2q7t+/ryQPwQ2BuvJn/LrpL6bUhYWFTWNXxq2M6S9fvpjZiZdEIJj+n/VRgzLzzc3NaY/klVl3U+pqtVrtsbExjXP8MUjzWPIuLS01BY/zdtaZP+PXefdpLy4utkdHR3uO35mZGffKUINGIKT+H9wu+jdv3qiRkRHtd5Z8Ko9QHIEkxlmlLy4uquHh4azZyZdAoM78k9rG+E3oBBankhiniRsfH1fXr19Py0JaQQSSbOOz/wc1Rf/hwwcl00sEdwSSOmCe2uTHl8gg9EegzvwZv/31iTylZEnHvAHqVf7GjRvq7t27vbKRbkkgyP6vzS14jMiUkzkt3Il7VKt2VSdN601PT2+afl9fX9+YBpycnNxkF5FB6I9AXfkzfvvrD3lLmctq0p9kSljGayeILcx8ci2VZSGCGwKh9v9Mr6p1g+SHVFkn6jjzpP8/cnJkQ+DZs2caZ7k4rK2t9RRplhMbyUWFkI+AybEu/Bm/+fpBv7lNJ9Kr/5hOXn7IE4onEHL/9zpFL1Mastvw9OnT0eTI6OhodMxBsQSePHmiCZR1uW3btmnnkiKHDx9W09PTWtKjR4+0OJHeBOrGn/Hb2+ZF5njx4oUm7vLly6njd2xsTMs/Pz+vxYnYEahE/y/+90w2iUlTv/KLU+4ozbv4bBLJ1YuADVfs0otu7/Q68Wf89rZ30Tnkjj3eh+LT8t3qiueXY0IxBKrS/73topdnreNhampKnT9/fuOUmeZzF2Jcx6YfYxe/PSAk/qYujF+/faNb7aaduJZ2I5XvvMk11P7vdYpekMo0UqvVipx7Pszk9kWApRRf5H+vNxT+jF+//SBP7fK4HKFYAqH3/5+LbW52aQJG/nimOjsznznNR+NCcTA+mZRZd2j8Gb9lWr+/usw+c+LEif4EUWoTgar0f28O/vbt25ugcSJcAg8ePNCUO3jwoBYn4pZAaPwZv27tbSv98+fP2jtF5Af5yZMnbcVS/r8EqtL/va3Bp/UUc32DdaM0Wu7THj58qE6dOhVVJBeLmZmZKM6BWwJV48/4ddsf0qTL++dfvXqlbt26tfE+eskr4/XevXupO+7TZJKWj0BI/R8Hn892jcud9Oa1paUltXv37sax8NHgKvIP6QLnw2Y+6jR/BHZ0kHX3S5cu4dw7QEr4H1L/977JrgTeVNEngSTnIs/D49z7BJqzGPxzAiP7JgJbt25Vnz592nSeE80gwB18M+ycu5VJzoWPVuTG2HeBKvMP6Q6mbwNUrKC8a/7r169q//79amVlRb1+/VrduXMnaoVsCrt27Rp38hERdwch9X8cvDs7V1ayfAP+7Nmzmv44dw2H00jV+Yd0gXNqqMCFy5vWLl68GK3Fi7osr7k3Wkj9nyl69/auVA1Vdy6Vgp2gLPwToHCqLwI7duzY2FwXf6T1ypUrfcmiUDUJ4OCraTcnWsunes07d1lz51vSTnBvEgr/TUg4YUlAvjUh76zvhNnZWe2OvnOe//UkgIOvp11ztUqm8uSDP/Ld6HgQ537mzJn4KY4dEIC/A6iIjAgcOHAgOpYD86M1WiKRWhFgDb5W5szfmIWFBXXkyJFNBRcXF3nL4CYqxZ+oI/+Q1iCLt1g1JWKT8uwWEmvu4Muze3A1yXqv6dxlvW5tbQ3nXoK14F8CZKqAQIMJ4OAbavykzVyTk5Mbb6jL8o34hmIrrNnwLwxlYwTJMprcHXb+5K11WcLy8rKWLb7pTksgUjsCOPjambR3g+StV+ZmOnn17K+//tq7MDmsCcDfGmEjBRw7dkxr9+PHj7V4t4hsrIsHHHycRr2PWYOvt303tU42dO3cuVM7z3q7hsNppAn8Q1qDdGrMkoUnvfxIltPSZtySyjDe3RoupP7PHbxbWwcnXd54FQ8M9jgN98fwd8+4rjXIp7XNu+9z584pmRGSr8fFg0zLS18bGRmJn1bywio+0a0hqXWEO/ham1dvXNLdo54jX4yv/OXj1RT+Id3B5LNQ+LnFce/Zs6cvReXHAV+V6wtdrkIh9X/u4HOZrtqZnz59Wu0GVFx7+FfcgAGoLx96klm3vAHnnpdYPfLj4Othx0ytmJ+fz5SPTG4IwN8N16ZJlSn2Vqul5AMyWcLU1BRPx2QBVcM8TNHX0KjdmmROHXXLl/U8U/RZSf2eryn8zXbST/L1kzy5ZROdvJnO/HqcPPIqd/uHDh1K3YSXpy7yZiMQUv8P0sFnw0guCEAAAhCAAAS6EWCKvhsZzkMAAhCAAAQqTAAHX2HjoToEIAABCECgGwEcfDcynIcABCAAAQhUmAAOvsLGQ3UIQAACEIBANwI/TUxMTHRLjJ+XnbBv377d2LH57ds3NTg4GE8O/hj9/ZoI/vC3IUD/saFnXxb+9gxtJPTNv50hrKystI8ePdpWSkV/x48fb8v5KgT092sl+MPfhgD9x4aefVn42zO0kWDDX/Wq+Pv37+19+/ZFjj3u5EdGRtqSHnJAf7/WgT/8bQjQf2zo2ZeFvz1DGwm2/Hs6+OfPnyc6946jf/nypY3+zsuiv3PEqRXAPxWP80T4O0ecWgH8U/E4T2w6/56b7D5+/Ji6dLC6upqa7jsR/f1aAP7wtyFA/7GhZ18W/vYMbSTY8u/p4IeGhlL12759e2q670T092sB+MPfhgD9x4aefVn42zO0kWDNv9cciawBDA8PJ07TV2UNHv17WdldOv3HHdsskuGfhZK7PPB3xzaL5Kbz77kGLxBlF5/smu+su8v/qu2iR/8sw8FNHvqPG65ZpcI/Kyk3+eDvhmtWqU3mn+tjM+/evVPv379Xu3btUnv37rWZefBSFv29YI8qhX+EwssB/L1gjyqFf4TCy0ET+edy8F6sQqUQgAAEIAABCOQm0HOTXW6JFIAABCAAAQhAwDsBHLx3E6AABCAAAQhAoHgCOPjimSIRAhCAAAQg4J0ADt7SBB8+fFD3799XV69eVQMDA9GfxGdnZ9Xnz58ta/BT/MKFC1Fb/GiQrda68s/WenLZEqhr/2H82vaMmpTP+qgB+TYTmJyc1B4djD9GGD+WfFUKc3NzWrtC1b2u/EPlXTe96tp/GL9166n9tyfTc/D9i69vyfHxcc0Jxh160rHkr0JYXFzc1K4Q9a4r/xBZ11GnuvYfxm8de2v/bcLB98FuampqkxNMcurmOSkXcmi1Wu3R0dFNbQtN57ryD41zXfWpa/9h/Na1x/bfLhx8TnYyiEzHLU5RfjnHg8STnOX6+no8WzDHSb/8O+0MRsl2u11X/iExrrMude0/jN8699r+24aDz8luenpac/C9pt5NJz8zM5OzRvfZRaeOM0/6716D7DXUkX/21pPTlkAd+w/j17ZX1Lc8Dj6nbU2HLXcEacG8YxgbG0vLXmqa6Cb6xJ262T5JCymY+lWZf0hcm6JLnfoP47cpvbb/doZ19e6/HaWUNJ11r7v3jlKmE11bW+skefuftINY9BTd4g4/JAdfJ/7eDN/giuvUfxi/De7IOZrOc/A5Hnf8xz/+oeU+ePCgFu8W+etf/6ol/fOf/9TiPiJXrlzRqp2amlK3b99W27Zt086HFKkT/5C4NkWXOvUfxm9Teq1dO3HwOfiZL63ZsWNHptJmvn/961+ZypWRaWxsTLVaLXX+/PkyqrOqo478rYBQOBeBOvYfxm+uLtC4zD83rsUWDf73v/+tlf7DH/6gxbtFzHymnG7lXJ6XC4P8DQ8Pu6ymUNkmN5Nrt8rMfKacbuU4Xy8Cpt3NftGttWY+U063ci7PM35d0q2PbBx8Dluur69rubds2aLFu0XMfOZUYbdyLs/LdHzVQp34V419HfStU/9h/NahR7pvA9+Dz8FY3jUfD+227EfLFmzKZquhuFyh6mqjl03Z4sgiyScBmz5gU7bsNoeqq41eNmXL5h9SfazBh2QNdIEABCAAAQgURAAHXxBIxEAAAhCAAARCIoCDD8ka6AIBCEAAAhAoiAAOviCQiIEABCAAAQiERAAHH5I10AUCEIAABCBQEAEcfA6Q4+PjWu4vX75o8W4RM58pp1s5zusETG4mVz33j5iZLwh7SgAAFHlJREFUz5TzIydHdSZg2t3sF93abuYz5XQrx3mdgMnN5Krn/hEz85lyfuTkyCSAgzeJpMS3bt2qpZodT0uMRcx8ppxYVg5TCJjcTK7dipr5TDndynG+XgRMu5v9oltrzXymnG7lOK8TMLmZXPXcP2JmPlPOj5wcmQRw8CaRlPjQ0JCW+p///EeLd4uY+Uw53cpxXidgcjO56rl/xMx8ppwfOTmqMwHT7ma/6NZ2M58pp1s5zusETG4mVz33j5iZz5TzIydHJgEcvEkkJf6nP/1JS11dXdXi3SJLS0taUsgfdNEUDSwC/8AMUjF16D9+DQb/8vnj4HMw/+Mf/6jlfvTokRbvFnnx4oWW9Oc//1mLE8lGAP7ZOJErmQD9J5lLWWfhXxbpWD05Pi1L1na7PTo6qn0vXb4xnRbMb1BL+dBDqN+DF25N4B96/6iyfk3oP4zfKvfQYnXnDj72YyfL4d/+9jct29///ndlbgLpZJDzkh4PZvl4Gse9CZj84N+bGTl+EKD//GDh4wj+JVMv9vdC/aWZd+Tya1nuChYXF7XGS9y8W5C8ve74NSGeIiHfATSBvyezN6LaJvQfxm8junKmRqpMucikEZicnNSm6c0B1S0+NTWlyQk1Yuofmp515x8a77rpU/f+w/itW4/tvz04+D7Yra+vJ96dmwMrHh8fH++jJj9F4nrLcWih7vxD4103ferefxi/deux/bcnvKt3/20ptaRcJLLeCUi+KoXQLxDCss78q9RXqqprnfsP47eqvbJ4vQdEZMnL/rWq7sOHD+rp06fq3bt36saNG1Hb5HWKe/fuVX/5y1/Ujh07ovNVOBgYGNDUDLmL1JG/Bp+IUwJ17D+MX6ddplLCcfCVMhfKQgACEIAABLIR4DG5bJzIBQEIQAACEKgUARx8pcyFshCAAAQgAIFsBHDw2TiRCwIQgAAEIFApAjj4SpkLZSEAAQhAAALZCPw0MTExkSWr7KR++/atkg+nfPv2TQ0ODmYpFkwe9PdrCvjD34YA/ceGnn1Z+NsztJHQN/8sT96trKy0jx49qr297fjx4205X4WA/n6tBH/42xCg/9jQsy8Lf3uGNhJs+Pd80c3379/b+/bt05x750UKIyMjbUkPOaC/X+vAH/42BOg/NvTsy8LfnqGNBFv+PR388+fPE517x8m/fPnSRn/nZdHfOeLUCuCfisd5IvydI06tAP6peJwnNp1/z012Hz9+TF06WF1dTU33nYj+fi0Af/jbEKD/2NCzLwt/e4Y2Emz593TwQ0NDqfpt3749Nd13Ivr7tQD84W9DgP5jQ8++LPztGdpIsObfa45E1gCGh4cTp+mrsgaP/r2s7C6d/uOObRbJ8M9CyV0e+Ltjm0Vy0/n3XIMXiLKLT3bNd9bd5X/VdtGjf5bh4CYP/ccN16xS4Z+VlJt88HfDNavUJvPP9bEZ+WLa+/fv1a5duza+lGYz9eCjLPr7oP6jTvj/YOHjCP4+qP+oE/4/WPg4aiL/XA7eh1GoEwIQgAAEIACB/AR6brLLL5ISEIAABCAAAQj4JoCD920B6ocABCAAAQg4IICDdwAVkRCAAAQgAAHfBLw7+IWFBXXz5k01MDAQ/V29elXNzs6qL1+++OZT+/qXl5c3WJs2EHuIHe7fv68kDwECEAiPAOM3PJuIRhcuXIj8mVcNsz5qUHS+xcXF9ujoqPboXfwxvM7xzMxM0VUjr91ut1qt9tjYWE/+HTtI3qWlJdhBAAIBEGD8BmCELirMzc1p19Uu2Uo57WUX/Zs3b9TIyEjmHzbj4+Pq+vXrmfOTMZ1AXv5xaYuLi2p4eDh+imMIQKBEAozfEmHnrCrJNvKpV1+h9Cl6mVLK49wFzI0bN9Tdu3d9MapVvUkdME8DxXYigwABCJRPgPFbPvOsNX748GFjWTNr/jLyle7gf/vtN61do6Ojam5uTq2vr8tb9Tb+5C5xbGxMy/fLL78oAUiwIyDr6maYnp5WS0tLEX+xg9hD7DA5OWlmD64Tb1KQExCoKQHGb5iGlR9eO3fu3NjPFJSGpSwE/LcSWXfvrOnKf1mDX1tb66qCuUY8PT3dNS8JvQk8e/YsF/+ORLOc2E7WmQgQgEB5BMxx2Ov62dHMLMf47ZAp5r/sE4v7NfO4mFr6k1LqHfyLFy+0HzeXL19W27Zt087FI+Zd/Pz8fDyZ45wEnjx5opWQfQ1p/DuZDx8+rOQuPx4ePXoUj3IMAQg4JsD4dQw4p3iZUZbd8qdPn45Kyox0SKHUTXYCQh5/6wSZBt6yZUsnmvhfHteKB58bFuJ6VPHYhuXnz5/V4OCg1mxsoeEgAgGnBBi/TvHmEi6PFV+5ckUrIzek165dC+o6WaqD12hkjNh06oxVkC0jAWyRERTZIBAgAcZvcUYxWU5NTanz589vVGCm+bwRKnWK3havPC5HCINAaFNRYVBBCwhUgwDjtxg7yV17q9WKnHsxUouT8nNxooqXZD6OdeLEieIrQWImAqYtuEBkwkYmCARBgPFbrBnEsctf6O8ECdbBy5pv/JEQcSgnT54s1kpIy0zgwYMHWt6DBw9qcSIQgEC4BBi/xdrm9u3bxQp0JC24NXh5//yrV6/UrVu3og154tzv3buXace3I06NFvvw4UN16tSpiIHYY2ZmJopzAAEIhEuA8VuubUJagw/GwZudsGMSWXe/dOkSzr0DpOT/MrVnvnlQXoqze/fukjWhOghAIC8Bxm9eYvb5Q3LwwW+y27p1q/r06ZM9dSTkJpB0cZDn4XHuuVFSAAKlE2D8lo48uAqDuYOXd81//fpV7d+/X62srKjXr1+rO3fuRMA6zxhmeTFLVIiDvgkkXRz46E/fOCkIgVIJMH5Lxa1VFtIdfDAOXiP034i8KejixYvRWrycZno4iVSx5+Qb8GfPntWE4tw1HEQgECwBxq9f04Tk4IOeot+xY8fG5rr4I1nm24P8mrJ+tXNxqJ9NaVFzCDB+m2PrLC0N+g6+0wBzA57s4I47/U4+/tsRkMcS5dO88SBr7mfOnImf4hgCEAiQAOM3DKNwB5/TDgcOHNBKmB+t0RKJ5CYgSyHynQCce250FICAdwKMX+8mCFaBStzBC72QfhUFa80+FFtYWFBHjhzZVFK+BR/6W5o2Kc0JCDSMAOM3PIOH5KuCXoMPz3T10kjW60znLksfa2trOPd6mZrW1JAA47eGRi24SaU6eJkGll83nT95a12WsLy8rGVj/V3D0VckaTPO5OTkxhvqeBSxL6QUgkBpBBi/paGudEWlOvhjx45psB4/fqzFu0Xi35CXPDj4bqSynZdNi+ZjcLJx8ddff80mgFwQgIA3Aoxfb+grV3Gpa/BJL1+Q6eC0O8akMqwP99/PZEPOzp07NQHw1HAQgUCwBBi/wZomUqyxa/Cyacu8+z537pySX6Ty9bh4kGl5ebud+R50eeEKm7/ipPIdC9N4wLnHaXAMgbAJMH7Dtk9o2pV6By+NF8e9Z8+evjjIjwO+KtcXuo1CSb/++5emVLvdtilOWQhAIAcBxm8OWB6zNvYOXpjLh0rkrjFvwLnnJbY5/9OnTzef5AwEIFAJAozfSpgpKCVL3WTXablMsbdaLSUfkMkSpqam2N2dBVSPPPPz8z1ykAwBCIRKgPEbqmXC1av0KXoThWyikzfTmV+Pk0e25G7/0KFDqZvwTHnEuxMwp46658yWwhR9Nk7kgkARBBi/RVB0L8O0k8/rpHcH7x43NUAAAhCAAASaR8DLFH3zMNNiCEAAAhCAQLkEcPDl8qY2CEAAAhCAQCkEcPClYKYSCEAAAhCAQLkEcPDl8qY2CEAAAhCAQCkEfpqYmJjIUpPsBHz79u3Gjvdv376pwcHBLMWCyYP+fk0Bf/jbEKD/2NCzLwt/e4Y2Evrm384QVlZW2kePHpXXlkV/x48fb8v5KgT092sl+MPfhgD9x4aefVn42zO0kWDDX143mhq+f//e3rdvX+TY405+ZGSkLekhB/T3ax34w9+GAP3Hhp59WfjbM7SRYMu/p4N//vx5onPvOPqXL1/a6O+8LPo7R5xaAfxT8ThPhL9zxKkVwD8Vj/PEpvPvucnu48ePqUsHq6urqem+E9HfrwXgD38bAvQfG3r2ZeFvz9BGgi3/ng5+aGgoVb/t27enpvtORH+/FoA//G0I0H9s6NmXhb89QxsJ1vx7zZHIGsDw8HDiNH1V1uDRv5eV3aXTf9yxzSIZ/lkoucsDf3dss0huOv+ea/ACUXbxya75zrq7/K/aLnr0zzIc3OSh/7jhmlUq/LOScpMP/m64ZpXaZP65Pjbz7t079f79e7Vr1y61d+9em5kHL2XR3wv2qFL4Ryi8HMDfC/aoUvhHKLwcNJF/LgfvxSpUCgEIQAACEIBAbgI9N9nllkgBCEAAAhCAAAS8E8DBezcBCkAAAhCAAASKJ4CDL54pEiEAAQhAAALeCeDgLU2wvLysZmdn1c2bN9XAwID2d/XqVXX//n0leQhuCNSV/4ULF6K+5IZcMVLhXwxHpOgEqtL/da0DjGV91IB8OoFWq9UeGxvTHh2MP0ZoHkvepaUlXQixvgnUmf/c3JzWr/qG5LAg/B3CbbjoKvT/qpiIXfR9/Oh68+aNGhkZ6aOkUouLi2p4eLivshT6nUCd+Se1TT4VGVJI0jGrfqH3/6S2hcY/K+sq5oN/sVZjij4nz6QOmEeE/DAQGYT+CNSZ/4cPH5Qs64Qc4B+ydaqtWxX6f+UIV2WqIRQ9R0dHtelTmYqfnp7eNP2+vr7eXlxcbE9OTm7KLzII/RGoK3/pK+ayTifeHyk3peDvhmvTpVal/1fNTpleVVu1RrnS99mzZ9pFWC52a2trPaszy8mFW9aZCPkImBzrwn9mZkbrVx3H3vmfj5K73PB3x7bJkqvS/6toI6boc8y5PHnyRMt9/fp1tW3bNu1cUuTw4cNqenpaS3r06JEWJ9KbQN34y5Sk7BY+ffp01PjR0dHoOLQD+IdmkWrrU7X+X0naVfxV4kvnzh1V538ePeROv1Ou8z9PefJu7DTTGOZhEhr/pKUbedIiND3jjDv9tvM/ntbrOLR2VZF/L8ZVSod/OdZiF32JP8vkOfl4YHdunIb745D4m7pMTU2p8+fPb0Aw0+rST0Jql6lLE/i7H2HZa4B/dlY2OZmit6FnUTbkqViLZlWmaCj8x8bGVKvVipx7ZQBaKgp/S4A1Kd7U/l+W+X4uq6Km12M+GhfKBa4pdgmNv1zY5K8p70SAf1NGWrZ2Nq3/Z6NSfC4cfPFMEyU+ePBAO3/w4EEtTsQtgdD43759222DA5MO/8AM4lmdpvV/X7hZgy+B/MOHD9WpU6eimuTufWZmJopz4JZA1fib65NVX4OHv9v+XTfpdev/Pu2Dg3dMP+nNX0tLS2r37t2Oa0a8EKgi/zpd4ODPOMxLoE79P2/bi87PJruiicbkJV3c5Hl4nHsMksND+DuEm0E0/DNAIgsEHBLAwTuCm3RxGx8fV2fOnHFUI2LjBOAfp1H+MfzLZ06NEDAJ4OBNIgXE5Rvw5tfmxLnLm+8I7gnA3z3jtBrgn0aHNAiURwAHXzBrubidPXtWk4pz13A4jcDfKd6ewuHfExEZIFAaAR6TKxC1fOrzxo0bmkRZc2daXkPiLAJ/Z2gzCYZ/JkxkgkBpBHDwBaCWjyZcvHhRzc7OatJw7hoOZxH4O0ObSTD8M2EiEwRKJ4CDt0S+sLCgjhw5sknK4uJiY95StqnxJZ6Af4mwE6qCfwIUTkEgEAKswVsYQtYbTecuL7FZW1vDuVtwzVoU/llJuckHfzdckQqBogjg4PskmbSZaHJycuMNdVm+Ed9ntRT7LwH4++0K8PfLn9ohkIUAb7LLQsnIY756U5Ll1bN8QMYA5Shad/6hv8kL/o46NmI3CITe/6tkJhx8TmvJhqKdO3dqpVhv13A4jTSBf8gXOPg77d4IV0qF3P+rZiCm6HNa7O7du1oJnLuGw3kE/s4Rp1YA/1Q8JEIgKALcwecwR9LdS47im7JW/Sthmxrk+ERT+Id6BwN/xx0c8RsEQu3/VTQPd/A5rPb06dMcuclaNAH4F000nzz45+NFbgj4JoCDz2GB+fn5HLnJWjQB+BdNNJ88+OfjRW4I+CbAFH0OC5hTRzmKJmZlij4RS9eTTeFvtjOUfmLq1dVQGRNCaZeprtnOUPU09a5LHP7FWRIHXxxLJEEAAhCAAASCIcAUfTCmQBEIQAACEIBAcQRw8MWxRBIEIAABCEAgGAI4+GBMgSIQgAAEIACB4gjg4ItjiSQIQAACEIBAMAR+mpiYmMiijewkffv2rXrx4oX69u2bGhwczFIsmDzo79cU8Ie/DQH6jw09+7Lwt2doI6Fv/u0MYWVlpX306NG2Uir6O378eFvOVyGgv18rwR/+NgToPzb07MvC356hjQQb/qpXxd+/f2/v27cvcuxxJz8yMtKW9JAD+vu1Dvzhb0OA/mNDz74s/O0Z2kiw5d/TwT9//jzRuXcc/cuXL230d14W/Z0jTq0A/ql4nCfC3zni1Argn4rHeWLT+ffcZPfx48fUpYPV1dXUdN+J6O/XAvCHvw0B+o8NPfuy8LdnaCPBln9PBz80NJSq3/bt21PTfSeiv18LwB/+NgToPzb07MvC356hjQRr/r3mSGQNYHh4OHGavipr8Ojfy8ru0uk/7thmkQz/LJTc5YG/O7ZZJDedf881eIEou/hk13xn3V3+V20XPfpnGQ5u8tB/3HDNKhX+WUm5yQd/N1yzSm0y/1wfm3n37p16//692rVrl9q7d6/NzIOXsujvBXtUKfwjFF4O4O8Fe1Qp/CMUXg6ayD+Xg/diFSqFAAQgAAEIQCA3gZ6b7HJLpAAEIAABCEAAAt4J4OC9mwAFIAABCEAAAsUTwMEXzxSJEIAABCAAAe8EcPDeTYACEIAABCAAgeIJ4OCLZ4pECEAAAhCAgHcCOHjvJkABCEAAAhCAQPEE/j+nZXJs14Zq5AAAAABJRU5ErkJggg==" | |
| } | |
| }, | |
| "cell_type": "markdown", | |
| "metadata": {}, | |
| "source": [ | |
| "" | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "execution_count": 2, | |
| "metadata": {}, | |
| "outputs": [], | |
| "source": [ | |
| "def at_most(bools, count):\n", | |
| " return AtMost(*(bools + [count]))\n", | |
| "\n", | |
| "def at_least(bools, count):\n", | |
| " return AtLeast(*(bools + [count]))\n", | |
| " \n", | |
| "def at_equal(bools, count):\n", | |
| " return And(at_most(bools, count), at_least(bools, count))" | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "execution_count": 21, | |
| "metadata": {}, | |
| "outputs": [ | |
| { | |
| "name": "stdout", | |
| "output_type": "stream", | |
| "text": [ | |
| "sat\n" | |
| ] | |
| }, | |
| { | |
| "data": { | |
| "text/html": [ | |
| "<table>\n", | |
| "<tr>\n", | |
| "<td style=\"border-top:1px black solid;;border-left:1px black solid;;border-right:1px black solid;\">.</td>\n", | |
| "<td style=\"border-left:1px black solid;;border-bottom:1px black solid;;border-right:1px black solid;\">3</td>\n", | |
| "<td style=\"border-top:1px black solid;;border-left:1px black solid;;border-right:1px black solid;\">3</td>\n", | |
| "<td style=\"border-left:1px black solid;;border-bottom:1px black solid;;border-right:1px black solid;\">3</td>\n", | |
| "<td style=\"border-top:1px black solid;;border-left:1px black solid;;border-right:1px black solid;\">.</td>\n", | |
| "</tr>\n", | |
| "<tr>\n", | |
| "<td style=\"border-left:1px black solid;\">.</td>\n", | |
| "<td style=\"border-top:1px black solid;;border-bottom:1px black solid;\">2</td>\n", | |
| "<td style=\"\">0</td>\n", | |
| "<td style=\"border-top:1px black solid;;border-bottom:1px black solid;\">.</td>\n", | |
| "<td style=\"border-bottom:1px black solid;;border-right:1px black solid;\">2</td>\n", | |
| "</tr>\n", | |
| "<tr>\n", | |
| "<td style=\"border-left:1px black solid;;border-right:1px black solid;\">.</td>\n", | |
| "<td style=\"border-top:1px black solid;;border-left:1px black solid;;border-right:1px black solid;\">.</td>\n", | |
| "<td style=\"border-left:1px black solid;;border-right:1px black solid;\">.</td>\n", | |
| "<td style=\"border-top:1px black solid;;border-left:1px black solid;;border-bottom:1px black solid;\">.</td>\n", | |
| "<td style=\"border-top:1px black solid;\">1</td>\n", | |
| "</tr>\n", | |
| "<tr>\n", | |
| "<td style=\"border-left:1px black solid;;border-right:1px black solid;\">.</td>\n", | |
| "<td style=\"border-left:1px black solid;;border-right:1px black solid;\">.</td>\n", | |
| "<td style=\"border-left:1px black solid;\">1</td>\n", | |
| "<td style=\"border-top:1px black solid;;border-right:1px black solid;\">.</td>\n", | |
| "<td style=\"border-left:1px black solid;;border-bottom:1px black solid;\">2</td>\n", | |
| "</tr>\n", | |
| "<tr>\n", | |
| "<td style=\"border-left:1px black solid;;border-bottom:1px black solid;;border-right:1px black solid;\">3</td>\n", | |
| "<td style=\"border-left:1px black solid;;border-right:1px black solid;\">.</td>\n", | |
| "<td style=\"border-left:1px black solid;;border-bottom:1px black solid;\">2</td>\n", | |
| "<td style=\"border-bottom:1px black solid;\">1</td>\n", | |
| "<td style=\"border-top:1px black solid;;border-bottom:1px black solid;;border-right:1px black solid;\">.</td>\n", | |
| "</tr>\n", | |
| "</table>" | |
| ] | |
| }, | |
| "metadata": {}, | |
| "output_type": "display_data" | |
| } | |
| ], | |
| "source": [ | |
| "puzzle = \"\"\"\n", | |
| ".20.\n", | |
| "2..1\n", | |
| "3..2\n", | |
| ".11.\n", | |
| "\"\"\"\n", | |
| "\n", | |
| "puzzle = \"\"\"\n", | |
| ".3.2111.3.\n", | |
| "3.1....1.1\n", | |
| ".020..020.\n", | |
| "1.3.11.3.1\n", | |
| "2..3..2..1\n", | |
| "2..3..2..1\n", | |
| "1.2.21.3.1\n", | |
| ".010..010.\n", | |
| "3.2....2.1\n", | |
| ".2.2121.1.\n", | |
| "\"\"\"\n", | |
| "\n", | |
| "puzzle = \"\"\"\n", | |
| ".333.\n", | |
| ".20.2\n", | |
| "....1\n", | |
| "..1.2\n", | |
| "3.21.\n", | |
| "\"\"\"\n", | |
| "\n", | |
| "puzzle2 = \"\"\"\n", | |
| ".22...3\n", | |
| ".3..2..\n", | |
| "......2\n", | |
| "..3.12.\n", | |
| "1..333.\n", | |
| ".2.2..1\n", | |
| ".2223..\n", | |
| "\"\"\"\n", | |
| "\n", | |
| "puzzle = np.array([list(row) for row in puzzle.strip().split(\"\\n\")])\n", | |
| "h, w = [t+1 for t in puzzle.shape]\n", | |
| "\n", | |
| "directs = [(-1, 0), (0, 1), (1, 0), (0, -1)]\n", | |
| "block_directs = [(0, 0), (0, 1), (1, 0), (1, 1)]\n", | |
| "edge_locations = set(itertools.product(range(h), range(w)))\n", | |
| "block_locations = set(itertools.product(range(h-1), range(w-1)))\n", | |
| "s = Solver()\n", | |
| "\n", | |
| "edges = {}\n", | |
| "for y, x in edge_locations:\n", | |
| " for dy, dx in directs:\n", | |
| " if dy >= 0 and dx >= 0:\n", | |
| " y2, x2 = y + dy, x + dx\n", | |
| " if (y2, x2) in edge_locations:\n", | |
| " edges[y, x, y2, x2] = Bool(\"link_{}_{}_{}_{}\".format(y, x, y2, x2))\n", | |
| "\n", | |
| "blocks = {}\n", | |
| "for y, x in block_locations:\n", | |
| " if puzzle[y, x] != \".\":\n", | |
| " blocks[y, x] = Bool(\"block_{}_{}\".format(y, x))\n", | |
| " \n", | |
| "dot_links = defaultdict(list)\n", | |
| "block_links = defaultdict(list)\n", | |
| "row_blocks = defaultdict(list)\n", | |
| "col_blocks = defaultdict(list)\n", | |
| "\n", | |
| "for y, x in edge_locations:\n", | |
| " for dy, dx in directs:\n", | |
| " y2, x2 = y + dy, x + dx\n", | |
| " key1 = y, x, y2, x2\n", | |
| " key2 = y2, x2, y, x\n", | |
| " if key1 in edges:\n", | |
| " dot_links[y, x].append(edges[key1])\n", | |
| " if key2 in edges:\n", | |
| " dot_links[y, x].append(edges[key2])\n", | |
| " \n", | |
| "for y, x in block_locations:\n", | |
| " block_links[y, x].append(edges[y, x, y, x+1])\n", | |
| " block_links[y, x].append(edges[y, x, y+1, x])\n", | |
| " block_links[y, x].append(edges[y+1, x, y+1, x+1])\n", | |
| " block_links[y, x].append(edges[y, x+1, y+1, x+1])\n", | |
| " \n", | |
| " if (y, x) in blocks:\n", | |
| " row_blocks[y].append(blocks[y, x])\n", | |
| " col_blocks[x].append(blocks[y, x])\n", | |
| " \n", | |
| "for links in dot_links.values():\n", | |
| " args2 = links + [2]\n", | |
| " args0 = links + [0]\n", | |
| " s.add(Or(at_equal(links, 0), at_equal(links, 2)))\n", | |
| " \n", | |
| "for key, val in block_links.items():\n", | |
| " c = puzzle[key]\n", | |
| " if c != \".\":\n", | |
| " #s.add(blocks[key] == at_equal(val, int(c)))\n", | |
| " s.add(at_equal(val, int(c)))\n", | |
| " \n", | |
| "for val in row_blocks.values():\n", | |
| " s.add(at_equal(val, len(val) - 1))\n", | |
| " \n", | |
| "for val in col_blocks.values():\n", | |
| " s.add(at_equal(val, len(val) - 1))\n", | |
| " \n", | |
| "print(s.check())\n", | |
| "m = s.model()\n", | |
| "\n", | |
| "html = [\"<table>\"]\n", | |
| "for y in range(h-1):\n", | |
| " html.append(\"<tr>\") \n", | |
| " for x in range(w-1):\n", | |
| " edges = []\n", | |
| " for edge, border in zip(block_links[y, x], (\"top\", \"left\", \"bottom\", \"right\")):\n", | |
| " if m[edge]:\n", | |
| " edges.append(\"border-{}:1px black solid;\".format(border))\n", | |
| " html.append('<td style=\"{}\">{}</td>'.format(\";\".join(edges), puzzle[y, x]))\n", | |
| " html.append(\"</tr>\")\n", | |
| "html.append(\"</table>\")\n", | |
| "display_html(\"\\n\".join(html), raw=True)" | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "execution_count": 11, | |
| "metadata": {}, | |
| "outputs": [ | |
| { | |
| "data": { | |
| "text/plain": [ | |
| "[link_0_0_0_1, link_0_0_1_0, link_1_0_1_1, link_0_1_1_1]" | |
| ] | |
| }, | |
| "execution_count": 11, | |
| "metadata": {}, | |
| "output_type": "execute_result" | |
| } | |
| ], | |
| "source": [ | |
| "block_links[0, 0]" | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "execution_count": 16, | |
| "metadata": {}, | |
| "outputs": [ | |
| { | |
| "data": { | |
| "text/plain": [ | |
| "[True, False, False, True, False, True, True, False]" | |
| ] | |
| }, | |
| "execution_count": 16, | |
| "metadata": {}, | |
| "output_type": "execute_result" | |
| } | |
| ], | |
| "source": [ | |
| "[m[b] for b in blocks.values()]" | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "execution_count": 78, | |
| "metadata": {}, | |
| "outputs": [ | |
| { | |
| "name": "stdout", | |
| "output_type": "stream", | |
| "text": [ | |
| "[[0 0 0 0 0 0 0 0 0]\n", | |
| " [0 0 0 0 0 0 0 0 0]\n", | |
| " [0 0 0 0 0 0 0 0 0]\n", | |
| " [0 0 0 0 1 1 1 0 0]\n", | |
| " [0 0 0 0 1 0 1 1 1]\n", | |
| " [0 0 0 0 0 0 0 0 1]\n", | |
| " [0 0 0 0 0 0 0 0 0]\n", | |
| " [0 0 0 0 0 0 0 0 0]\n", | |
| " [0 0 0 0 0 0 0 0 0]]\n" | |
| ] | |
| } | |
| ], | |
| "source": [ | |
| "h, w = 9, 9\n", | |
| "y0, x0 = 4, 4\n", | |
| "locations = list(itertools.product(range(h), range(w)))\n", | |
| "cells = {}\n", | |
| "paths = {}\n", | |
| "\n", | |
| "s = Solver()\n", | |
| "\n", | |
| "for y, x in locations:\n", | |
| " cells[y, x] = Bool(\"C_{}_{}\".format(y, x))\n", | |
| " paths[y, x, 0] = Bool(\"S_{}_{}_0\".format(y, x))\n", | |
| " if x == x0 and y == y0:\n", | |
| " s.add(paths[y, x, 0])\n", | |
| " s.add(cells[y, x])\n", | |
| " else:\n", | |
| " s.add(Not(paths[y, x, 0]))\n", | |
| "\n", | |
| "directions = [(0, 1), (0, -1), (-1, 0), (1, 0)]\n", | |
| "\n", | |
| "for step in range(1, 10):\n", | |
| " for y, x in locations:\n", | |
| " paths[y, x, step] = Bool(\"S_{}_{}_{}\".format(y, x, step))\n", | |
| " neighbours = []\n", | |
| " for dy, dx in directions:\n", | |
| " y2, x2 = y + dy, x + dx\n", | |
| " if (y2, x2) in cells:\n", | |
| " neighbours.append(paths[y2, x2, step-1])\n", | |
| " s.add(paths[y, x, step] == And(cells[y, x], Or(neighbours)))\n", | |
| "\n", | |
| "rows = defaultdict(list)\n", | |
| "for y, x, step in paths:\n", | |
| " rows[y, x].append(paths[y, x, step])\n", | |
| "\n", | |
| "for y, x in rows:\n", | |
| " s.add(cells[y, x] == Or(rows[y, x]))\n", | |
| " \n", | |
| "s.add(at_equal(list(cells.values()), 8))\n", | |
| "s.check()\n", | |
| "m = s.model()\n", | |
| "arr = np.zeros((h, w), int)\n", | |
| "prr = np.zeros((h, w), int)\n", | |
| "for y, x in locations:\n", | |
| " arr[y, x] = bool(m[cells[y, x]])\n", | |
| " prr[y, x] = bool(m[paths[y, x, 1]])\n", | |
| "#print(arr)\n", | |
| "print(arr)" | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "execution_count": 52, | |
| "metadata": {}, | |
| "outputs": [ | |
| { | |
| "data": { | |
| "text/plain": [ | |
| "{(0, 0, 0): S_0_0_0,\n", | |
| " (0, 0, 1): S_0_0_1,\n", | |
| " (0, 0, 2): S_0_0_2,\n", | |
| " (0, 0, 3): S_0_0_3,\n", | |
| " (0, 0, 4): S_0_0_4,\n", | |
| " (0, 0, 5): S_0_0_5,\n", | |
| " (0, 0, 6): S_0_0_6,\n", | |
| " (0, 1, 0): S_0_1_0,\n", | |
| " (0, 1, 1): S_0_1_1,\n", | |
| " (0, 1, 2): S_0_1_2,\n", | |
| " (0, 1, 3): S_0_1_3,\n", | |
| " (0, 1, 4): S_0_1_4,\n", | |
| " (0, 1, 5): S_0_1_5,\n", | |
| " (0, 1, 6): S_0_1_6,\n", | |
| " (0, 2, 0): S_0_2_0,\n", | |
| " (0, 2, 1): S_0_2_1,\n", | |
| " (0, 2, 2): S_0_2_2,\n", | |
| " (0, 2, 3): S_0_2_3,\n", | |
| " (0, 2, 4): S_0_2_4,\n", | |
| " (0, 2, 5): S_0_2_5,\n", | |
| " (0, 2, 6): S_0_2_6,\n", | |
| " (0, 3, 0): S_0_3_0,\n", | |
| " (0, 3, 1): S_0_3_1,\n", | |
| " (0, 3, 2): S_0_3_2,\n", | |
| " (0, 3, 3): S_0_3_3,\n", | |
| " (0, 3, 4): S_0_3_4,\n", | |
| " (0, 3, 5): S_0_3_5,\n", | |
| " (0, 3, 6): S_0_3_6,\n", | |
| " (0, 4, 0): S_0_4_0,\n", | |
| " (0, 4, 1): S_0_4_1,\n", | |
| " (0, 4, 2): S_0_4_2,\n", | |
| " (0, 4, 3): S_0_4_3,\n", | |
| " (0, 4, 4): S_0_4_4,\n", | |
| " (0, 4, 5): S_0_4_5,\n", | |
| " (0, 4, 6): S_0_4_6,\n", | |
| " (0, 5, 0): S_0_5_0,\n", | |
| " (0, 5, 1): S_0_5_1,\n", | |
| " (0, 5, 2): S_0_5_2,\n", | |
| " (0, 5, 3): S_0_5_3,\n", | |
| " (0, 5, 4): S_0_5_4,\n", | |
| " (0, 5, 5): S_0_5_5,\n", | |
| " (0, 5, 6): S_0_5_6,\n", | |
| " (0, 6, 0): S_0_6_0,\n", | |
| " (0, 6, 1): S_0_6_1,\n", | |
| " (0, 6, 2): S_0_6_2,\n", | |
| " (0, 6, 3): S_0_6_3,\n", | |
| " (0, 6, 4): S_0_6_4,\n", | |
| " (0, 6, 5): S_0_6_5,\n", | |
| " (0, 6, 6): S_0_6_6,\n", | |
| " (0, 7, 0): S_0_7_0,\n", | |
| " (0, 7, 1): S_0_7_1,\n", | |
| " (0, 7, 2): S_0_7_2,\n", | |
| " (0, 7, 3): S_0_7_3,\n", | |
| " (0, 7, 4): S_0_7_4,\n", | |
| " (0, 7, 5): S_0_7_5,\n", | |
| " (0, 7, 6): S_0_7_6,\n", | |
| " (0, 8, 0): S_0_8_0,\n", | |
| " (0, 8, 1): S_0_8_1,\n", | |
| " (0, 8, 2): S_0_8_2,\n", | |
| " (0, 8, 3): S_0_8_3,\n", | |
| " (0, 8, 4): S_0_8_4,\n", | |
| " (0, 8, 5): S_0_8_5,\n", | |
| " (0, 8, 6): S_0_8_6,\n", | |
| " (1, 0, 0): S_1_0_0,\n", | |
| " (1, 0, 1): S_1_0_1,\n", | |
| " (1, 0, 2): S_1_0_2,\n", | |
| " (1, 0, 3): S_1_0_3,\n", | |
| " (1, 0, 4): S_1_0_4,\n", | |
| " (1, 0, 5): S_1_0_5,\n", | |
| " (1, 0, 6): S_1_0_6,\n", | |
| " (1, 1, 0): S_1_1_0,\n", | |
| " (1, 1, 1): S_1_1_1,\n", | |
| " (1, 1, 2): S_1_1_2,\n", | |
| " (1, 1, 3): S_1_1_3,\n", | |
| " (1, 1, 4): S_1_1_4,\n", | |
| " (1, 1, 5): S_1_1_5,\n", | |
| " (1, 1, 6): S_1_1_6,\n", | |
| " (1, 2, 0): S_1_2_0,\n", | |
| " (1, 2, 1): S_1_2_1,\n", | |
| " (1, 2, 2): S_1_2_2,\n", | |
| " (1, 2, 3): S_1_2_3,\n", | |
| " (1, 2, 4): S_1_2_4,\n", | |
| " (1, 2, 5): S_1_2_5,\n", | |
| " (1, 2, 6): S_1_2_6,\n", | |
| " (1, 3, 0): S_1_3_0,\n", | |
| " (1, 3, 1): S_1_3_1,\n", | |
| " (1, 3, 2): S_1_3_2,\n", | |
| " (1, 3, 3): S_1_3_3,\n", | |
| " (1, 3, 4): S_1_3_4,\n", | |
| " (1, 3, 5): S_1_3_5,\n", | |
| " (1, 3, 6): S_1_3_6,\n", | |
| " (1, 4, 0): S_1_4_0,\n", | |
| " (1, 4, 1): S_1_4_1,\n", | |
| " (1, 4, 2): S_1_4_2,\n", | |
| " (1, 4, 3): S_1_4_3,\n", | |
| " (1, 4, 4): S_1_4_4,\n", | |
| " (1, 4, 5): S_1_4_5,\n", | |
| " (1, 4, 6): S_1_4_6,\n", | |
| " (1, 5, 0): S_1_5_0,\n", | |
| " (1, 5, 1): S_1_5_1,\n", | |
| " (1, 5, 2): S_1_5_2,\n", | |
| " (1, 5, 3): S_1_5_3,\n", | |
| " (1, 5, 4): S_1_5_4,\n", | |
| " (1, 5, 5): S_1_5_5,\n", | |
| " (1, 5, 6): S_1_5_6,\n", | |
| " (1, 6, 0): S_1_6_0,\n", | |
| " (1, 6, 1): S_1_6_1,\n", | |
| " (1, 6, 2): S_1_6_2,\n", | |
| " (1, 6, 3): S_1_6_3,\n", | |
| " (1, 6, 4): S_1_6_4,\n", | |
| " (1, 6, 5): S_1_6_5,\n", | |
| " (1, 6, 6): S_1_6_6,\n", | |
| " (1, 7, 0): S_1_7_0,\n", | |
| " (1, 7, 1): S_1_7_1,\n", | |
| " (1, 7, 2): S_1_7_2,\n", | |
| " (1, 7, 3): S_1_7_3,\n", | |
| " (1, 7, 4): S_1_7_4,\n", | |
| " (1, 7, 5): S_1_7_5,\n", | |
| " (1, 7, 6): S_1_7_6,\n", | |
| " (1, 8, 0): S_1_8_0,\n", | |
| " (1, 8, 1): S_1_8_1,\n", | |
| " (1, 8, 2): S_1_8_2,\n", | |
| " (1, 8, 3): S_1_8_3,\n", | |
| " (1, 8, 4): S_1_8_4,\n", | |
| " (1, 8, 5): S_1_8_5,\n", | |
| " (1, 8, 6): S_1_8_6,\n", | |
| " (2, 0, 0): S_2_0_0,\n", | |
| " (2, 0, 1): S_2_0_1,\n", | |
| " (2, 0, 2): S_2_0_2,\n", | |
| " (2, 0, 3): S_2_0_3,\n", | |
| " (2, 0, 4): S_2_0_4,\n", | |
| " (2, 0, 5): S_2_0_5,\n", | |
| " (2, 0, 6): S_2_0_6,\n", | |
| " (2, 1, 0): S_2_1_0,\n", | |
| " (2, 1, 1): S_2_1_1,\n", | |
| " (2, 1, 2): S_2_1_2,\n", | |
| " (2, 1, 3): S_2_1_3,\n", | |
| " (2, 1, 4): S_2_1_4,\n", | |
| " (2, 1, 5): S_2_1_5,\n", | |
| " (2, 1, 6): S_2_1_6,\n", | |
| " (2, 2, 0): S_2_2_0,\n", | |
| " (2, 2, 1): S_2_2_1,\n", | |
| " (2, 2, 2): S_2_2_2,\n", | |
| " (2, 2, 3): S_2_2_3,\n", | |
| " (2, 2, 4): S_2_2_4,\n", | |
| " (2, 2, 5): S_2_2_5,\n", | |
| " (2, 2, 6): S_2_2_6,\n", | |
| " (2, 3, 0): S_2_3_0,\n", | |
| " (2, 3, 1): S_2_3_1,\n", | |
| " (2, 3, 2): S_2_3_2,\n", | |
| " (2, 3, 3): S_2_3_3,\n", | |
| " (2, 3, 4): S_2_3_4,\n", | |
| " (2, 3, 5): S_2_3_5,\n", | |
| " (2, 3, 6): S_2_3_6,\n", | |
| " (2, 4, 0): S_2_4_0,\n", | |
| " (2, 4, 1): S_2_4_1,\n", | |
| " (2, 4, 2): S_2_4_2,\n", | |
| " (2, 4, 3): S_2_4_3,\n", | |
| " (2, 4, 4): S_2_4_4,\n", | |
| " (2, 4, 5): S_2_4_5,\n", | |
| " (2, 4, 6): S_2_4_6,\n", | |
| " (2, 5, 0): S_2_5_0,\n", | |
| " (2, 5, 1): S_2_5_1,\n", | |
| " (2, 5, 2): S_2_5_2,\n", | |
| " (2, 5, 3): S_2_5_3,\n", | |
| " (2, 5, 4): S_2_5_4,\n", | |
| " (2, 5, 5): S_2_5_5,\n", | |
| " (2, 5, 6): S_2_5_6,\n", | |
| " (2, 6, 0): S_2_6_0,\n", | |
| " (2, 6, 1): S_2_6_1,\n", | |
| " (2, 6, 2): S_2_6_2,\n", | |
| " (2, 6, 3): S_2_6_3,\n", | |
| " (2, 6, 4): S_2_6_4,\n", | |
| " (2, 6, 5): S_2_6_5,\n", | |
| " (2, 6, 6): S_2_6_6,\n", | |
| " (2, 7, 0): S_2_7_0,\n", | |
| " (2, 7, 1): S_2_7_1,\n", | |
| " (2, 7, 2): S_2_7_2,\n", | |
| " (2, 7, 3): S_2_7_3,\n", | |
| " (2, 7, 4): S_2_7_4,\n", | |
| " (2, 7, 5): S_2_7_5,\n", | |
| " (2, 7, 6): S_2_7_6,\n", | |
| " (2, 8, 0): S_2_8_0,\n", | |
| " (2, 8, 1): S_2_8_1,\n", | |
| " (2, 8, 2): S_2_8_2,\n", | |
| " (2, 8, 3): S_2_8_3,\n", | |
| " (2, 8, 4): S_2_8_4,\n", | |
| " (2, 8, 5): S_2_8_5,\n", | |
| " (2, 8, 6): S_2_8_6,\n", | |
| " (3, 0, 0): S_3_0_0,\n", | |
| " (3, 0, 1): S_3_0_1,\n", | |
| " (3, 0, 2): S_3_0_2,\n", | |
| " (3, 0, 3): S_3_0_3,\n", | |
| " (3, 0, 4): S_3_0_4,\n", | |
| " (3, 0, 5): S_3_0_5,\n", | |
| " (3, 0, 6): S_3_0_6,\n", | |
| " (3, 1, 0): S_3_1_0,\n", | |
| " (3, 1, 1): S_3_1_1,\n", | |
| " (3, 1, 2): S_3_1_2,\n", | |
| " (3, 1, 3): S_3_1_3,\n", | |
| " (3, 1, 4): S_3_1_4,\n", | |
| " (3, 1, 5): S_3_1_5,\n", | |
| " (3, 1, 6): S_3_1_6,\n", | |
| " (3, 2, 0): S_3_2_0,\n", | |
| " (3, 2, 1): S_3_2_1,\n", | |
| " (3, 2, 2): S_3_2_2,\n", | |
| " (3, 2, 3): S_3_2_3,\n", | |
| " (3, 2, 4): S_3_2_4,\n", | |
| " (3, 2, 5): S_3_2_5,\n", | |
| " (3, 2, 6): S_3_2_6,\n", | |
| " (3, 3, 0): S_3_3_0,\n", | |
| " (3, 3, 1): S_3_3_1,\n", | |
| " (3, 3, 2): S_3_3_2,\n", | |
| " (3, 3, 3): S_3_3_3,\n", | |
| " (3, 3, 4): S_3_3_4,\n", | |
| " (3, 3, 5): S_3_3_5,\n", | |
| " (3, 3, 6): S_3_3_6,\n", | |
| " (3, 4, 0): S_3_4_0,\n", | |
| " (3, 4, 1): S_3_4_1,\n", | |
| " (3, 4, 2): S_3_4_2,\n", | |
| " (3, 4, 3): S_3_4_3,\n", | |
| " (3, 4, 4): S_3_4_4,\n", | |
| " (3, 4, 5): S_3_4_5,\n", | |
| " (3, 4, 6): S_3_4_6,\n", | |
| " (3, 5, 0): S_3_5_0,\n", | |
| " (3, 5, 1): S_3_5_1,\n", | |
| " (3, 5, 2): S_3_5_2,\n", | |
| " (3, 5, 3): S_3_5_3,\n", | |
| " (3, 5, 4): S_3_5_4,\n", | |
| " (3, 5, 5): S_3_5_5,\n", | |
| " (3, 5, 6): S_3_5_6,\n", | |
| " (3, 6, 0): S_3_6_0,\n", | |
| " (3, 6, 1): S_3_6_1,\n", | |
| " (3, 6, 2): S_3_6_2,\n", | |
| " (3, 6, 3): S_3_6_3,\n", | |
| " (3, 6, 4): S_3_6_4,\n", | |
| " (3, 6, 5): S_3_6_5,\n", | |
| " (3, 6, 6): S_3_6_6,\n", | |
| " (3, 7, 0): S_3_7_0,\n", | |
| " (3, 7, 1): S_3_7_1,\n", | |
| " (3, 7, 2): S_3_7_2,\n", | |
| " (3, 7, 3): S_3_7_3,\n", | |
| " (3, 7, 4): S_3_7_4,\n", | |
| " (3, 7, 5): S_3_7_5,\n", | |
| " (3, 7, 6): S_3_7_6,\n", | |
| " (3, 8, 0): S_3_8_0,\n", | |
| " (3, 8, 1): S_3_8_1,\n", | |
| " (3, 8, 2): S_3_8_2,\n", | |
| " (3, 8, 3): S_3_8_3,\n", | |
| " (3, 8, 4): S_3_8_4,\n", | |
| " (3, 8, 5): S_3_8_5,\n", | |
| " (3, 8, 6): S_3_8_6,\n", | |
| " (4, 0, 0): S_4_0_0,\n", | |
| " (4, 0, 1): S_4_0_1,\n", | |
| " (4, 0, 2): S_4_0_2,\n", | |
| " (4, 0, 3): S_4_0_3,\n", | |
| " (4, 0, 4): S_4_0_4,\n", | |
| " (4, 0, 5): S_4_0_5,\n", | |
| " (4, 0, 6): S_4_0_6,\n", | |
| " (4, 1, 0): S_4_1_0,\n", | |
| " (4, 1, 1): S_4_1_1,\n", | |
| " (4, 1, 2): S_4_1_2,\n", | |
| " (4, 1, 3): S_4_1_3,\n", | |
| " (4, 1, 4): S_4_1_4,\n", | |
| " (4, 1, 5): S_4_1_5,\n", | |
| " (4, 1, 6): S_4_1_6,\n", | |
| " (4, 2, 0): S_4_2_0,\n", | |
| " (4, 2, 1): S_4_2_1,\n", | |
| " (4, 2, 2): S_4_2_2,\n", | |
| " (4, 2, 3): S_4_2_3,\n", | |
| " (4, 2, 4): S_4_2_4,\n", | |
| " (4, 2, 5): S_4_2_5,\n", | |
| " (4, 2, 6): S_4_2_6,\n", | |
| " (4, 3, 0): S_4_3_0,\n", | |
| " (4, 3, 1): S_4_3_1,\n", | |
| " (4, 3, 2): S_4_3_2,\n", | |
| " (4, 3, 3): S_4_3_3,\n", | |
| " (4, 3, 4): S_4_3_4,\n", | |
| " (4, 3, 5): S_4_3_5,\n", | |
| " (4, 3, 6): S_4_3_6,\n", | |
| " (4, 4, 0): S_4_4_0,\n", | |
| " (4, 4, 1): S_4_4_1,\n", | |
| " (4, 4, 2): S_4_4_2,\n", | |
| " (4, 4, 3): S_4_4_3,\n", | |
| " (4, 4, 4): S_4_4_4,\n", | |
| " (4, 4, 5): S_4_4_5,\n", | |
| " (4, 4, 6): S_4_4_6,\n", | |
| " (4, 5, 0): S_4_5_0,\n", | |
| " (4, 5, 1): S_4_5_1,\n", | |
| " (4, 5, 2): S_4_5_2,\n", | |
| " (4, 5, 3): S_4_5_3,\n", | |
| " (4, 5, 4): S_4_5_4,\n", | |
| " (4, 5, 5): S_4_5_5,\n", | |
| " (4, 5, 6): S_4_5_6,\n", | |
| " (4, 6, 0): S_4_6_0,\n", | |
| " (4, 6, 1): S_4_6_1,\n", | |
| " (4, 6, 2): S_4_6_2,\n", | |
| " (4, 6, 3): S_4_6_3,\n", | |
| " (4, 6, 4): S_4_6_4,\n", | |
| " (4, 6, 5): S_4_6_5,\n", | |
| " (4, 6, 6): S_4_6_6,\n", | |
| " (4, 7, 0): S_4_7_0,\n", | |
| " (4, 7, 1): S_4_7_1,\n", | |
| " (4, 7, 2): S_4_7_2,\n", | |
| " (4, 7, 3): S_4_7_3,\n", | |
| " (4, 7, 4): S_4_7_4,\n", | |
| " (4, 7, 5): S_4_7_5,\n", | |
| " (4, 7, 6): S_4_7_6,\n", | |
| " (4, 8, 0): S_4_8_0,\n", | |
| " (4, 8, 1): S_4_8_1,\n", | |
| " (4, 8, 2): S_4_8_2,\n", | |
| " (4, 8, 3): S_4_8_3,\n", | |
| " (4, 8, 4): S_4_8_4,\n", | |
| " (4, 8, 5): S_4_8_5,\n", | |
| " (4, 8, 6): S_4_8_6,\n", | |
| " (5, 0, 0): S_5_0_0,\n", | |
| " (5, 0, 1): S_5_0_1,\n", | |
| " (5, 0, 2): S_5_0_2,\n", | |
| " (5, 0, 3): S_5_0_3,\n", | |
| " (5, 0, 4): S_5_0_4,\n", | |
| " (5, 0, 5): S_5_0_5,\n", | |
| " (5, 0, 6): S_5_0_6,\n", | |
| " (5, 1, 0): S_5_1_0,\n", | |
| " (5, 1, 1): S_5_1_1,\n", | |
| " (5, 1, 2): S_5_1_2,\n", | |
| " (5, 1, 3): S_5_1_3,\n", | |
| " (5, 1, 4): S_5_1_4,\n", | |
| " (5, 1, 5): S_5_1_5,\n", | |
| " (5, 1, 6): S_5_1_6,\n", | |
| " (5, 2, 0): S_5_2_0,\n", | |
| " (5, 2, 1): S_5_2_1,\n", | |
| " (5, 2, 2): S_5_2_2,\n", | |
| " (5, 2, 3): S_5_2_3,\n", | |
| " (5, 2, 4): S_5_2_4,\n", | |
| " (5, 2, 5): S_5_2_5,\n", | |
| " (5, 2, 6): S_5_2_6,\n", | |
| " (5, 3, 0): S_5_3_0,\n", | |
| " (5, 3, 1): S_5_3_1,\n", | |
| " (5, 3, 2): S_5_3_2,\n", | |
| " (5, 3, 3): S_5_3_3,\n", | |
| " (5, 3, 4): S_5_3_4,\n", | |
| " (5, 3, 5): S_5_3_5,\n", | |
| " (5, 3, 6): S_5_3_6,\n", | |
| " (5, 4, 0): S_5_4_0,\n", | |
| " (5, 4, 1): S_5_4_1,\n", | |
| " (5, 4, 2): S_5_4_2,\n", | |
| " (5, 4, 3): S_5_4_3,\n", | |
| " (5, 4, 4): S_5_4_4,\n", | |
| " (5, 4, 5): S_5_4_5,\n", | |
| " (5, 4, 6): S_5_4_6,\n", | |
| " (5, 5, 0): S_5_5_0,\n", | |
| " (5, 5, 1): S_5_5_1,\n", | |
| " (5, 5, 2): S_5_5_2,\n", | |
| " (5, 5, 3): S_5_5_3,\n", | |
| " (5, 5, 4): S_5_5_4,\n", | |
| " (5, 5, 5): S_5_5_5,\n", | |
| " (5, 5, 6): S_5_5_6,\n", | |
| " (5, 6, 0): S_5_6_0,\n", | |
| " (5, 6, 1): S_5_6_1,\n", | |
| " (5, 6, 2): S_5_6_2,\n", | |
| " (5, 6, 3): S_5_6_3,\n", | |
| " (5, 6, 4): S_5_6_4,\n", | |
| " (5, 6, 5): S_5_6_5,\n", | |
| " (5, 6, 6): S_5_6_6,\n", | |
| " (5, 7, 0): S_5_7_0,\n", | |
| " (5, 7, 1): S_5_7_1,\n", | |
| " (5, 7, 2): S_5_7_2,\n", | |
| " (5, 7, 3): S_5_7_3,\n", | |
| " (5, 7, 4): S_5_7_4,\n", | |
| " (5, 7, 5): S_5_7_5,\n", | |
| " (5, 7, 6): S_5_7_6,\n", | |
| " (5, 8, 0): S_5_8_0,\n", | |
| " (5, 8, 1): S_5_8_1,\n", | |
| " (5, 8, 2): S_5_8_2,\n", | |
| " (5, 8, 3): S_5_8_3,\n", | |
| " (5, 8, 4): S_5_8_4,\n", | |
| " (5, 8, 5): S_5_8_5,\n", | |
| " (5, 8, 6): S_5_8_6,\n", | |
| " (6, 0, 0): S_6_0_0,\n", | |
| " (6, 0, 1): S_6_0_1,\n", | |
| " (6, 0, 2): S_6_0_2,\n", | |
| " (6, 0, 3): S_6_0_3,\n", | |
| " (6, 0, 4): S_6_0_4,\n", | |
| " (6, 0, 5): S_6_0_5,\n", | |
| " (6, 0, 6): S_6_0_6,\n", | |
| " (6, 1, 0): S_6_1_0,\n", | |
| " (6, 1, 1): S_6_1_1,\n", | |
| " (6, 1, 2): S_6_1_2,\n", | |
| " (6, 1, 3): S_6_1_3,\n", | |
| " (6, 1, 4): S_6_1_4,\n", | |
| " (6, 1, 5): S_6_1_5,\n", | |
| " (6, 1, 6): S_6_1_6,\n", | |
| " (6, 2, 0): S_6_2_0,\n", | |
| " (6, 2, 1): S_6_2_1,\n", | |
| " (6, 2, 2): S_6_2_2,\n", | |
| " (6, 2, 3): S_6_2_3,\n", | |
| " (6, 2, 4): S_6_2_4,\n", | |
| " (6, 2, 5): S_6_2_5,\n", | |
| " (6, 2, 6): S_6_2_6,\n", | |
| " (6, 3, 0): S_6_3_0,\n", | |
| " (6, 3, 1): S_6_3_1,\n", | |
| " (6, 3, 2): S_6_3_2,\n", | |
| " (6, 3, 3): S_6_3_3,\n", | |
| " (6, 3, 4): S_6_3_4,\n", | |
| " (6, 3, 5): S_6_3_5,\n", | |
| " (6, 3, 6): S_6_3_6,\n", | |
| " (6, 4, 0): S_6_4_0,\n", | |
| " (6, 4, 1): S_6_4_1,\n", | |
| " (6, 4, 2): S_6_4_2,\n", | |
| " (6, 4, 3): S_6_4_3,\n", | |
| " (6, 4, 4): S_6_4_4,\n", | |
| " (6, 4, 5): S_6_4_5,\n", | |
| " (6, 4, 6): S_6_4_6,\n", | |
| " (6, 5, 0): S_6_5_0,\n", | |
| " (6, 5, 1): S_6_5_1,\n", | |
| " (6, 5, 2): S_6_5_2,\n", | |
| " (6, 5, 3): S_6_5_3,\n", | |
| " (6, 5, 4): S_6_5_4,\n", | |
| " (6, 5, 5): S_6_5_5,\n", | |
| " (6, 5, 6): S_6_5_6,\n", | |
| " (6, 6, 0): S_6_6_0,\n", | |
| " (6, 6, 1): S_6_6_1,\n", | |
| " (6, 6, 2): S_6_6_2,\n", | |
| " (6, 6, 3): S_6_6_3,\n", | |
| " (6, 6, 4): S_6_6_4,\n", | |
| " (6, 6, 5): S_6_6_5,\n", | |
| " (6, 6, 6): S_6_6_6,\n", | |
| " (6, 7, 0): S_6_7_0,\n", | |
| " (6, 7, 1): S_6_7_1,\n", | |
| " (6, 7, 2): S_6_7_2,\n", | |
| " (6, 7, 3): S_6_7_3,\n", | |
| " (6, 7, 4): S_6_7_4,\n", | |
| " (6, 7, 5): S_6_7_5,\n", | |
| " (6, 7, 6): S_6_7_6,\n", | |
| " (6, 8, 0): S_6_8_0,\n", | |
| " (6, 8, 1): S_6_8_1,\n", | |
| " (6, 8, 2): S_6_8_2,\n", | |
| " (6, 8, 3): S_6_8_3,\n", | |
| " (6, 8, 4): S_6_8_4,\n", | |
| " (6, 8, 5): S_6_8_5,\n", | |
| " (6, 8, 6): S_6_8_6,\n", | |
| " (7, 0, 0): S_7_0_0,\n", | |
| " (7, 0, 1): S_7_0_1,\n", | |
| " (7, 0, 2): S_7_0_2,\n", | |
| " (7, 0, 3): S_7_0_3,\n", | |
| " (7, 0, 4): S_7_0_4,\n", | |
| " (7, 0, 5): S_7_0_5,\n", | |
| " (7, 0, 6): S_7_0_6,\n", | |
| " (7, 1, 0): S_7_1_0,\n", | |
| " (7, 1, 1): S_7_1_1,\n", | |
| " (7, 1, 2): S_7_1_2,\n", | |
| " (7, 1, 3): S_7_1_3,\n", | |
| " (7, 1, 4): S_7_1_4,\n", | |
| " (7, 1, 5): S_7_1_5,\n", | |
| " (7, 1, 6): S_7_1_6,\n", | |
| " (7, 2, 0): S_7_2_0,\n", | |
| " (7, 2, 1): S_7_2_1,\n", | |
| " (7, 2, 2): S_7_2_2,\n", | |
| " (7, 2, 3): S_7_2_3,\n", | |
| " (7, 2, 4): S_7_2_4,\n", | |
| " (7, 2, 5): S_7_2_5,\n", | |
| " (7, 2, 6): S_7_2_6,\n", | |
| " (7, 3, 0): S_7_3_0,\n", | |
| " (7, 3, 1): S_7_3_1,\n", | |
| " (7, 3, 2): S_7_3_2,\n", | |
| " (7, 3, 3): S_7_3_3,\n", | |
| " (7, 3, 4): S_7_3_4,\n", | |
| " (7, 3, 5): S_7_3_5,\n", | |
| " (7, 3, 6): S_7_3_6,\n", | |
| " (7, 4, 0): S_7_4_0,\n", | |
| " (7, 4, 1): S_7_4_1,\n", | |
| " (7, 4, 2): S_7_4_2,\n", | |
| " (7, 4, 3): S_7_4_3,\n", | |
| " (7, 4, 4): S_7_4_4,\n", | |
| " (7, 4, 5): S_7_4_5,\n", | |
| " (7, 4, 6): S_7_4_6,\n", | |
| " (7, 5, 0): S_7_5_0,\n", | |
| " (7, 5, 1): S_7_5_1,\n", | |
| " (7, 5, 2): S_7_5_2,\n", | |
| " (7, 5, 3): S_7_5_3,\n", | |
| " (7, 5, 4): S_7_5_4,\n", | |
| " (7, 5, 5): S_7_5_5,\n", | |
| " (7, 5, 6): S_7_5_6,\n", | |
| " (7, 6, 0): S_7_6_0,\n", | |
| " (7, 6, 1): S_7_6_1,\n", | |
| " (7, 6, 2): S_7_6_2,\n", | |
| " (7, 6, 3): S_7_6_3,\n", | |
| " (7, 6, 4): S_7_6_4,\n", | |
| " (7, 6, 5): S_7_6_5,\n", | |
| " (7, 6, 6): S_7_6_6,\n", | |
| " (7, 7, 0): S_7_7_0,\n", | |
| " (7, 7, 1): S_7_7_1,\n", | |
| " (7, 7, 2): S_7_7_2,\n", | |
| " (7, 7, 3): S_7_7_3,\n", | |
| " (7, 7, 4): S_7_7_4,\n", | |
| " (7, 7, 5): S_7_7_5,\n", | |
| " (7, 7, 6): S_7_7_6,\n", | |
| " (7, 8, 0): S_7_8_0,\n", | |
| " (7, 8, 1): S_7_8_1,\n", | |
| " (7, 8, 2): S_7_8_2,\n", | |
| " (7, 8, 3): S_7_8_3,\n", | |
| " (7, 8, 4): S_7_8_4,\n", | |
| " (7, 8, 5): S_7_8_5,\n", | |
| " (7, 8, 6): S_7_8_6,\n", | |
| " (8, 0, 0): S_8_0_0,\n", | |
| " (8, 0, 1): S_8_0_1,\n", | |
| " (8, 0, 2): S_8_0_2,\n", | |
| " (8, 0, 3): S_8_0_3,\n", | |
| " (8, 0, 4): S_8_0_4,\n", | |
| " (8, 0, 5): S_8_0_5,\n", | |
| " (8, 0, 6): S_8_0_6,\n", | |
| " (8, 1, 0): S_8_1_0,\n", | |
| " (8, 1, 1): S_8_1_1,\n", | |
| " (8, 1, 2): S_8_1_2,\n", | |
| " (8, 1, 3): S_8_1_3,\n", | |
| " (8, 1, 4): S_8_1_4,\n", | |
| " (8, 1, 5): S_8_1_5,\n", | |
| " (8, 1, 6): S_8_1_6,\n", | |
| " (8, 2, 0): S_8_2_0,\n", | |
| " (8, 2, 1): S_8_2_1,\n", | |
| " (8, 2, 2): S_8_2_2,\n", | |
| " (8, 2, 3): S_8_2_3,\n", | |
| " (8, 2, 4): S_8_2_4,\n", | |
| " (8, 2, 5): S_8_2_5,\n", | |
| " (8, 2, 6): S_8_2_6,\n", | |
| " (8, 3, 0): S_8_3_0,\n", | |
| " (8, 3, 1): S_8_3_1,\n", | |
| " (8, 3, 2): S_8_3_2,\n", | |
| " (8, 3, 3): S_8_3_3,\n", | |
| " (8, 3, 4): S_8_3_4,\n", | |
| " (8, 3, 5): S_8_3_5,\n", | |
| " (8, 3, 6): S_8_3_6,\n", | |
| " (8, 4, 0): S_8_4_0,\n", | |
| " (8, 4, 1): S_8_4_1,\n", | |
| " (8, 4, 2): S_8_4_2,\n", | |
| " (8, 4, 3): S_8_4_3,\n", | |
| " (8, 4, 4): S_8_4_4,\n", | |
| " (8, 4, 5): S_8_4_5,\n", | |
| " (8, 4, 6): S_8_4_6,\n", | |
| " (8, 5, 0): S_8_5_0,\n", | |
| " (8, 5, 1): S_8_5_1,\n", | |
| " (8, 5, 2): S_8_5_2,\n", | |
| " (8, 5, 3): S_8_5_3,\n", | |
| " (8, 5, 4): S_8_5_4,\n", | |
| " (8, 5, 5): S_8_5_5,\n", | |
| " (8, 5, 6): S_8_5_6,\n", | |
| " (8, 6, 0): S_8_6_0,\n", | |
| " (8, 6, 1): S_8_6_1,\n", | |
| " (8, 6, 2): S_8_6_2,\n", | |
| " (8, 6, 3): S_8_6_3,\n", | |
| " (8, 6, 4): S_8_6_4,\n", | |
| " (8, 6, 5): S_8_6_5,\n", | |
| " (8, 6, 6): S_8_6_6,\n", | |
| " (8, 7, 0): S_8_7_0,\n", | |
| " (8, 7, 1): S_8_7_1,\n", | |
| " (8, 7, 2): S_8_7_2,\n", | |
| " (8, 7, 3): S_8_7_3,\n", | |
| " (8, 7, 4): S_8_7_4,\n", | |
| " (8, 7, 5): S_8_7_5,\n", | |
| " (8, 7, 6): S_8_7_6,\n", | |
| " (8, 8, 0): S_8_8_0,\n", | |
| " (8, 8, 1): S_8_8_1,\n", | |
| " (8, 8, 2): S_8_8_2,\n", | |
| " (8, 8, 3): S_8_8_3,\n", | |
| " (8, 8, 4): S_8_8_4,\n", | |
| " (8, 8, 5): S_8_8_5,\n", | |
| " (8, 8, 6): S_8_8_6}" | |
| ] | |
| }, | |
| "execution_count": 52, | |
| "metadata": {}, | |
| "output_type": "execute_result" | |
| } | |
| ], | |
| "source": [ | |
| "paths" | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "execution_count": null, | |
| "metadata": {}, | |
| "outputs": [], | |
| "source": [] | |
| } | |
| ], | |
| "metadata": { | |
| "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.10.4" | |
| } | |
| }, | |
| "nbformat": 4, | |
| "nbformat_minor": 4 | |
| } |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment