{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "2c9f3b67",
   "metadata": {
    "tags": [
     "CSP",
     "complex",
     "easy",
     "AllDifferent",
     "Extension"
    ]
   },
   "source": [
    "# Problem *Subgraph Isomorphism*"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "423ae2ef",
   "metadata": {},
   "source": [
    "An instance of the subgraph isomorphism problem is defined by a pattern graph $G_p=(V_p,E_p)$ and a target graph $G_t=(V_t,E_t)$: the  objective is to determine whether $G_p$ is isomorphic to some subgraph(s) in $G_t$. Finding a solution to such a problem instance means then finding a subisomorphism function, that is an injective mapping $f : V_p \\rightarrow V_t$ such that all edges of $G_p$ are preserved: $\\forall (v,v') \\in E_p, (f(v_p),f(v'_p)) \\in E_t$. Here, we refer to the partial, and not the induced subgraph isomorphism problem."
   ]
  },
  {
   "attachments": {
    "subgraph.png": {
     "image/png": "iVBORw0KGgoAAAANSUhEUgAABG0AAAFBCAQAAABnMZqmAAAAAmJLR0QA/4ePzL8AAAAJcEhZcwAAASwAAAEsAHOI6VIAAAAHdElNRQflCxYLDibIJF5RAABJdUlEQVR42u29X4wr237n9alu984BTc65dQTzMtHJSe0ghid2UjviCekSVSsRSAgxcedG0bzAUA7PKLijPEIm9jASQkKT2BPxBMpNeyIipBkSubj3PvAwIl05h4s0/FFc589EGpFA19n7TsTV2b334qHKbtttu13/y/b385P27rbbVauWV/3qu37rt9ayDEIIIYQQ9WM5JAYQExKbsISjStocCpaLvfRrZKKmSySEEEJkx3Lp4mLjbnr3/PO3f0pEYCa5jy9p02Ysmy4uzvlPvv14w9shMSGBCZoupxBCCPE0VhfvvX/7hz82/31V34TAwwPt4gdv/pCAiYkzn0XSpp1YDl1cug+veNhpzG6uaeZ0Xt9/m4Ag+9cvhBBC1IHl43V+7v59AIcu3mIcap2YkJDJw1MuIGCc5QknadM6LBuf7lzGJl//6ljUnIiIgODh658QmHHT5RdC1IW1GtAvJUtBiPKxPPp4AC5dulskzToxEwKSUanzz9/+5v7PN0mblmENzn7l3Qdgp0Ebe4/PREwIH77+/0gDVEIcM2lM104eFWvvfWVui2UpCFEulvvs7379TXDo7/lMWyUmYEwAXHz55j/c7/kmadMiLP/i1998BB7+8kjUnsRMGBIBz7739W9I3ghxfFguXudb9y/mvzs4i7BNRLyapfC7hHmyFIQoD8uhjw82Pv0csuaBcfp8I2D49PNN0qYlWF7nv7h/AS6DTV2xvRkyJAYYM9QcKiGOBcumf/6LyXQCmy4e7pagfrCapTBhrI6OaAbLZwTQLyhr5iyeb0Nz/cSZJW3agDXCT8J1fuFjxQwZE9N5ff+ryrwR4hiYR3QfzS7YSpKHl45KBfTU0RF1Yw3oQ5fBnpk1+xAzZAgQcLUzImlkDRt25xOMbfqmPGammxx80PTVyWSyYkb3/DMMxjPTzJ7gzvSNnRxmhNP0lchOx7CffReDGZX4XJtza2yDee/7uNvPr6hNw1jue3/wwx+zmW5euagAY3rAe3/ww/9Ao+1CHCZWOkJdJKI77+d2Xt//1lNhfCHKwHI7v3P/oornWkLEFSGd1/d/Y9tgq6RNo1jdzu/cv+8yLWUccp2AK2I6n97/DQWjhTg8LO/sH7z7wGZQeKA6YsgYYEJPXR1RLZbX+f37911uShyIWiemlwy39janXZw1XQmnjOVzc/++X5GwAY8pLvcvrNCqRjoLISrD6jN990GXWQkZeA6jxM90O9+RNxBVYrmd379/v8u0QmEDNjf0AUbWxttDUZvGsLrcQJ9BpWdJtK31lXHUVxPicEimFpTrH54O4wtRDMu2IvONdGJU5SRpF7x8vFSlpE1DWG7nO/fvDxLdWTGXBHQ+vf9ZiRshDgHLZopbxkDUOk+F8YUoxsUn9y9cbms7X48xndf3P7WedCFp0wiW/d73f/hjdSnbmJdEMDa9pq9bCPE01hSvuhTM62Ty7JXWKxZlY43wHW4rSrHYzOauu3JtGqHznR/+mFvxUNQDNjfY4Ft1nVAIkRtrhGdzW5GwgSRW3Pkd5dyIcrH6+OnTpkZucLl/sf44VdSmAawRvs2s1gYw4QrUUxOi5STrt1YnbBJ6jLn48s0LDVKLsrA8pjAqfRD1aUIuiddWKJa0qR3LY1pdsHk7Q645e/XuJ+TMhGgrlsttHY+HmEtCCM3Lpq9YHAsXn9y/qHpazDYmXK093TQgVTvnfx/6tQsb6OPx7oNa8paFEDmwHCuglO1WnsJOpoK7Vj3pfuLosfz7F05Dwga6dHn3wfLpFbWpGctn5DBr5NwhLwGeawE/IdqINcL3mNZ0tjSMf6mJ4KI4z75481ETg1FzIp7D0tNNUZtaseyLX6exwImbNDzFbYRoIZaHb9c0axLkD0R5WIM3H7kNChtwkrMv4jaK2tSKNaBfX6/sMamy3bDAkRCiWX7ku19/s95chZjnituIwlj22WfvPpjiNVqK1dasqE2NWPbZrzTbSXKSs2sSuBAtw/K+/qZds3dIznf+95u+dnHg9N994DUsbMBeiUIqalMjZcRsYob0C0wbT5Wt4jZCtIqm5pc8J9LaxKIQ51+VG7MJCYmAiJhBhik3y083RW1qpPNzRQMmAS8ZUkSVpMq223RdCCEeaG5+SR84/7Wmr18cLlb33QduqTGbl/QYMmRCtpHS5aebpE1tWM79Czv3pO+QMZdcUnxyUxe4+KWma0MIsYTX1FC1j8vbj62mRxPE4eKW3Vc2mHQWcdYnpkcSQpC0qZNuvgYQYGHxkmFJa+G4OLz5yKpyv3khRAYsO693KANv8Y8Q2Xnvl6toPknSRdbjetjcv7AcSZsa6XwrXwNwmTJlxqy0cLUHGpISoj14iVNuBsVxRX4s94c/5lSwBG0yFJX9uN30H0mbmrDs+xd2Lj1h4+FRZpBF0kaIVuEV6/eGBAUy8NI4rjbLFHmoKN6YtOfsd8U8BilpUxfd9sR8u8kS6xqSEqIVdL6V9/EQc81zrpjQ4yUhEDDMfJTu4h8hMuJV03QCsmfapMUBz7IlbeqiYL+s9MK0qThCnDCWd/++mysuG/KSIT4zRtzic8WES66ZZDyO/IHIh2Xj5p8cs52YkHxNMh0bcTsN18zpYOcZN6wKZ/GPEKJhcnZ7Aq6Il3YJ9wnpAWTO2vGgTe5JHA5uNQ0nb6YNpA82T1GbuvDa5DtcyO7/hBAVkd03hFwRr+0S7hMDeTMUlG0jMmNX00fOm2kD8/IoalMbbVISNihqI0Q7cLN7h5gr4vnGKQuSWzpfGJ92uShxGORou9sIiRfZNXkzbSC9CzQgVQ9Wq2I2CkAL0SKc7DfjkIh0QsASSRg/j7RJgvgZF38VopREi5ghE8AjBEY4uTNtIG3LtqRNPVQUtitSoFh9NCHagJO15xuls6D8tdfzh/Hb5Z3EwZC57T4m5IqIQRqBHHOVtuu8kklRmzopMWxXVoHUQROiHWQVI8lelo9nVeUP4zsA/66ybURG/lrRqM2mZPhEuOefsucSKtdGCCEOi2Ry97rrzz9hNuVf0ARwkZHPi3XaNyfDj8mfaQNJiTRDSgghDog43SR3XYcUmTArRP2UnQy/jKI2QghxQMy3VNgsbQo8Ev4/jVKLjPy1Ih/elQxfRKLHSNrURUA/aroMawUSQrSDPHeju/Eo8zB+TJwpNTgC+B/MddM1IQ4La8q/FuSU0+Unwy8fQQNS9RCTLqbVDmJIvZkQolnOP8/zqfUMh4iIhwfCME013hc5A5GLKP+Trfxk+IQYIJS0qQUTUmBn3vIJQd5MiFbw9k+zxW0SUbPu+lfD+GHGR0P0cAgh9ifO/2SrKBk+KU8saVMT1leti9q0SWsJcbpk7Pm62Kz3TOI0uD8fjgoy7sYcL/4RIgO5nyLVJcNHoKhNfZjbNnWKpGqEaA2Ze74+q5+IuVwJ648f5S88RUgSWxYiE7mjNpUlw6eSSdKmLqI2CYpE1zZdCiEEEGbt9vRxiRbZNCGX+Nwssm9ihhmlTVhkXEGcMmGxzIankuHzHDsZXNUMqboI8NviO+JklLM9QSQhThgzuXgdvh9lmNFkM+WKHhEQETLCA2644hqPCYOMAX35A5EPE1tR5GTN7HrgqWR4GGQ+5gQ0IFUjAUxaMpg9AZiYdhRGiJPn/ttZlYXNlFtswGeWPgo8ZvjATebhqMniHyEyMsnXdKpIhk+LA6FRGnFdmDhvEyifENRHE6I9ZB6SAnDpM1jJSrDxM0dsICTivT9Tpo3IRc7nWhXJ8JDeRxPl2tRJkFdPBAQEDLlKf79mmL6WL/Ci8LMQrWLSZEw3AH74j5quAnGYmPC9P4ty5cSUnwwPDxFISZv6mOTVE5dccsk1E8DDJuQ6fS1PR2tCTOdTo1VthGgJzcZ01dURRfjhP8rXdstOhk+OEvPe/2YiSZsaMTFhnKsJmCWbcrf0W54pcgHJ2L4QojUEpMH4upkQYr027RgrF4dIkDfbZopHj2uuueKKAT42N9hcc83LHEOrSTmSCKRlmq6WE8LqM3C5bbQMEc8BnitqI0Sb6Hz29uNRrhB8MZ4Twf/OjzA02fZmECLl/Kt3H8wy7Vn2QEhAjLfUTY+ZENHNIWxiXhLBSxNK2tRMU+7rgR5jGJte0zUhhFjG6nJjM3s0HbZaxvTo/Pn9XwUgkrwR2bFs/h7f8pg2XRCuGUJgLkEDUjXz9jebCjsnBIy5+EGjRRBCbMBMnn0vrvnWTM53/0/TXx1G1sxqsuclDgzLtgbM+PnO66DxdK04ydtJbyFJm1ox44svowaVxRB48/c0GCVE+/j6N2Bc6zypIRHPvsfV0jbhkjdiT1JZ08fmG/f/pNlOO8CQGAKTKiwNSNWM5TGtP+ycEHBJ5/X9x1qsT4g2Yt3Q7XJT09lCLonh0gRgOfRXRso1OCV2YNn08ZceY1+9989/+GNNJlusZ5EqalMzJiCoO+w85xq4/y0JGyFayvXZqwnXtZwq5ooYxkkv10Smx3NFb8TTLEVr5oxxf/ifNRu3GQKMl0YkjKxmw8NgRqZufIM5/6zpq5fJZNutPu/gGkznE+y18zuMVl6Y4TddJ7L2GDaDlfVHDCOc5IfzzzCD2p9rCbdJEZylkjZdVado9DG2ua31qx8YTOcVbtPXLpPJdlk93sE3mM6rdWGTlkDyRrbBdskag4EuBnNT63MtYWZsg2GwUtqmq+s0jRHGMXe1ffXT5LRyUDJZ640Rxq7UO4zMUx0dyRvZsj0la9K/GtTfaTfmzrgGw3StLE1X2ala5xOMW9NXf7tB08pksrYatxi3skdE6gielCqSNzLDvrIm/dsRxq2x026MMV2zcWi16Wo7VcO2vsL4NXzxqab9h01fsUwm28+wucXYFQT370yqTvp7lkTy5qQti6xJ/r7zCcar4bk2p282RyAbr7pTNXxenf8A41escG+NazDWXxArz0YmOxTDTiRFuWmZSTen84puprJI3pykZZU16aeczqt6Ou3GJEOrGLwN5Wi6+k7T8DEYfnD+g2rDd1NjG4z1FxgMdxI3MtnhGANMmQ+JZGD64os8fkDy5rQsn6xJP+ti6hE36dDqxghk41V4ipYKG4PhH59/Vl3iVapo/yFxejaJG5nsgAy/8wrjlDAZfDEQdbt5VtRepZG8OQkrImvSI/idV9Xn3KSNb0sOaePVeHq2JGxusbGffRdTxUoWD1887qKhStzIZAdkuMwwGNdMC8iavkn1TOGpBJI3x23FZU16HPfiiypnSy2GVre2vsar8tRsVdikr40wGN/MSvvip2tfvMSNTHaohn/xBQbj5XpQjOay5ibPI2pjeSRvjtLKkjXzo3U+wdiVLD95axzz5PIFTVfnadkmYbP8er+EEN7MJDlV558tf/ESNzLZ4RqDs68wGNf09xQ4d+bG+KmsefbdTYmWhcojeXNUVq6sWRw17bSXOzCVxCAfT/deO3fTVXpKtk3YGB5chW36hWRN4l86rxg8OoPEjUx2sIY9lzcYx/R3TAyfmZFZmgJ1m20+VIYSSd4chVUja9Jj9zHJU60ceTMyacFGT51ZO3/XhuUzSn8Mudy0SaXlPvu7X38THHy6OBmPHzKZb082ZLj5+EzTLc1iLk3YdI0IIbJheXgXv/Tmo/nvHvaSpwiJeNgf8L0/+OE/ZrK0YWAV5dGO4QfNox28YcywzDZjOYzwEv1UbLfVgGtCoPPp/a8mm7rupGnFeCq2K2Kz8ncet8mP+4eeHwLPT+ltRW5kssM3XPpMkwTjDXbLCD//TKjMpVH05iCtymjN2pm8ZLKMY0Y5ozc3aZrFxRf7ti1FbWrh6YjNyl938c5+8d0HAA4eDi7OoyhOSExAxCT9vfPp/R+tbOq++diK3AhxNFguNv8xPw3AbxIRPuVdKiqHojcHRfXRmkdn7J7/nbcfA3Tx6K6cejsxAQETYuDs1bvfNtd7n0/SpnqyCZvFp1y657+YNIYEd9EcQlYOEjLZP/AscSPEMWEN6AMYq+FySN4cBPXLmsWZfTy6yc8uXVy8rX8bEhIsOu6ETBhnke2SNpWTT9gsPu3QxcbFxl17KyAmImKS+ZgSN0IcDW2RNiB503aakzVLJejiXfz8mx9NfrdxcZYKlDzUimeMSdpUTDFhs3YsmzsA/sS4RY4jcSPE8dAmaQOSN22leVmzUpouHo710nxjyx8ExATZO+6L40vaVEmZwgYWX1dgLgsfSeJGiKOgbdIGJG/aRrtkzVrZPOCX+SYA/wf/DXEZGWNnTV/WMVO2sCkTE3KZJuzYTK2CUSAhhHjARKbHcx7EjMPImlnFZv+KXFi2NWBGf0nYjHlueu0QNmACE/Df8TEf8zH/q5mYoIxnpaRNZbRZ2IDEjRCiSiRvmqftsqY6JG0qou3CBiRuhBDVInnTHKcra0DSpiIOQdiAxI0Qomokb+rntGUNSNpUwqEIG5C4EUJUj+RNfUjWgKRNBRySsAGJGyFEHUjeVI9kzRxJm5I5NGEDEjdCiHqQvKkOyZplJG1K5RCFDUjcCCHqQvKmfCRr1pG0KZFDFTYgcSOEqA/Jm/KQrNmEpE1pHLKwAYkbIUSdSN4UR7JmG5I2JXHowgYkboQQ9SJ5kx/Jml1I2pTCMQgbkLgRQtSN5E12JGueQtKmBI5F2IDEjRCifiRv9keyZh8kbQpzTMIGJG6EEE0gefM0kjX7ImlTkGMTNiBxI4RoBsmb7UjWZEHSphDHKGxA4kYI0RSSN4+RrMlKp+kCHDLHKmwATGhdMsUmETeXJmy6REKIU8FE9KwhfeaCxmFk9RmacaHDZsJycPCA1a5dSExIVJ+osGz6+EuiBsYMJWqewMhyGv7ix1vsms6Z/Det6Wwud+mPd7hN17dMJttkDJIfmi5HJdfmMFp5YYZfw1ldBuefPfFHtwyq94rYDBZeOLERTtPfSgXX6aU/DMo6omWa1lYHSjMRm/TrCsxlTedz08gNxChyI0QLsQb0AYzVdEkquj5nKXoDEFUXvbE8uhc//+YjAAcXZ2HJiSNCYiKCdLz+4ss3v8ukGs94StEay2MKwNBcl3TIptXaYVoTERtD3VEbgyI3Mlnb7ZijNotrrCF6g8c0+dExfXNrdjM1fbMIn0zL9o2nEq1Zqvvkh9KiNo1f0iFaU8KmCWkjcSOTtdtOQdoYqpU3OM++i8HYZmBmZn9uTd+kj4DSpMepyRpDFdJGM6Qyc8zJw5vQbCkhRPNUNXPKcqwRs6+/adNnRj8dfNoPl2TiEuAzswaWneHDm8qimVAlIWmTkVMTNiBxI4RoB+XLG8u1QnzoM2NAHmViM2CWJAP1O9/J7x8la8pE0iYTpyhsQOJGCNEWypQ3ls+t+YaXW9YsFYFbXO5fdL5jdXOUQ7KmZCRtMnCqwgYkboQQ7aEceWMNGIHPNNMg1DZcpvjcv8+N1c9UCsmaCpC02ZtTFjYgcSOEaBPF5I1lWzf0YbRw68WxGSV5NwNrz4NK1lSFpM2enLqwAYkbIUS7KCBvbujaTCl7/4YBI2zwnxY3kjVVImmzFxI2CRI3Qoh2kUfeWCM8myleBeXxk3VO/V3DUpI1VSNpswcSNg9I3Agh2kY2eWP5+DClKvflJg+MweaEYsmaOpC0eRIJm1UkboQQ7WNfeWO5jGBUmbAB6NIHOr+z7h8la+pC0uYJJGweI3EjhGgjT8sbyzn7n1jblKoKBvjcv3/+Dx4W8ZOsqRNJm51I2GxG4kYI0U6ekDeDdx94DGooxwCXtx8np5KsqRtJmx1I2GxH4kYI0Va2yRvLo2tzU0sZ0vP41gvJmvqRtNmKhM1uJG6EEO1lk7w5/6/BL7TucBacZNjrtyVr6kfSZgsSNk8jcSOEaDNr8ub/fvuv2mRaKrggfWz4N/hB+qtkTW1I2mxEwmY/JG6EEO3mQd6cnVNwr6ispHGb/xfJmpqRtNmAhM3+SNwIIdqOiUyPX3/3LzmVz4xap48NH/M3JWvqRdLmERI22ZC4EUIcAC+odTAqwU7E1L/Z9MWfGpI2a0jYZEfiRgjRbiybLnSLHygzPnD2i01f/6khabOChE0+JG6EEK2mC91a82zmOLi8+0BesV4kbZaQsMmPxI0QosW4FN5aISAgIPuDwYNmAkYnjKTNgvYLm4Vg+NBymi7LYyRuhBBtpfOtIuoi4AqLayYMec51xk93gXMNSdVKp+kCtIW2ChvLpYuNc/Yz7z5YvPjTzCzOP3/7p4TETNqSeW9C65IpNom4uTRh0yUSQgiwPN53ydcjjOgR0GWWfj7mkutMWzW4OEQfW05bPPUpIGkDtFPYWF28zrd4P/ntHfZSODUm5O3HfIwHDC4+vf8jJm0QEhI3QogW4qXDQpmZ0COmvyRlbPpcrSwwvM/px+AiaVMbkja0T9hYPl4SO73HxcNj020ZExIRMiF+wQv6z75884dMTNBs2SVuhBBtJE/MZsIV4K/FaGwgypS5YwO4TJqug9NB0qZlwsbyz3+NjwFcunR33I52KndGhEyYEH2Ej28FXDcrJyRuhBAtw80jbSJ6gP1o8ClciaHveXoamZ51spx8GnGbhI3l/ch3Gb392GHEHbf097wZXQbM5lvLetxao2bTjJVQLIRoFXae+VE9Yh5vpxkyzLymsQ35wkYiJycubdojbCzHmjL9+psOI2a59qZ1GDBLVtv0mVkDq8E+gsSNEKJFuNmDJiHJ6P6yjIm55pJupiTi9PSSNrVy0tKmRcJmwAzPps9toT1ObAbMkiP0rcjKlzdXChI3QohDJkmMsRlzzTXXXPGS50TcLB4b+6OoTd2csLRpi7CxbGtEH/rMStmV1mHELR7mG0ytuveCW0LiRghxuCQxm7njcvAZccdNzplWol5ONo24PcKm8537FzajUherdJlyzRBGlmt6TV2bEoqFEIdK4q58LSN8kJxo1KY1wsbtfH7/wmFawe0zSC7R/5HvNpd1o8iNEOKQKdFpNb6syClxktKmNcLG5/b+fY/bMm+fJXxusfn6m+d/0pyokLgRQjRO7sXyykmQCWAeBhK1cILSpjXCxmUEfjpiUw0uM1zeftz5HUVuhBAnSzTPnWm2DKIuTk7atEbYOJ3vQD9Hrn02bKa43L/gpqkrlbgRQjRMlH08aFe6cMBVpmMFoAGpWjkxadMaYWN3fv/+fS/z6gh5sLnBBs+qWkXtQOJGCNEgcfbxIG/+wUeE9JIVxLKhqE2NnJS0aYuwAUb3L9zaAikOUwBfU8GFECdJmF1Z+DiwYdunIZfcZMyPVK5N3ZyQtGmPsLEGdG1GNW4p4iaXPmpSUkjcCCEaIoBJxhGhJN59vaJIJlwSZJ74ERFy9kqLX9TJyUibFgkbjz6ZVX9RfPqAFWj7BSHEqWFiJmTeeNtlisvlYjXiD5nQZ5p51tQEePd7TdfBaXEi0qY9wgae/Tr0G1jRcpCsUJxjiLg8JG6EEI0Q5BkRcpmmUsbGz70W8SQ9v6gPyzRdgjouskXCxvIZ2cwa2d8+4JKLH7z58YZrwF3Md4/RCsVCFMQaJB0WYzVdkjZjOcxs7ho4c8yH6NvZjeUlCaEMzXU5RzyBqE2bhA1c/Dql7BSVBw+PNz/abNxGkRshRP2YiDDOPCRVBpPFP6I+jl7atEvYWP6bj5xCe3sXYwTQtxregVbiRghROxMYN3DaIWg4qnaOXNq0TNjYZ3+HWtay2UYqqxqO20jcCCHqxLKtAdfWXwa1a4wxEWf/D/0ml944RY5a2rRL2AD+uw+8UjbCDPkw5y3axwa/eTEhcSOEqAPLtgbM6PMN8xdQUirHnsQMgXcGh5E1k7ypjyOWNq0TNtClpMGoXu41u9O4TfkbjWdG4kYIUS0LWZOkN37c+fOw1kGpIRHn/yf/MoDkTZ0crbRpn7CxHFy7FE1xXWhZSw/o/FzTtQESN0KI6liTNQDj+/8qzX2phZgx8PY/X1JTkjc1caTSpn3CBuiWEyyJCt6aHjb3L5pOJU6QuBFClM8mWcNz0zN/u/NpVNug1DUxBOa/NT2eS97Uy1FKm1YKG3ApZaG+Xua1MNfpLv5pHokbIUSZbJU1EcD9r8KwlkGpIWM6r+kBmEjypl6OUNq0U9hYNt0ypM2Q4qrEW/zTBiRuhBDlsFvWAJiAHvQq36tywjVw/7eWzix5UyNHJ23aKWxIh6OKLtUXMV5cXn4SadPkblKrSNwIIYrytKxJMGPGLFxONYRJsGZo1pbqk7ypiyOTNq0VNiUNR/XwCw9HQZrM3Jq4jcSNEKII+8qaBNN79r24QnETc0UM482bBkje1MFRSZsWCxtwKCxKhpS12p4D1Lz1+BNI3Agh8pBN1iR8/e+ffx5WJG5CLokg3JWtLHlTNUckbVotbDj7maJhknIGoxJcoKGNrLYicSOEyEYeWQNg4re/cP55yPPSc24CLgnpfPr0M0jypkqORtq0W9jAuw+KKolruiUMRiXYUDyIVDoSN0KIfckraxJM+PanO5/GXJY6W2qYuLDJ/c/u9wySvKmKI5E2bRc2lld0/GdCVOLuUx60UNpI3Agh9qGYrEkw8ZufYhzTK2mdm8WRhuYqyzNI8qYKjkLatF3YJBSJ2sT0ShuMWtBCaSNxI4TYTRmyZo7p0YPhirLIx5iX6To2JodSkrwpmyOQNgchbLxiSqKHX3LWb4umR60hcSOE2EyZsibBjLk8/zyix2XuXcEnPKdHBMH9z5rcGknypkwOXtochLApSLmDUe1H4kYIsU75sibBBPc/Qe/iy4BLLjOnFU+45IqIiy/pmUtTMCtZ8qYsDlzanIKwqWQwquVI3AghHqhK1swx4zcvGJ69CnjJh/SYPPmJmAk9PuSKgLNX9L7+8fzxmrWySN6UwEFLm1MQNnBd+mDUISBxI4SA6mVNgonN9bufYNj5NGbMFR9yxZDgURQnJOA6fX9MDCHX736iLFmzKI3kTVHMwRr+4sdb7KZL80RZPYxv8jA1zqPX+gaDmeY63hwMpulaebLWXO7SH+9wmy6NTNZOY5D80HQ5Krk2m8HCCyQ2wqn4nA59bpdfcoxnPOOZtcfMDf0ayjJaeWGG3/R3Usl1eukPg7KO2GlaWuXl8CI2eboYlQ5GldrnqQITWpdMsUkiN4XHsYUQh4Nl08dfmVo6ZlhurGYTJmLI0LLp4uBg40ULZ3n26t0fExMRManjqWMietaQPvN4jcPI6jMsO0p0fByotDk0YWMCK9eql0O6lcxlCuAApI3EjRCnSVOy5gETl7qWX5GSSN7k4CBzbQ5N2ACcvcpTzJAh1iMbAnCZ/pZnuakYDkLaKOdGiFOjntyaw0K5N1k5wKjNIQobePfHeGHmdODBxu3brgmBQXq0POvlhEBl296WjCI3QpwKzUdr2ouiN1k4OGlzmMIGklT6rNJm89/b6Xv5h6oioPR94SpD4kaI40ey5mkkb/blwAakDlbYQEDutS7LZ5KW6FDQsJQQx4wGofZHg1P7cFDS5oCFDUxg0pIxoETYHFb9SdwIcZxI1mRH8uYpDkjaHK6wsRyrz7TzaVmBkjithLwEAD9q3Vi+VWTPzpqRuBHi2JCsyY/kzS4ORtocprCxHKtv3TJjgHt/VlTahARM0iRiGDMkIMgx0WkC8NfpMuLukASOxI0Qx4NkTXEkb7bS9CqEe65VeEArD6clfrSiJQZjF1pB2FscZ3kJzH7Go9wazNlnayW7wT+QetUKxTLZih3iasRNrDJ8zHboqxaXvxpx45e0VyEPSthsFjUYbvg+5qaQuCmDvsHwu1tKeAACR+JGJlu2Q5M2kjUV1esBy5uTlDaHI2x2iBof20Af4zUsbO6SfVDcp0vbXpO4kcke7JCkjWRNxfV7oPLmBKXNYQib/WQC9tlXRbe1LIpvMNxkLXnbTOJGJpvboUgbyZqa6vkA5c3JSZv2C5ts0oA+G3byro9ZUgyn2FW0wSRuZLLEDkHaSNbUXN8HJm9OTNq0W9jkkwMXX2BGjUmbrsEwKveKGqt/iRuZjPZLG8mahur9gOTNSUmb9gqbIhIAH+OYu0aEzdRgLl4/WcKDETgSNzJZu6WNZE3D9X8g8uaEpE07hU0Zj/3OJ9knbJeDl6HpHIbAkbiRydoqbSRr2mGHIG9ORtq0T9iU96hPvsT6k4n7BmPFGcvaeoEjcSM7dWujtJGsaZe1Xd60Wtrg4CVW+EitEjblP94ZYGwzq1XYpAk2ub6bdgucMsUN9rwNN39dMtl+1jZpI1nTTmuzvClf2lim0FrGlksXcM9/8u3Hy693Xt//L8REREyyborQni0VLIcuXR4v6D8hyH5dK0e+oesypa4dDtIdCnpmnP8Y1dVGUayHqoy5NBk317Icuti4gPeo2mJCYiZa+l20C8vBwcXGwV6024iIKGmzppzt6rKXy6aPv+LYxgx1/7QFy6HP8jYMEcMiT4XSyuUxBWBorks6ZG6V1WV09tXyS97C1jq8N/T31+ztiNhUHafAfu/7mG5NEZt0mb5R8XK3NYKTL3KDy6DzyfJLzqINrzbYzicMNNwla4PhbrkDV+zsK0Z135GK1hyGtTF604qojeXjdX7u/n0AFw8XG/dR/CEkJiBKtmIEOp/ef/vp3m/zEZu6YhOW2/nO/ft9BpVfUcwlIZ1P3/zU4dVShhJlitxYHt7FL735CMCmi4OLg7P2VxERIRGTdE/Oiy/f/CGTpvrD4tSxXLoPrdZdeN75bRgvwowhixtgQkBQfdRE0ZrDom3Rm8ajNvjnnyU/umawV7bInRkZ/yGOM9jVj2g2YlN3PCLRqVXPlbozrsGcf1bJFbQqgrNv5AaXafKjY/p7pnPfmv5DHGdaPJtMJstmD57XMf09dqKbmVGyilVilUZPFK05TGtT9KbRNGK8iy8wGNeMcqzLcpMs8W8uXm+TN80Jm6Ye0ckVdytc5ebWOAZjxVUOprRH4DwtbuY3s2365jZHbfbnIl2uW1ab4T37LiYRNdlabdKxTA8zqKR7I1lz0NasvMHGo8+AG/5nPuMzPiNkyoABXtFWtO+feUlP1ym0ku4sWVnFnH31uPqaETZNP5bxOq8wbo7H7D6MjG0wnU9quZJWCJxd4gZ7PpOkX0BM3i3LG82iklVsOInntQt43lkqbzqvyusTGyRrjsWakDdbnxdLVizDcb8/GmAwthmU8LidpvKG2+WboH5h045HsQGn8wnGrmCdm35yglKShw+nVreJG7pJ0rtfwqT7+aNik0SXycqzuectIsYTblO/e/5ZOcOpkjXHZfXJG5yHyRu28UzfDMx00bmfmakZmb7pLpJYLr5glKfNPv0HdtJrKH5zPXBjHIM5+2r+6KlX2DT/+H1Uwzdl1/BsPs7er/96mq7hTeKGPgbjlbiW0KKGS+0Hy2Rzw07uofL8wtSkt0PBh5ZkzXFa9fLm4Qy28Z/MGCuW4fjU2+5738fYpQ+Y3M1jN36dwqZtomapZCXGxZZiCt1Gr6mx2l4VN9jJ7VR+wnaqajQwJSvdcC++qMLzFo3lStYct1Unbx4SAvxMrXqWM8Nx95vdJBOkmnVz05vs9xenq1DYtFfULEpYSjZT+zJBmqn5JXETJwN+T88pycPNPJtJzl1WouEnnreKCQb5M/Aka07DqpA3DIokBOR5ru16y0+KUt38nbTr8E8xVCZs2i9qlspaaA7akrq9aZvDqf9bmIsb6y8xTkVp2sYYc2tcU/UcNNlpWdK79Stss7bBnH+Wpc1K1pyWlSlv5kktXiE/PB+N2Lfdbn/Dx1S/6kpykzGrQtgckqhZrvf5+hVdM9pT4d6avll82y1edaXebwSX2PrLqvq+DySDq1YsRy8rwxJhU8bQ9K42mwryvdqsZM1pWjnyBre8iTIz4xpM59U+qRbbi/Oq6tsrIRU3/2XJX8kBipql8vtJYjEmWRpxukXtTs3NUqLV2Vf5Mslrv7qavh3szvcxbg1t2BjP1DXJXnbcRhdDoUHp/bjbs81K1py2FZU3ZSe13M3XaXpygszmF+3OqyoDoqtMk5OWkqx06KJm+TvAZ9R59fCSs7RL1+o+XRdfMDgEUVPvN8UI41QcsXm44VyDee+/b7pWZYdt9XUp522Wmx2lkayRUUTeVJPUsl8q/KaX7M4ndfV2E0YGc/G6WLbC8YiatevqMuBmvjXAsp19xZQR/UPO8qjuW2NQxfyS7aTRR00Fl+U27Isv6utS7m6zkjWyZcsjb6pLarnZY8PnTS/V2Nud4xuMFed7mB2rqHl0nTbewg5YztTxDSZh/WpmRW2jzOij7BSN2+ozw/Zps5I1sk2WTd7gYqobWk1l+a7zP3rBr7e3O8c1GKaZq/okRM1pWHnfJvbZV3WF9ZcZGMzZV3oIyPJYEmest0uZtNnOq4c2K1kj22X7yhucqpNa0pDN1kSM9V/t88/qSGJ7zF2iwvbMGJGoOVYr45tlhOk20IZNskJxrVtbyI7DcDA00KVM2+yNQbJGtp89LW+SpBav4pbbN5jOq20jGOu/Dqov0DYGBnP+2R7VKlFz9FbkW04eEtUsM/kUs6QIehzIMhqjOrNslkk7lf+eZI1sf9stbxjVM7TaNdtn+a3+Yl+8poKNGvfFMewYPZOoOTXL941z09RDwpikJ/Hsu03XnOywDA9jNyTHkzZ78ccrBZKskT1p2+RN0prriECms/w2J8Kv/NJgzMaYdKbUFxurUKLmZC3bt5/cVnVnLCzfbFkGVmUyg+HZd6tfHvXJNhumhZGske1tm+RN55P6WvPUYDqvNqmA1UKaZkZ7H1jXYBI1smwtgWmTDwlj0lUXMibEy07ZmpbjaQL8P0OyRpbD1uTNP8E4NbbdbfmNlmGONcL3GZGPkAmQzFB2cx4DAi45e/X2G2A5dOluONSEgImJc59CHDBPtQrLY2ozw855/JCApGl5eDmPEfOSCHpm3HRticPAmuEM6DdahudE8OvmbzddF+IwsRz6+ACdP7//q6Pkx1qIeA7w3ERrJXqQNudfvftghpPj4AE9IjwgIgIc/Nw36ktCGONK1Iht7BA4/yL/Tp9BrqNOuAY8bBKJY+PTzyWSxvRgbHpN15M4BCyXW4dZjk/GhAQAhDi5O6UJY3oQmMuma0McLpZDn3+LfyVfa85Pj/Emf7sIKnXzrkDcN5j+Ipw6TTdqzJsfPTAYPlmLLWn4SfbINg1Rnf0g79yovnFWlvhLIpz59gyfGUznVdP1IzsMY5B3CHU5e7LoYgd3yXHkZWWFzIrrn4g0S3LF1oZSzxYaxyVXCH7MmFsGi96txxQXCLkkT4ClC5z/5OLXCT0+NFdmrGiNWMVEZmhe8pxrwvSlP3v3V9xccccJAbd0l15J4o4RVzlasYPL/ftWN/MHxQnS+bl8nhf6GEwa+s+fBJBgJ61fbVYUwHLNN9zcQ/l5cTa23YW0ee+X87TrmGv6a7eVzQ0AIcNcxXR5+1f4ZxI1Yh9WBM6f5X1IXBPyktXkmORuiMiTMtOF4k8bcQJYzv0Lu9DDIOlUFn+ceOUcRpwy3WaakAd0vrX6Wpprk3e895rJxk9dMQHyJXReM4ShuW6ghsRB8+yLNx/d5lAUMR+mP5mV1y0giUNmJeQlF19+/eNN14hoO1afQf7JG5BkJ9rcFS5JzIdc/ODr95uuEXG45PXAy4TEgJtROXxIvJZKPI/adPPFIkMiLB7nniXKLU6T3LLRBc5/sVDtiBPEct985LQkVOLi8OYjqx2FEW0mZyLAnJiQcgKENi5vflTDqCIvRT1wRI8P6TFhzEsuF3kG+/A45jiXNjlvsCD9dz1oP893yFK4OS4Obz/WY0FkxMv7kLDTfIXVWX3zDkCe3B2UuSD2o2AIP/HA5TjLLmhISuTHy+/yYq55TsgNt4y4YYbPFdHen98ubXI+FvK5/adwgdxLk4hTxc7vl0fcMlubND6X5fkeGx5UdXuIo8Hy5ssN5CVppeXoERfUZkV+vLzeMuaSIT7TRUsOmRBnyHN83JVcpBHna9FJP9ctuXvqpNUkRAbcInr48cyqpD/sFFl8SvJc7MYuqiWSVlqOs/QA62XTVSIOFetlvqhNzCUhLqMlh3nFhDhD1CZJxbeWbqYzSPoO+W4wnxlTbh/58GI9XnUcRHbOf7LMSUlxurp23gRPDzj7mabrRLScQnJ8nmlTZi/QfKPZChGHi/lGvrZ8Rciqpw1TUZO5Za9LmyJ9B2fj6cP0sPluOgc0dVZk5O3HZYZJromxGRV4bNi8+6DpOhHtp4ijW860iQhyTdtYxgOU5SjyYOUcjromAPyVz7r0sec7N+yJu/gn4Wz+apmx8yjt8fo5j+qAgvkiE5ZTXu814IoxHtNCO6G4JLe7EFsp6HnnmTYBl1wx4ZoPc60mNsde/CNEdrI3nXk+zbqnHXCXccOc9bbbmf9QplQfpkfMt5fPPGpjZV9ORJwuHxY/RLo6AgBdBhoYFTVQPGoTMVzEF3tcExfzvP+JBLnIwb+eZ+xnSEyyUG9R1qM2C2lTnlQPGfOwJnEBdIOJmkkWPosIGPIcj4HGRUXF5Pe8SaaNzXgp23HAmGGBfeuBv87PN10n4gD5PM+HEnFexSoZZ8UPsUpMD7CZqs8rDhQHn1tcAi5zbbMgRB0kjwWb6ZI8snFArVYcBHE6pFpFB3IRtSlro6ZrQux0i8yCFM2JE6fEh/x0mYezGXBJTG++caAQLSN5LAzW4j7OItdRiHYzn0ldxQDNQtqEpTjwMeMShE0MEJnLQgcRJ4XlclvuET1cQqBXcFE1IXYR5vaWm4P5SSc1yh81/0+NlJHIjJV7KzS7FP8awcr2B2cPrxZnTA+XWeGITVhimcRpYMLyw3zzndDyhfdDwCjyKHYR54+Xb1vTJvHu+dxnmJZJiMxE+TZWKms4ar3FL6RNvkItE9LDXRn3LVTI4gUSJ8XFl1UdOZ8+0RNCPEmUX5Bv3j2q2GKp8rwiN2F2n7d7ICrgKsOx4rQMc87mhSoaJAm5xF9blzjKeVQFbER23vxfeR8TYz7kQ64fvf6wn0l2QlC2mHiKAq5u8+5R88VS83UwI8BIk4scmDiPp+yy7VMhvbUNi3cTwYq2OpsXqpiciLik+2iobZwzlL+uv4TYgyhfpCSiR0zM8FGTK+Lj46IHEKdAgXj5LmmTLy1TclwUIkeIpA/EGxrdkEtuMsUe1xMA5pO/gyJaIuZqg7CBMOctFoBCNyIruXoNyw1tvckVCe6rDYs9iPI3koBNEibJAM7nd9f7vUJkIiTz3DyXEcm2Ng9MuCTgNqOwWXf/Z4t3ck8YjLlMC7hOkCtLPyLi4kujqI3IxiRfG563UXvrrZTnQREs/hFiGyY6/zwq0Kl8nGkTQ+7lCoLkEELkI8jjgX1uiHnONddcc8WHTOhnXhdvkp7/gc7inX5eP3wNdDd48YB8m25OgDd/mLMw4mQx4bMvo4+yT3p1cIjx6T76ZHKb2jl2kooI6bx+I2kjnuDt79GflLZk2Xw/nnyZNpPFP0Jkx0ye/SD80Thz6+vSJSQgxsbPuYvB47abShsTXrwO38+zFkKPMbB5CZp8N+xj/SXEPrz5Q/xJptSzhBGXG3YxGadDBaMcD4oJcP/tputDHAC5O5X2o7GjmAn59+6bENP59I0GUUVu3vwh3UmuTYXdQvI+Gen5euOAFPffziPYr3cmCueJ2cSEPPvnWjRK5CBXQBQ8Rum2gg+E6YypUa7gvoajxH6YsPM6zJVv83iYdEiMnXfdNEIkx0VBgmbc3qaRnoc9pHIVarjz3bzDUV//j/VXjjh8zCTvY8JnyoTn9BgTEHDNJTEO01w9kCTjX/Jc7EO+TiX4rKYgjxkWWgle0XJRmAlMGpg9MYZHbXchbcwEgszp8Wan5QmMqr8r8nP/7byNx2PGCJsJV1wR0uWGWc6ZJspZEBnIHWvsMlm09jG9QsImJOL8c03eEEUwMeOnAh7lM07a7tpNZJmHH2/o9nOO05ZFyEuAD7VslMiD5TNymDVciudE0DPaflnsxflX7z6Y5pDRMUPG+EBIiE+/wErwPcYwNNe5DyAEYDnMYJZ/B7PMxLzc6G/Pln4ewrDhpTiuAYYSNiIfZnz+eVR7r2GVtA8hYSP25N1v5+vp2gzS9d99Zo92AM9CwJjO65wrrAqxwEQMoVfjGYdEPPveY3+7FLUBa4Sfe/vOEgi4pPP6/mNJG5EXy2NqM2tsr+5tfQghtmHZZ5/li9uUxSWBYjaiFCy78/n9+3W15pjnxHD5eCPis5XfhjBucM2ma+D+tyRsRH5M8Ox7cYNxm219CCG2YeJ3v1lvT3eVgICLHzQc7BRHgonvf6u+fJshMQRmQ4LlStQGrAF9j2kjVTKmx8WXX/94IycXR0MSt7mtcbT3ge19CCF28eyLNx+Ncs3HK85zIrg2kjaiFCzbisw36hj/GScdgpeb0t/P1n4fnr0KGpmglPS03/xGA6cWR4UJGDcVt9nehxBiF29+I209tZPmhknYiJIwsfE6r/Nujr0/YSJsepvn9a1JGxO/+224auAWuyaCSIF8UQLD/LvOF2GSCKrmRhbEwWLGBBH1J7skS1O+/c2mr18cEya8/1XoVRokiZM9EMbbNMN61AZzTRBzWbO4GSYZ+le1nlQcKSaiB9c1Z42lfYhro6XqRR6uO6/HNYubOOnGjtWlFOVixgzhqjIfnGiUZ98zWzuSa7k2AJZ9/idvP65zptQk0TRXWr9VlIU1wq9zplQ6M2psFLMRObG63ECdGTeXBHQ+vf9ZTd0Q5WPd0HUZlbb56wMxVwScf/72p7e33LPHL5n47S/U2X9Ie7tDCRtRHqbX+bTO6OMlEZ1PGxhREEeDmXBdZ7SxR0DntYSNqIgeYchl6Quzh1wSYH319hd2tdyzTS+a8P5vJYNE1bMIieqhIErl/mfPPw9r0ho9Qs5e6SEhimGGjOOach2TbDS1WVEVJuYyac9l5qgHXBLS+dS4T2wLsm3/J/oYzMhUy8y4BtP5BNsgk5VruJ1XGL/iNmyMbzCdV7hNX6/sGIxbjGtmFbfZUXIyv+mrlR27McCU54UHyUFvnlYMu94aYTD9Cm+vqbGNhI2sOqPbeYVxzV1lbfguEeev9JCQlWPYnU8wtplW6HnTxjpo+lplp2D4nVcYx9wU1gtecsC92u0TRcJguhU9GNJ+wx76SybLa7jnn2Fsc1tJG741jlHERlauYXODqSpmLjEuq9sSL4zxcgv2WSrHz77at90+9baX9HrLD4+q3yCrx+a94PIfFDeKOsoqsnLD+A9IjMuaMfyzrzAYL7OauDN9g8FcvGawv699+g/c8h8Mt/PAkvoNslpsPrhaXvxxfrsxkrCRVWFJzNwrNd44khiXNWbYDBJ545r+Xu16ZgZmocFHOJnOtleBbjAYp5TR33lgyYrVb5DVZ0lavF2SvOmb9NnQb/q6ZMdruFaMwfilRM1vTPpkkBiXNWYP8gbjGN/cbJQ4MzM1fbMkEG6yyRrDXtLGYMAvOlZmzFJP12QJLMlkZRgOUwzGKRiBHM0fEVOJc1m1hp0MTBWNOM4TMM8/o9v0NclkuAwuvnh4wTHewpadaucVo7wtNsuf9i9eYzB+rhDp7KGnmzGwJJOVZXjPvotJ5E32R8WduUlvvPe+j9f0tchOw3CS4VTb9HNFb+ayRonDsnYZLn1ukg7nmt0yZVCs67hho4XtWDb9s1959wHYdPHo7vWpkAnBfIXNgGtT79Y+Qqxg+ee/9vZjgC4eHs4en4kICNJVNc8/f/ub2nNH1InlMsADcOni7bl0/YSACTFw9urdbzPU4nyirVje4sewnHaaSdoAWA5+5+fuXyS/dfFw8Db+ZUhEyIRkt8CzV+9+j4mpcitQIfbE8h+UuUsXF2ejxInSNrxQ4xNCU+bSmkLsieXRPfvFdx8AOHTxsDdKnJiQaCHEofPp/bcZS9aI0yKztEk/5tDtfGsucAA87PThEBMR8bD98cWXb36XQKJGtAvLpovb+db9+/NX3KWHRUi8tJdP5/X9HxEw0QNCNIvVxb34pTcfzX93cHDSTWAjYlbcbEDARDvRi1Mkp7RJP2wnHd7zn0wC/GsExERMNAAl2ozVxV1RNcskCifU1q2iTVguXRzsTQHz88/f/mkSbJQQF6dLIWmzciA37ToAoBiNODysVXkTqb8r2s5am43VkRQCSpQ2QgghhBDNc9Z0AYQQQgghykPSRgghhBBHhKSNEEIIIY4ISRshhBBCHBGSNkIIIYQ4IiRthBBCCHFESNoIIYQQ4oiQtBFCCCHEESFpI4QQQogjQtJGCCGEEEeEpI0QQgghjghJGyGEEEIcEZI2QgghhDgiJG2EEEIIcURI2gghhBDiiJC0EUIIIcQRIWkjhBBCiCNC0kYIIYQQR4SkjRBCCCGOCEkbIYQQQhwRkjZCCCGEOCIkbYQQQghxREjaCCGEEOKIkLQRQgghxBEhaSOEEEKII0LSRgghhBBHRCuljWVX+/dCCCGeIo9nlTcWbaB10sayrRGjjB8aWVk/IYQQYiu5PDHIG4tWYJmmS7BaHJspcGni6j8lsmA5OHgABIQPNW3ZeGbSdOmEEGWS36fKGxdFvrYM2iZtbnB5mfN2Ck0v02d8ulvfjImICEzUdI00j2Xj08UFAgBsXMYMk7qxpmAuGyvbABdwscFYTdeUEMfCqidO7zMPCJ6+2/N4Y7D6ZBnKisy46ToqH/na8ug0XYBlrAHdPMIGTGz1uLVic53hQxEh4KQCJ2b1VvFwwQoYmqDpemkSq08fm4gek4Wjc+hza12bsdXHo8n6iUhvNiFEWTzyxBHs6AiukcsbwyD9PyZMf7Jx059C5mWZ3+0BRydt5GtLxbTG8DAMCnx+gMHL8bkpBsPo0esON5hiZTpsw05roL/hPZc7BtxhmDZezhkG03QpZLLjsM2eGBvD3nd7dm+MwXCDs/La7eNz4jLFMGu6lkquc/naskvadAFWKu0Ou1DjuMvT4FNpM9jx3ihXebxdDXH3u20w7NSxdLe873KHoQ232xRzGLebTNZ+2+aJMewvbTJ6YxwMN49enW4+J7ftvN/zenX52vKtNTOkrD4O4yKpZyZmjGMN8h9hA8l4sW95OT7rFni3DdzgAr1tiWsmJONouhCi7RT3xJDDGzvAcO+/butgVF6vLl9bOq2RNvhkadqbGabHKQ0TES1KlxWnwLuNYw3SpMEdTsRMGh37FUKUTxmeGLJ749iEe//tBKw2dg5zeXX52ipoibSx/JJ6ChNsq1Rxk0qbvVPolugWeLdhLIc+8LSLa2vvSQiRg3I8MWT2xg77CxtMTNTKhNYcXl2+thpaIm3wIEvT3kqQHqtxLH/Xrbf73RaQ3GzRU7PDzAStXiHE8VCWJ4Zs3jiTtGHe5WwVOb26fG0ltELaWDZdoIzFiAKgW8FS3xkbleUyyPtu81h2Gkje5xspyw0KIRqmRE8M1XljgLht2Yr5vLp8bVW0Y10bD5ZXXVzH8pJVZoCIYNd6jCayIhy80m7Oea9j5Xi7y2PZdBlgA/ZS+nF6fbvfXTqKj5uO3AZMHpYOtFxsHBwgMEFalsUCVpaLna4GMX+luyjpZO8w8zysus+tFK66mN3l27MGH44RmTFYDt20PzR5ajw+1/UKIeBJTzzHchergU22L2uaxRtnXAMHc7Uoy76+ZIc/WvIboZmAZdOni0PE1bLH2eqV9/TqG8jta5v2tK33tU1P0TKkayDcbHnPZsoUHw+bLlMMt7g7jnVDxpVodk7+9jGY5amQT5UHb8tpvKffXTrGjDsGuDj4zDD4a6VNS8yIKX1m8/IvvTs14DJjhE+XGwx3u+rt0fdhMPv8PfbaShQ7y7ffN7p8FdiMuGPAgAEzDNPHpZpPSMx7vTKZzLDbE88nf+MwZcYAD58pG+/IxScye+O1z2+Z/L14P4sv2eKPDHSZYRgxYMAdd/SZMcChv1wb273yfl59R40bcvjaJjztIfnaxguwqK7B1vdmy02E0e6KZEDG2f/bpU26msDK2fYtT9Jcdlb7lnfxV4+IvSpuDPSTEjNg9HBjLd5Nfp/iMls6StIA91o3aN7gc3+fu8u3Vw3SxWASZ7L2tyt1sVTe3Ncrk8kMuz1x6rVm3C0vK0eXO+7W78jFu5m98Yby7PKj+/mS3f5oxd9iczevA7oPtfG0V8627s/aFeb0tXV72kPytY0XwGDgblMlGgy46Q8LtZo2ve2NvY/hLkfjWruhcebrP64Im73LgyGXtEmb5+ot08Vwt6LYDYYRt2lJ7zDJz0tXNF2LJiUNuL+tRBtqpMDCTNvLl7EGH5U4XbOzu6G8ua9XJpMZdnliw+KOXO9YJJHtjRGK7N547fM7pU1GX7LZHzkPUmapzGYtFr2/V65V2tTtaQ/J1zZegEUhNt8a81DfckWOVr+wTZ/I0bhmTBeWrAx5x816qfYvD4Z80mbGBmfw6PZL/psHRB36y5p5k1hLS75XcLgkabOxfBlr8PbRkZ30uynxemUymWGXJ168e7vh9VsMs43rF2f2xmuf3y1tsvmSzf6ov37NmzxHBq/chLSpzdMekq9twQwpa8cyRyZgCAxXUpqShCUn7zG3EDNc2DWXfGg+NFfrE/LylmfvuujisClbfvM0yvTvTGSGG9K4Vo8SllfKvdlQvow1+OiqTMQYsDcsBtb89QpxwOzlNTeli04AZ/vyfDm88V5k9sab/KW34aiwsq5wRq/cBPV62oPwtW2YIbWzSsw1GXPn02NmXfcg3m+H75zl2ZfkRnnsPpJdV1d5Iv9+NcPdxBaw57oLi11nN81+sJyN39jj0mwpX+EaTK6ru77EVYHrFULkfzhtuSOXjlvRKjSZfMlmf/TotQ2T1bN45ayU4Wtr9rSH4WvbIG32wuri4iymqjVOReVJjvV475VNN1B10+3CdEriZpfk4W8oz+WjhcCfKF/uGoy21ogQon6SO73BO3IvX7LZHyW+bvmxnE4CX3oli1fOShm+Vp52Ay0YkHoKy7FG1h03OAQMzfNS9jdpa3m29Q9ChjVukDYPN25s1GZsXhrLWDxPm37Eh8baL+aVUKwG52eqKswthMjCvA/fxB1Z2BuPiVkdVvKAeGVbgyq9cqW+9pQ9bRuiNjs1p+UzwCagZ7IENSuLaOQsz75EyahuFqFQPiayAjye0OvpglwQZVuuqWgNLgLG7VskSohDpugdFWd8vTDFvbGJrUtu8a10OTvLxQeuV45XoVeu0teetqdtQdRm16qHls8Im4m5zPblZNhDNhN5y2O51mCvd5OjNp+alvRZuuXr9bw1uETqBFq4/qUQB0xerzlff3fbHdk2b7xGl4CAG2tqDawbbgl5ubZWcS6vvNvnL1GRrz11T9sCaZOyIQnJstNdObYG/TY0ngqDZ7nKM7+6Xar84d2WbFxvJmlJyt1FvUgNPpDUVXlbaQghHsieDpouzb/hnXZ641W6DM0lz5kAAc/N5SMpls8r2/tlqVTja+Vp2yFtAjYH5FxsINihGvuPXnGoTiDkKU82EgW/oX9g2dasoqvaTI8Y6FvlJpGVUYNJ2l1LRKAQR8Q2T7wbd/HZdQ7BGzsAJjJjc23GGyMcVXvlKnztyXvadkibkM19hc2af3dg0Ka6De+zlCdmV/9ny7smZgi41uNj9iu7qo2YiEti4GbHzr3Zb8Ws3+ijv7eSzd6C9e3thBCF2eaJH3h8RyYrn2y+I9vijXfzRLxkb6+82+dvP34VvvbkPW07pE3E5q9iw1JAi+blbFyBIGkCVW3+nqU8E8BdvOKtlWnru+aaABitXpvl4hdboyB7j8CEXBLjMN38WStPhCrrN7o24dKyGQERVzxBydEmIU6BbZ74AfvRQMYAe+sd2RZvvIuArnVrDZasvy5i9vTKu33+DirwtbV52tb62qaXQ35Y0nnjO8m+qKOlJZ1nOOkepnayKdjK39ubFpLeelYPD5+7dEFpHw9v92f3L0+6teYo/Xm2tifJjnexGWG4fVj8G/9hAzpcvHRx8HmJ7ZXjeumOHoY+3mK/cS8t+R3dp65xrY7ShbXXl1FnwB0uPmtLi+8uX6YaNBhuuV3aydbhNvm7qq5XJjtl2+6JDQYMdzgrd+TcV23cGjGLN175lJfafFfsu+Tent/fi7/cw5c85Y8Wvnjd7lZ93m6vvHKkLT5/j7rP5Gvr9bSH52sbL0BajFsebcS1aEAzDDMGDLhlipM2G4Nh+qgRdNm4y8nGIw82vvzEThj7lwePGYZbpsw27KC6+91u2rSmTJktb9G5tA393Jb3P3n07sYvOdNuH/jpnlpTBvh4DBhxNy8TPjcrf72zfFlqcP47A2aMGHCDWa+rKq5XJjtd2+6JDRh8w8odebfJey3+PoM3XvqUt+vttb990pfs7Y/WdxA0PJJs273yUtl3ePU9rj2Dr63X0x6er7VM02EjIJ2oNjRbhlwsBwePkPAhycvyiB6nfFkjfHpVjw5mKI+XroiwMZnriXc3nKUpLIfuYi3LmIhJsQmd+9SgZYDAXIJl4+IRElU1jVQIAU954sVf7XVHts0bb7yOGzyuzdpSdpZLlz4wNr2nz7b2Fzu9+l7XU6KvPV1P2xZpYzMjNs8LH+cOeH6Y8/DFKg83nBCiHsryxHAI3tga0N8m5Kw+AzBW02WsoRaO0tO2I40YEzPGsQrO7Ld8bMZtvpWEEKK9lOOJ4UC8cZetk5uTSI7V/PKpIhctkTbAkDidR5+fPnHTO0wJIcQBU4YnhsPwxjuma6dziBpPBhD5aI20MTE9vCK9BauPQ6/lvQQhhGgxxT0xHIw3ngD9LdPE+0DQfJ6jyEdLcm3Swozo5h2btRxuCcwes/DFIWC53AJxu8fqhThGinhiOCRvbI3wCemtps1aNgN8Qi6P3/scq6dtl7SxmRLnS2eyptin0BBPAWu6tmrm0aW4CdFminhiOCxvbHn08QgJCIkBD4cuEZOn5okdPsfsaVslbdJbKjS9zJ8b4R7KrSSewnLXxr/jw5+KKMQhkdcTwyF6Y8uhu9jOMiIuurjFoXDMnrZl0ia9pYJsetka4B3WrSSEEG0mjycGeWPRDlonbQAsN5t2zPr3QgghniKPZ5U3Fm2gldJGCCGEECIf/z/Cmpj7DUdpWQAAACV0RVh0ZGF0ZTpjcmVhdGUAMjAyMS0xMS0yMlQxMToxNDozOCswMTowMHeNZSAAAAAldEVYdGRhdGU6bW9kaWZ5ADIwMjEtMTEtMjJUMTE6MTQ6MzgrMDE6MDAG0N2cAAAAFHRFWHRwZGY6VmVyc2lvbgBQREYtMS41IAVcCzkAAAAASUVORK5CYII="
    }
   },
   "cell_type": "markdown",
   "id": "76893599",
   "metadata": {},
   "source": [
    "An Instance of the Subgraph Isomorphism Problem.\n",
    "<img src=\"attachment:subgraph.png\" alt=\"Subgraph Isomorphism\" width=\"500\" />"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "017ebd7a",
   "metadata": {},
   "source": [
    "To build a CSP (Constraint Satisfaction Problem) model, we need first to import the library PyCSP$^3$:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "6aff8e4e",
   "metadata": {},
   "outputs": [],
   "source": [
    "from pycsp3 import *"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "9fb435a5",
   "metadata": {},
   "source": [
    "Then, we need some data. For example, for the two graphs shown above, we can write:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "cb78022e",
   "metadata": {},
   "outputs": [],
   "source": [
    "n = 4  # number of nodes in the pattern graph\n",
    "m = 5  # number of nodes in the target graph\n",
    "p_edges = [(0,1), (0,2), (0,3), (1,2), (1,3), (2,3)]\n",
    "t_edges = [(0,1), (0,3), (0,4), (1,2), (1,4), (2,3), (2,4), (3,4)]"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "ccd85cf8",
   "metadata": {},
   "source": [
    "In the pattern graph, we have 4 nodes and 6 edges, whereas in the target graph, we have 5 nodes and 8 edges. Note that we use indexes for nodes (for example, index 0 is used for node 1 in the pattern graph and for node a in the target graph). "
   ]
  },
  {
   "cell_type": "markdown",
   "id": "7dd5616e",
   "metadata": {},
   "source": [
    "We start our CSP model by introducing an array $x$ of variables."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "bf082887",
   "metadata": {},
   "outputs": [],
   "source": [
    "# x[i] is the target node to which the ith pattern node is mapped\n",
    "x = VarArray(size=n, dom=range(m))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "572d6950",
   "metadata": {},
   "source": [
    "We can display the structure of the array, as well as the domain of the first variable (note that all variables have the same domain)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "81d2d411",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Array x:  [x[0], x[1], x[2], x[3]]\n",
      "Domain of any variable in x:  0..4\n"
     ]
    }
   ],
   "source": [
    "print(\"Array x: \", x)\n",
    "print(\"Domain of any variable in x: \", x[0].dom)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "54607884",
   "metadata": {},
   "source": [
    "Concerning the constraints, we have to post first a constraint *AllDifferent*."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "1fb86819",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "   # ensuring injectivity\n",
    "   AllDifferent(x)\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "a8776ee6",
   "metadata": {},
   "source": [
    "Interestingly, by calling the function *solve()*, we can check that the problem is satisfiable (SAT). We can also display the found solution. Here, we call the function *values()* that collects the values assigned to a specified list of variables."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "b6227e28",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[0, 1, 2, 3]\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(values(x))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d8d47760",
   "metadata": {},
   "source": [
    "It works, but edges are not preserved. We need a table for enumerating all possible mappings of any pattern edge:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "266030f9",
   "metadata": {},
   "outputs": [],
   "source": [
    "table = {(i, j) for (i, j) in t_edges} | {(j, i) for (i, j) in t_edges}"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "929b9a80",
   "metadata": {},
   "source": [
    "We can now post a group of constraints *Extension*."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "4b0ca5cf",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    # preserving edges\n",
    "    (x[i], x[j]) in table for (i, j) in p_edges\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "cdb27690",
   "metadata": {},
   "source": [
    "We can display the internal representation of the posted constraints; this way, although a little bit technical, we can see that everything we need is present."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "8ec7be36",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "allDifferent(list:x[])\n",
      "extension(list:[x[0], x[1]], supports:(0,1)(0,3)(0,4)(1,0)(1,2)(1,4)(2,1)(2,3)(2,4)(3,0)(3,2)(3,4)(4,0)(4,1)(4,2)(4,3))\n",
      "extension(list:[x[0], x[2]], supports:(0,1)(0,3)(0,4)(1,0)(1,2)(1,4)(2,1)(2,3)(2,4)(3,0)(3,2)(3,4)(4,0)(4,1)(4,2)(4,3))\n",
      "extension(list:[x[0], x[3]], supports:(0,1)(0,3)(0,4)(1,0)(1,2)(1,4)(2,1)(2,3)(2,4)(3,0)(3,2)(3,4)(4,0)(4,1)(4,2)(4,3))\n",
      "extension(list:[x[1], x[2]], supports:(0,1)(0,3)(0,4)(1,0)(1,2)(1,4)(2,1)(2,3)(2,4)(3,0)(3,2)(3,4)(4,0)(4,1)(4,2)(4,3))\n",
      "extension(list:[x[1], x[3]], supports:(0,1)(0,3)(0,4)(1,0)(1,2)(1,4)(2,1)(2,3)(2,4)(3,0)(3,2)(3,4)(4,0)(4,1)(4,2)(4,3))\n",
      "extension(list:[x[2], x[3]], supports:(0,1)(0,3)(0,4)(1,0)(1,2)(1,4)(2,1)(2,3)(2,4)(3,0)(3,2)(3,4)(4,0)(4,1)(4,2)(4,3))\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "0105f914",
   "metadata": {},
   "source": [
    "We can run again the solver."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "id": "90b3c4af",
   "metadata": {},
   "outputs": [],
   "source": [
    "if solve() is SAT:\n",
    "    print(values(x))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "a00c1f40",
   "metadata": {},
   "source": [
    "Nothing is displayed. This is because the result is UNSAT, which is confirmed by executing:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "id": "27891c3b",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Status:  UNSAT\n"
     ]
    }
   ],
   "source": [
    "status = solve()\n",
    "print(\"Status: \", status)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c121d0e1",
   "metadata": {},
   "source": [
    "The instance is unsatisfiable because there is no 4-clique (4 nodes that are all linked each other) in the target graph. "
   ]
  },
  {
   "cell_type": "markdown",
   "id": "ad82c4bc",
   "metadata": {},
   "source": [
    "We propose to modify the target graph by adding an edge between the nodes a and c, before updating the constraints *Extension*. First, we modify the table:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "id": "869dc0f0",
   "metadata": {},
   "outputs": [],
   "source": [
    "table = table | {(0,2), (2,0)}"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "cf690c99",
   "metadata": {},
   "source": [
    "We check it:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "id": "2995edb7",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "{(3, 2), (3, 0), (0, 2), (1, 4), (2, 1), (2, 3), (4, 2), (1, 0), (0, 3), (4, 0), (0, 1), (1, 2), (2, 0), (4, 3), (0, 4), (3, 4), (4, 1), (2, 4)}\n"
     ]
    }
   ],
   "source": [
    "print(table)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "1b09e496",
   "metadata": {},
   "source": [
    "The we remove all constraints that were posted during the last call to *satsify()*. This is possible by executing:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "id": "5851bd47",
   "metadata": {},
   "outputs": [],
   "source": [
    "unpost()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e5a6864e",
   "metadata": {},
   "source": [
    "We control that there is only the constraint *AllDifferent* left."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "id": "a3a25bee",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "allDifferent(list:x[])\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b8e16e12",
   "metadata": {},
   "source": [
    "Finally, we post the new table constraints:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "id": "6b7bcd7a",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    # preserving edges\n",
    "    (x[i], x[j]) in table for (i, j) in p_edges\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "04ccaa57",
   "metadata": {},
   "source": [
    "And we run the solver:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "id": "b7cc67b1",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[0, 1, 2, 4]\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(values(x))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e7826477",
   "metadata": {},
   "source": [
    "We can check that 48 solutions exist, as follows."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "id": "b8311919",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Number of solutions:  48\n"
     ]
    }
   ],
   "source": [
    "if solve(sols=ALL) is SAT:\n",
    "    print(\"Number of solutions: \", n_solutions())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "98efabe0",
   "metadata": {},
   "source": [
    "Finally, we give below the model in one piece. Here the data is expected to be given by the user (in a command line). We also pay attention to possible self loops."
   ]
  },
  {
   "cell_type": "raw",
   "id": "a3c2bd60",
   "metadata": {
    "raw_mimetype": "text/x-python"
   },
   "source": [
    "from pycsp3 import *\n",
    "\n",
    "n, m, p_edges, t_edges = data\n",
    "\n",
    "p_loops = [i for (i, j) in p_edges if i == j]\n",
    "t_loops = [i for (i, j) in t_edges if i == j]\n",
    "table = {(i, j) for (i, j) in t_edges} | {(j, i) for (i, j) in t_edges}\n",
    "\n",
    "\n",
    "# x[i] is the target node to which the ith pattern node is mapped\n",
    "x = VarArray(size=n, dom=range(m))\n",
    "\n",
    "satisfy(\n",
    "    # ensuring injectivity\n",
    "    AllDifferent(x),\n",
    "\n",
    "    # preserving edges\n",
    "    [(x[i], x[j]) in table for (i, j) in p_edges],\n",
    "\n",
    "    # being careful of self-loops\n",
    "    [x[i] in t_loops for i in p_loops]\n",
    ")"
   ]
  }
 ],
 "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.7.12"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}