Graph Colouring with SAT
Curtis Bright, MaplesoftTUZOV3RLVWI8b2I8Uj1NRExDZE5GWkpsOj5bPEo6eGpoQXRHQ0VvVkxDVEpjRFhvWHV1dEVTRFN5WD93Z1JhZk1fRGtnV0BdU0xNdEY/RmdhRj89Rko7Q0xBZE5DSGM9RG5HUkpvQmtjU0o7Qz5LVj9LYl5NZVprUlo7REJHREJbcnBDUlo7RG5DZW5bSDtdZzpdZzpdZ1pjQzxDYlJFYlJFSFxcZUJcXE1ZWFlJV1llU0lWYD1ZeXV3d3N4WHl3RVlzaVN5VWlic1lYWUlZWWlJWUlpYXljVEJyS0I/Zz5bYj9CPFFaSjpKOkxyPEI8Oj5aPFE6TEI6O1JSPVo8PW5lW1l1cXhnUXl0UXliQXdiZ3FodWF2XmF2TXluSV94cT5lUEJbRUJsP1J2Y2h4b2loT2dEZUdjY2hlX1R1a3lpUWdMZURvT2l0T1lvZVg/Z0Y8QHA6RExYZXRAcXJAUG1NTXdWRW9pUVNHbFl4UHlreXVJSU90SU1yVWVKblxcWldcXHF5eHFZW0VWW2R3ZWN4bFFfZG9eaXdgYnh2ZHdwZWF4bUFRbjs+XmY+cjxOeXdxaV1IdEp3Yk1Hb2Q/eXRWa3JWd2V5dGlAZXRCW0VCYEd0ZGVoTnFVXFxtaFxcWVdRZWdpd2ddRXc6O0RQO1ZOc2hxd2hkbVlWPXRkPXhQb0hWd1RCR3I9O0ZmSFQ+dVY8eG5jRHVkeWpqXFxVWG1VQFFKPDxOZjxySmxxd1V5UGRWalxceG1ETFBEUV9VUEREbGY+W0U+YD5OdG5Pb1NIa2dAeVRXZFF5dFFBZUBDWz5iYVh0S3ddbD9cXFBxbXROYXROcmxOWlpeXzphWlRpd3BfbEVxbVNAcFRIZHRZYVBIPD1VOkdHSVNXWWtFUFxcaj88cTpgcWtcXG9fXVZwPmJSP2pjXnZ0Zl52R3JjRj4/aDpTaFJFVVNFc1J3Ym9tZ1BzRFFDaDo/QkJeXWhvZ2hPbkZ3eFFgeD5ocEJmYUI+amp0ZmtpeXV5aD9DY1VkVUt1S3lHd3NJeVNWO2pKTFl3cG1ESFRncFRNPUs9WVNvWXVZcXlQeFlrUXhsUUxFQTtQdEtkcE5IVGRIdWZNdFl4d2hxd1xcbHNkYU5ieWpvSVJPUVdvbHdBaHBzSHFDdW86dW89aHI+PFJSPVJDUVBKRW9tWXhtZXlRYG5pUW5IWG5tSWw9ZFBAcHBYTXZ5eFVMVU9lVE9JeGtJUHlxUG5gdUtrbGp5UVxcOkBwOlBmSmZeRXByUlZ1Y0F5dFF5VGBpaGZ4eE5za1BrPFZlZ0F5VFFkZHBdc1FmUXZcXFF2X2l2X01Ad2lYdWdRZnNHWkpuXFxKP11kZmxERmBFcXl4cXlueV1dbl9laXh0d2JBd2JuWXJncWh1YXdmYXdHd1pkd2dpd2tjV2tyWVtlYVs6QHA6YGVCUHRRTmZWaXVXaW5qUF9PUHJocHdpeXdzaV9CYHdqQFZLSl5RbDtYS0VUS2NldVlgVD5oclpBVXhVb09RcmxYSlpcXE9aZE1uV1xca29kUFZvTEdlZlF3bFF4THh1TmZqdUI8UUJMT3Z2YXl2U2JGW3NJPVU9a2dMXVlvPURDPFJSPXJyXXRlaXhmTVBqQEw8UVZqTW5QZW9QVVJebF08UVpAWWJhcWJfeWM9d3NDP2U9QGFfZmx5XnNHaXNHbmdHPlo8UVp4T3JIcXNIYWxuVl9tYWpvPl1EWG53SG1IR1o6QHA6QGRKWGB4cGVYRmZrTnFXcV9MZnA6PlxcUD5cXFtWZVRobENPclRubEFAX1NwWjo/ZVtRal1XdW9RaXdAaGFpblJPclxcX19nZl9LWXNcXE90dz5bRT5bSHZleXBpX3dtX2h1aHdsXFxnZGRgXFx1UGF4bmFoPmBKcVo6QFBJQlZnZVdHeF11c0dxVVZLRmZHckpNZlBbdls7Q0U7eFlDVGlreFljdWZPU25PR09tZ1dlUldHRlxcRUhFV0VES3I8W3k+WXZdWWZrX3NgT2hDU1dqW1RBWWJIT1VaW29xUFBKYVNTcG07THJMeVdOXVc8bVo+aFpSb1pxTmJSSXVTSWBhZ2REYW1XR2hFR1tOSXg6QHA6dnZbV286aXJeRmZHPmRBWVo8UVp2PmJ1aHVwaHZ0P11gXl9Vb2teYmo/Yjw7ZmVnV0RNU21PZEM9VT1HZkplRV5JRkJmW2JxbkVmclBXdXJGYlJXaltgbVJfXmRHampUdGt0UXl0Y0lVV0VVU0VoZmVURFFoV0VYV3NDQHVFPD9oOkNmSklXUE1EdlNDZWFibztFVHNTZ0V0TWFqakBqazxteFxcUGpcXFM8UU1aXXhbPEtFPExCbFFXVHVVWXVNXFxWT01TSmhVZ3l3aVlOS1VLPmhKUnlqSDxQWXF1WFFzbFBPX1RzaEBsYmhKPFFKZnZyUXl1eXhpaT50az9sQD9lPXFvYkd1P3h1Oj5bRT55Q05xP1FrZ2BgZXZiQ1Znal5gO2FbXXhbOz9lOkhbYllyaUZzSWBtUk9yVG5udVl2XVlmUlhcXEJWW2JGXFxeUnRNdHBzSHFjZlVlZExvV1FddUtVZ0xFZ1pLRElLcjxLY0FXVVtVVnNhYm9baV4/U05RQltMaz5Vb09RWGV4bHNYTD5obnlMT3RMVztAcDpQVlpBd2pEVEFAS2U9Tmlkd1BOcmxPXFx0QWNFT2VUaGxhX2pvXl9JdnNIcXNaP2laXl9aVm5GXmduTl1obmI/aG1dXl9ATmNgSGJSP2JkP3d2aWhsQXBWZ3BkZnZkaGVbb3A/PltFPnNcXFZaV3BzZl9oUUBwQFZia1diQlliSkJGVVJnb1RtTUZHUXNpTXJUa2ReUUhlc2U6PVU6Z1ZiQWZpdWdRWXg7UWdOd0NwZWZFT0NEWUVLZ0tbRXFBbG1QRHZNdU5sdVFCVFN5dUx5XFx1WD1MUDxsUUxRVk1OZFhtTzxLZV1KV3FXUUJKa1RiQXRNUUZ2WVdMYXZTQ1ZHa2JIb1dLSVRFW2JPS0ZyY3ZBeXRSb2d5XWI/QXhgYVQ+W2I/W2ZYWWd3a1dua3dlQ1ZHa2JAdUVcXF9OQlRzeT13Yj1rWUlZQ3BNTWx0OmlqQExrWlxcT1pAUDtFdGZtUHd4U2dJeFVAcFJMbFVdVD1AcDpgVUpJV1Btd1BVdTpAcFhVSkNQVVpuXTx5cW5WX0pudGVHaUJwa1Q/XmZ2aWZIdW1gYGU+PEtCWGNZQl9SZztMQUhuTWFvPFxcUUhNS0dAcEJ0a0l4a2JEbUBEVnNQa09obE9AbGFdTT48U1JValtQcT9McXVBWT48UlJta0NBckp4bkJlakM9VUZMcWlBTXc9SzxRWD1Eal5IVTtAcExsV1RtTWFxSj1AcFZ4SmBEbj1AcEBIcl14S2VlcFRMTG9AYl5HXm5gYGU+XFxQT2JWYXVWQW5eT10+aF5FVml1V2lbaG5TZ15bXm94d3FJaGhSXnJLQGlYeHRXUWdvQHBUPl5mVm1KSW5EdnBAcFpQSGpReGxRWHNFWXNHaGtHSHVTSWVfQHdzYW9lZmBtdmBxdnB4cHF4SXhdeWJKR3FIYHJdR186P2VwP2prUV9UdmRRd2RvUWFrXnRsUGRhTmNXWV9vUWJEQGB4cG1OUGFPT2dPcHlPcGlgPnhPT3F5eHFBX1VQcD1sU21QUnRoS3NsVGtFdktEWU91VD1dUW9ReXRhbk5hUXNJbm5ZeDt4b1JRcjxRSmZ0Sj5oVkhMUVtITXVhdlp5eV1oVkJJcHRRUVNQb25pdFFNb0N1UUlsc0xxcXNMUWRFWk9YW1dvckZgbTpJcnlZZVNpc2VmeFZAamdAeXRxb05XdmJBd0JWY0FAd2E+W2VgeU9QW2xga3NPXFxYeG1ZWHZCUXl3T2ZwUHZlcXFQV293ZmF3RmY7dlo7b3BrVVJtRlpXdGY/dj15eXZBaGdpZl5VR3hvSWZ1V2lVVjtDVlQ9RmZPVDppY19DaEdrY1prd1hPeUpHY2pvRUtpZm1dZ21xU1BvYl8/QltFRkpBVHZLdkhJSUVHZVJRY2lnckl5ZXlTVlNzckRZUj53Ujs9VVM9ZklPWFo9UmlHWGxNWFxcX3RIbUM8UXV4Y0l3Y3Jsa1NUQUZrPUJHS3JEdUJeR1VfO1hBS3VzO0NlR2NtV0NScUVCU2c6O2ZGR0lDa0NJc0NPT0lCSVJSdUJVU0VVO1VAeUh3V1k+TXY7PVVCV0ZOO0JMW1hEZVdfQUZmZ0NmeUJDY3ZbS3ZhP0ZmR0NFQ0J1QVNGP2lma2dLV2JqT3dZbWl2RXJsa0ZZSVJrPWdES3JUU0Y9Q3Y7d0ZBXVVnYXljU0RVZXVPVWdPXURiQXJyQ1JSRVU6X0hlX1dCV3lfX1ZNZWJnV3I9WVJmO1ZAc3hZQ2RyQWZDU0NbTWJ2O3dxWXleQUdjY1hXT2Rnb1dlZWhUWXhtWUhQO0hNcUM7P0JlPWc+Z2JuU2d2QWl4b2lIV0VFYVlHXXNQXWg9XXNbR0hQbXlna0heWUZFP0RDU0Njb0c/RUZIeVdid0ZlR3RzYVNmZWJjS0hqb1VKa1RETG1PRXZCWG1GQWxZaHRDWHFBYWtfUG9RQHFNRHdGPHVkQFh3PUxcXEFUa0FYeFBPTGFvRE1yTVl0TXF0UHFsTGVwcnBVYWFUY3hPRGVRQHl0b11tWU1VVVVVVVVxeXhxQVFST0hOSVRSRUByQFBSUmVcXEROdmVpblxcbl15Rm5wdmBxdnZheXZlSWBSX3FaX3ZRSGp3PmFWWGBod3lHSGNxdnlBb15FR3FQYGBoWHFbdmFLP2VWVlpLb2tYd29BTnJsb11eUWRbZnNEQXVdV2J0ZmZmRmxXb2VYT2ZDUHNYaV88Rms+WWlFP2U+QWR2d1xcdWZtSF5bdGBnZmZfZ2ZjbGFuYnl3WXlxeXdrX05fVXZ2YXl2W15qYmd5Xl5vckF3RFZiPWZraEF4dVZhdVZmeUlbZEB0Ul5oXm51XXdsUFliRU92V3FtVllmQkFibT52YkZ2UmdhYmhlVz9vPFdmUmF1VmFuP3Znbk5dWl5fY0FeYT91dWldQD9eYkl1UnB3PUdpdmF5QmFyR2lzR3hvRFZyWU5yTGlyUD9oZmBzZUliVGl0YWBZY1RibUV4b3JqZUlrU0ZYP0JIb3J1b3Y7WWZqd0ZjSXJbeWJBQ2ldb3Y7dVM+Y2d2ZWZMRXhgdURxbWVqP2RgZVZRU1RIeUJBXWlqT1l3b2NfUUhJY2ViZ1J0Q0Q+Z1ZTY2dQVWNJZXNbU0JnS3c7YUY9Y3hyS0RGZ3ZsZ2JyR3ZcXHdDT29FREl3QWVCY21UTFt1VWFGQ3dJdk12SGNUYkVEV3FXUVliWnNnTV9iP29XUE1SSk9zaU1ZbWtISVtkR3NDSEd0V1lGZmtjaXdIVGNDQkFSQ2tTaFF0TFFUZGN5SGdSbW9DaFVDSHVzSztDRUF0eEFEQmVlYT9Yak9zRW1ZUElycXdDYVVGTDtmTWNoVldEY3FzSmtkaG9oU29ZPG9DQmF0PU91XVNXcFNlUk1JQzt0Q09VZ3FYVVtiT01zRFFyUGlmY0lyQ2V4PT9UP29nOklpcG1GTGlnQXVWS191WHF1PGFpXkd3O2FoWHFHZU9SckFzXFw/Zm1DRVc/WT5hUk1rRGc9dkJVaExHQ0hbdWBVeEVBWFA9R0pbZWJnUmg7SEJTR0VbWHZlRU1RRj5RdzthV0RjZXVxRl1FQj9LckM/SGtfUk1JdGNtVEJZSE5fZ0FTaFdpZV5jaEE/Ym91Ujtdd0JXRmtdYj9paURNZE5VWTpraDppRm9HWXZXSE5HZ0V5dHVpaFRlQz5nSEdDZm9XdHFNVUlrdmN1RUhjVGJzRXRDVEVNVV5rVURndWpxZkdPV1VDeVphR01fSXBdU3lXY3BnVmhfdWJFV19TdERtc3RfZkdNdztbZ1o/ZGhdWUhpdmVrQnhVaV9hV2prZENTU2Z3dkNbU1tRZXZpVmJdVUpLYz9hWDxbWUhNRl5XZlBnU11HdlRxQ15HVT9jZkFDZkRjRT9zZUBHVWlvSGtXUlJNeW5heGZhd0ZrZkpLZVhbYmRbWE5LREB1RVQ9RmZvVWl3Ym5TR3FleFpFVE1FVGNpWFpPQ1dXYlhjWWJVZ2ttZmNVYztNZU9Xdz5nVE49Rj1XclE/VUx1RDtJclZTR21nR0ZJVUZvU21PUm9nY10/djtNVz9RdFljaWBrRFBpUmpdRExhWT1XSD1dYl9XeUNVRkdRQ3Q9RGQ/dEk7dz5fRk1nRk1Rczp5aFxcc3RLS0hKS1lKS29RQHRXZHBGYXRBcGxlbU9CVXBscUpWRWxYbUpDTHF1PEw7PFZicWtUbUpEUHdEXU5mbE1rSGtuVE9pXXVlUGxCVEtIbWxZPHZIUFVFVEtFZG54dHdpVXVEWXRNWXRzSXlzcXRQcXREeUtmdVdpdVl2QXlrTVNuTFNgZUxMPE5KaUxkRHNrVUpmQFJxXXR0XVl2XW1uWVA+WU1jRXleRE9bRUxPZXdocXdIQU9vSG5OdVRjWFdfcFdcXFlreGFxP21vTVBUbnlvSXlzSVlOeWhqclFxeT1Pbzx1PmRUYllMYGBYTlFtSHlObURYb0R4ZW1RQ01TUnVwcXhwT1FXb3VVY3hWbGB0a3VMd2l5WF11bnR2ZFF3RHV5UGR5aUhKcUBMalxca0x1a21BbkRkeT1VcFNhTUNddFxcbVFzQVJIeVRUbFFDTWNid3JVWGtjPmhqcXRvV29OZ2BoQHBLSWpxXm5TR2ljeFpFWWNSUF92ZnFFPmw6ZmVKUWhxd2hRcGxJb2NJd2NNP1xcUGZxO0ZxQ3dlTF5xdHZlPkdtb2Zual5gSk5panZbW05jYmFaOl5cXEVmXUVxY0V5Xk9Jc0Fua11walJ5d3FZd29RaWlGeGVYeG9nXFxZcFpMeXdcXHFeO3dbYFdeZlBmTU9kO0Zeckdpc0d5R3lneFdsO3hjQmhqQFF4Q1BpZ3ltaV9udmdoeHBgPnZgaHhabE9wQ0d1Z2dcXEReZzxGWkJQWkNYcUZhaWxudGRxYmdgZnBvaHBxXk1ZXXZPZGRIdGI/dkhGaUBWYEdYb0RQZ21oWkJXclZhdVZvZnhGXmhOPlVRW2V0T1BZQ2F4QFRqUkVvSEVzeUBKVl1qa3B0WmhqbkxQP1xcUltJdltJVmh0TVlAdGVcXHE7PVVVRFVZZW1oaFBfcE9obE9qdW1aeEpbUEs7YFF0PWxpaG9rXVlsTFdcXHRKc3F1WkF4akFMcUlLdD1MZEBMWjxMVVxcTEh5Tl1gak9xc2txSmdMWGxwdFBBWFlgcTtIdjtManN0cldMSkxBdEhodWBRVnNhVk5hTXFNWHZIcnBQVGF0TmE8cUltUWNJUk1YTlRYWEhcXGxAXFxuW0F3YkFPSXRtZmFrXVlsS1V5Ul1za3FKRUBYY2lRPHRLcU1QU0hLRml5PElYaFV2R2xXaG1XbEF4Q1F4cmxRU2ROZkhtU0htQWFTaXB5b3lSbFhRc2V4WmhPYklSYlBySkhSRjxycFluYHRMSWxxQ3lOT1BTX2lYaEF3YmhSaG1nVnlzbnFaQVBjd2l3aXdpTWl3QWZkVlhvREhxcj50PUBEPVR2Y3JzPUhGS2lVd1l3WXdZVUhtSXNScXNFWWZASXhqQXhKZWNjaUdnY0VQaWR0UXhfWWN4ZWVIdWZdd0lxVWZLQVJ5QURxP3JkYXN2ZVZiZ2dxaUJsTVN5a2dZUVZuV3VnZVlsX1VOc2VGXUZmR1JWU3VpbWZDdXhcXHdlVmVlSllnSW9JcW9XSWdyb1FWYkdYb01CZVl3ZXFodmNFbnd5cUFiYU9TXFxZZDthZnBRSGVVV2VdVmp3dU1baXR5eHJPd2FVV2VVd29NRHdBQ3JXY0JvQmBsTGh4SmdFcEBoUmhgSkxAalVgcmRdTmNZUT5dWUxhT0J4U0BZVUBEUF9ES0JpTl9wd2FwcXRZakxdeG1UbVVYbWNQWEVkWF1gTVd5UUVkdXhBbkF0UlhpTWFlakxBUFxcQVheUEtsQVBZYE92aHRebU5DdG1GVXVEQVNHaXRkZVBUeXd0dVFtWHZxQHFRdHR0XXVYPGxWZG5xZFllSFNaTG9cXElLWkVzY1BNam50XXZ1ZG5wVF91QlZ3Wk52WlFsY2BndmZsSnhjdElncmFid0h5Q1hhV3BzRFFzREZgRWdhSGBqR1Ffb1ZgbVZiWWZ5UXdxdGlkS1dtanBtQG5gV19bPW5yclFyaG9nO2hsRlBbWk9cXElnXFxSTmlgeGR4aXVpcWlBaXVNSG1JT3drWXdJeXNJWVxcSWFeW1lsXnBmS3l3cXldeT9qWGlMO2hGU2RcXGdYU2tJUGNmT1VyO0dUOk9jRmFxTz1qaWVRdXR0RkxZTFRzQj1vXnhUWE1VVE1NW1lsTnRxWGh3V0VxPVh5V2l1V0VTZXV4dERuPWx2VTxrWFxcdGBlV3hUS0ZcXFFPbVhcXHlQaXVqc010bWRUWFRsZG1QVXBKcFRVV1BQRXlSUWVybHRMV1ltPVhqPWhwb2hwQFVuS3VvUUl3eVhNVVRNUXRMUURyZE1UW0RxYElOZVByUXhsUVhvZVhvV2llRVlzRVlobVdoXm9sbkhpaXdnaXdcXFVQXFw+d3NLdl1CUWdYUGBacWRheWE8bnN4WXN2RnNBYW5GP19QSHFCaGxCR2FBZ1pKWHlEZ2U+eVpcXHhra0lgQElnTkl1ZXBkZUhcXEtoakBXZWxPaXZAbWZhZ11Oa2Rwa0l4a11JZXNXZ2tPcHF3X3hOYV1WcXZhb053am5gXFxLeHRDSXNDb3Zdb19QcWJWdnNjRnM9PmNcXHhaZ0FcXFBobzpXYnhpbTtwZVtXZ2VXY0dVQXNDS3NZb1NmVmN5Wm9zUWlSb0V0TUV4XmVzam1EeUl3Y0ljWGt2QmF3YGdleFlEP2dHSnljd0dJal14b3NTR3NyUj13Q0tIaT11ZndCbW1yS19USFVkbD9lTl9lZ2tSUnl3cXlEUXNEXW9VdUNTbHVXSV9Ec2F2XkVTW0F3O0VJd01jR2dYYW1kOktmSUt4WF9kdGtTWnVkbllCVWFockNTdmVCXFxJR1RhWG9ZSExRV29fR0hZVmlbRl87SVF5d0FZRTxnWU1PZnVzSHZNQ0V1eGxNY1R5Y1BlV3FjU18/cmtddj5xYlpnU15neHZhVk89V2tJQm1DZz5gcGxNbWRYeVZxckBxcl54TGZpeHRVTnZkTjtBak9FTG1NV2xFdEd0bU9Mc0tkU2ltdklgbVl4bWVoal5lUDx0UXFwUVZxdVhxalhcXGpkXFxPQ3RqQXhqa1V5RWF0R1RuQE13VUFrYVBWcWRTXFxtVEpFTnQ9UGlEVkNtUGN4dE9gSnl5dUFRUEZlTXRxTEdRbkdVTW88WEt1S0RVbWBNV1ptamVoWEpoVT9Jd1JvbnFYc1VJdVNJZVRhbkFPa3VhZmBpZU1WY05OaGVWeHhganZBYj15Y0ZpcEpocHVJdmhQYXRidndGZkNXd19Icl9CPHlPcnVOYXROS0hZX11wRWlUZ011TVB1VTxza3BvPG12UHB2X1FNbEl4VkVReG15bXlteWFNV2RLYVVQRlh3dnhya1ByO2FwaFR0SllRV3BrQVlPWWRNO0RvWG1UdWBReFl0WXB5XnR5Y1lPalxcUWRQS2tEb2tocTtkbltFWXNFWVRtTT1ZVWRAbF5JU1hgeVFEeWhpbEZNcmxxVU9scXV1eGhkWU5lVFl1WG1ZeG1ReHlYVjtodk1kSnZQU1Z4dmBBakNlc0dpcz9FVXJFbXVNdkFJUWlVT1hQanhoTVNwcTp5S0BJUEF4UXhJeElwVWhUWW5Ia2R4eHNcXGtsSXJDeFJpQHJqQVc7dHVQeGNEeXhFV249XmxBYWU+aDpFQ2JvYjo9VXdvVUlNQ1tlQ0ZrQ25zc1VbR3Jnc2Q9RVlZZkA/RXhvVl1FY09ZYkhdWXZPRl5DdkVtVHVfaVF3RVRldmtxQz9HRT1FVkhZY3JVZFRxdVhxVEFFVUdTdm1FSGFdRVxcRUU7TXhOP0R4a2hxaVhrWWY8b3RiX1RqU114aHBvaFxcTnFoUl9zRUZoUVlmW3FbQnlySXhdXVhkWkliQElvPXdaQXZaWG9hal5tdD5eWUF3d2ddPD5cXGFna1heZkhXZ1pWb0hOZ3VeZD9uaWZGdkF5c3dxaXlQZWdwcUtxZHRfd095a2xWeVhuXVhecXY/ZlZAYUBYeFJnXFxAaWM+ckZ1Qj93VWBtVmBdYmFDZ09rVXhDZjxPSGM/V3NRZWNpQ111dWFxRF1xU25VdFFTZWBrVEJLVWdvZERRZFxcO3VOd3dveURIVUM/Z2lQV0REUWI+VVdOZWVNT0dMZ3hdXXJJd2RPPWlIXXVvc2JCZ0hVZ1N4QUloW1NPb0lUSWVZd2V5ZUlDaVVaaVVla1RyRWdcXHVJVl95Q3NzSXVTSUVEYWVlX1tnUFFUZG9mbmFVbG9XcVdDdztXS2F4ZWNkRHdWZXlnRUFCeVl4WXd5Pm1mYG9nTGtyVFlnT1FXWG9SPXFWam1YcG1Ucj1XdT9WPFFYPFF5Q1doXFxfRkxpc2NnQmF3R0tXZFhVZ09xSXlteXZbZ0BJd0NzeGNDaTtJY3ZdZExPZltrdDtJSWtPaXE9QlNNVU5TVk91RVxcQWZjYUZ1X1lQTVdFX1llc0ZcXEtnXz1EPEVkaXN2Sj1mO19ZY3lDWWtJYk9jRD9XZVF5YVVDc3djXUlDR2Noa0doa2l2RXlkW3l1XFxRckNhZVddeF9BcmdvSD5hR1dvc0l5c3c7VXNJU0BfUlVFV1ZpdkhfdVhpaVJpaXlxeU1tVkddcl9ldFdpdVd1VFRzYk5HaFdLZzx5SVxcX2hEd3ljO2ZnTXdaQXY6b0h0P1dYV3dmXVhQVXhoaXV1S0RGX1ZNU0ZOZUhGa0c/TXhaW0NpYVVFdVNPc3NUYVh3RXVZYVhPSWNIQVdxY2NtWWhkQ3hacWlUc2Q/R3RpS0lOQWhVZ3RoRXZVSVZrYWJfY2dhT1RsdWVlQ3lCX0hXUWhASXdCXWk9TVlKWUVPPXNgVWR2a0NHbXNOQ3VSV2NPdXhfY0JCT0N4ZVJ5d2NZd2I7aUVOU0NmS2Q8b0VGPWdEY0VXPVh3a3V2W2Jgd3M9T3RgU1NkT0h4O2c9TWdqc0ZyTVZMX2I7bVljRXZiQXZ5c1JPRUZpb1hyU1I6P1VJa2RLX3RUTUNbRXNTX2lcXFhvXFxhdUhJd2JBV19FTj1Ib01YamZQcmN1U1ZdbFhcXE8/QHB2WVF4bWNkQGFOQG8/aV07YGVmZ2FGWWNnUWNmSW1NRmw8Xm1CVmVYcWhiUGNsRl9zVnRcXGBrO0B1RGlsPmdfYXhaO1lxXFxIcnNoakNYZUFRXT9Abk5xY3ZRb15WbEROY09ucXB5eT94XmRHdVdAalVEQWlDX1lJam91Xll3X2dSY2d2TWNmdm9XOk9naj1FdnNVUF1XXFxvRG1PZ3VXZmI9eXZtVGZPR0ZXR1NnRHN3VFtHczpVQnQ9aGZLckxrV0xtQkpjU2ZlZFRDY1F3d1s/SWRPQ289R015d2tzSVBjeFpFVT5ndko9ZltfV0E9UlpFUnJ3QnFvYnc/RUt1RUN1VEJ5YmNTQm9Lc2hzZWJTd19nZXVrWWhDQ2tFV1I/Rjw/eD1JeU9vZmRFdWNlZmFlSFJFRXJbaVdrZFRrRU89WWpbc3JDczxddls/UllhUmBZYks/RHRraWh5Uk9tWEg9WEhNVmNXRUNPR09hZjxzVD9XRmVHRltDVEVZZT1bVUNbc0VJY2ZDdk5VdXZHQz1Dd2xjRnhPSWVHRlZpUkdrZXFdVGl3dGdRdzt1STxfR2tVR25VZWQ/SGRBeEtbVlRnZFd1aFFlZHdBWXJXWXZtVUBbWFxcb3RXaXVXR3lxdXhmVUNrZ2ZEU0JJVWhsV2k/P0dpY1NEPUlyV2ZQR3lMPVV1b3lXRXZCT1VXVUVheVVId2d1XUleT1Rsb0VmY2VqX2VoQ0JjY0R0T3NGQVVyVFFxbVFzZEpAWE9cXGRYVGhsaVhMTFR4aXVqQExWUGl2bEhrb0FSPWBWUmxZOlxccXN0TVZEWUJdc25hbUpZdFxcPExZdU1FVFZTRUpEWU1NUFhOXFxORmRzXkB4cm1uQWRTZFBSSG1qPj1YXU1LRmhqQVVTeXVLYlBycURuTWRwRFl0ZV13R0lVQ2B4VTxVdFB4Vj1ZV3RVSUxvVWhsUmVRYk1qakBuRFRUQ1lyTFBOa3FNUWxNTnh2PHl3aXl3bWlTO2h4RER0PXBOQlRXWkF2alhKdVB4amBrYVxccklIWW1UVjtpcWtMc2pMVTxVb09RalNNc0tZakBAS0VJcWtNVFBEckhEV2tQTT5Jd1NpS2lNamVwa0VcXG5yZXVtUU0/aFZMYXhaSE48UVhrPVJFaFVqVXBETXhXTEtzZVBIQXBxWXk7SE9EZUxsWGxlSXV2dVdpXXhaSE48UWpkXFxzOmRtYmhsWWFMRFltQjxORHh1RUR4PUVsYGVsUGxqPVluQHB1Q0xvalR4WGlsbUhOVnRRQVB0dE1YT0huRFR4cmFSQGxLZGVRcHVXR21sTVlNXFxETHA8S1ZpdUY8dkJwVl9QVGtNVj1cXHByQXVebVhbSVFtcUpraXhGWVlkSHNDWFBEYW5DZU1ZdE1dcU1hSXV5WVBeTFRzdW9BVHh2ZVN3XXJbeVVAUG1TPG1ZcHVabXdHUVNXaG5LTEpyYFZ0ZHdmVWs6TWpsRE1ORU55XFxXcmxLbD1TSUxNX1xcT3BVTFpdTXM9cmFpWUN5U2tJUWx1TUhZck1gVU9MVlRdUng9VVNAUmRgS1VgbGVUcEtocjx1WE5RU1xceVA/TG5BVFR3RVVMdVliVFZwXVRJTFVaXFxPYlByPD1yV0VtQl1OSHV4UlVqVElOSHhrSXh1bkV2c2xxSHBzV2lSd2xzaXl1eXh4U0BwcnhSQWx3bkVqRUhRXzxWRlFZajxPR2xRP2VMZGFNS1xcU0VAT2plcGltV2hdWWBcXE94UWx4dXY+RFVLeGpdVXh2WEpueVZhZFlfXVhtUE9DeW1vQFhFaFZATE06YHZKaVM/bFJWSG86VG9FbHJAZVRyQVlUcFRDbG5cXFFxWFxccDpfZ0tWcFlBdGdXbW5Ya1hgXlpYdlk+eVZRY2FYeWNBeXROdGZgeUpZalA+W2U/XFxGb2ZKSGlqR2NXdmJOWGpvYWZveVxcQU9tT0dpakBdRnBwPT9lU1hbRz9qY0F0XWhhPWhvcHZ0dmZqclFxO2hlWz5bPFFqZF5fT05hTHZ5SXlpeFlgOnlvSXd1VEZ4b1daPmhmZUF3Rkd1dFFyUF9aaj9kVT5mOkhbQV9tYGdqPWhdWWd4WmhjPFF4aU9qRUBfPFF1VVl1TXlmc0lebm9zVm5jbVBbXkhiPz9qdD90VEZmU0djZHlbZFdaXlFmPWd1TnBzaVFuc0hsclFhTXhcXExpeURZXmZWa2d3ZGZBcEB4dVdvcl9oZzpgd2s/eXQ/dDt5dXFfXkdRW2RAcF4+ZWlfZ2FgX1RJXUhRW0VPZVJ5dF12YW9fXlhBaGdnaWNAbUxwZl9PaEhYY0o/cFhhXkRRdXVXYk9ubHFIWkhPZ3hWYF9wa0FJYWpmXkdPY21QZk8/az1obWxucD1XcWNRYFBBXz1uXl9nZj1edG1oX1ZpXUhObWpga1NxZGdBa0FBbGpueURRb3F3ZnZoZVs/bXQ/aExgYW5HYGlQYHNHXW1eZFtHdkpAYERvcmBZdV1BeVNhblheXTtXcFNhX2pfeFtIc0FuXltPaFNeZXJ3eW5Bbl9PclxcV2w8QWZfVmVVPl5xSWJxT15jXmVBeXRNR2k/QGhbaWFNWWpQSFtFaGNkSHRiP3JUTmtUX3NuSG9nUWFLV2NsR3ZbYW54SWFpT2pNdnVbP10/QGJCUWZUb3k+PltuXlxcdUhaYFdjZHdmZ29fbW9hdXZzRE5zUGVcXElHWG1JX01YUml1SGNGVndHVW1GRWtUP0dGTnFjQnN1OmNoYFFkXT90b1VkaV9JQ2tySmViPz9iY3dVPElzbD9CWXNDZD9oWmdWRnl5Xk10Rz9zakt5al9Dald0UXVnUVlYdGNZSmVieEN3O0VEPmdCTU9HZFVCZltSdUF3PmVHVW1XaW9DZWdETD1oUHdSY1NCTGF4Wj9DPFF2QWdDYWVibD1TWXVGZEVlaXdFYGFzRk9WT3lCYFFZX2FCQWlXPl9WVFNzalV4Tk9XcFNlal9DdU9Zal1CVj9nP01GS0FVXmtZY0VXQ2dHWz91cV1kSm93YmFIPmVlRkdjcmFFSmVic3lIOlFIbFtGR2dDaz1Hbz1XWk1ndk1VWl13cD15YEV5Pj1VPmdyZD9EO29CO1dFWm9jYmNkcWtGZVd0Y2FkV3dpZEt3S1diWFtYWD9oQDtJeG1zcV9YX3VUc3F3ZmF3Tl9IO29iTWFnRHFTVWVoWGFEP1N1W3dXPmdiOlVibmNJckNTWGtEX091Rm1WeEVST2t2U3FDP2VFUz1TW0FDcHNVYk9SW1lFWlNpZEN5ZztlV21ITUdpb0FUP0dlcVdSS3VTX19GYXVDQXlzU29ER0FoYU1ldkdyRWFkYT1ydnVVal1IR21zOkNid2FUPmNZVGtTbW9iT19mdz15R3lWRWVWeFt0XXdlcWd0WUtWcm1IQTtkVmd2X2dIO11EPj1EVl9kRlNkbGVWPVt2Xl1kXlFoSHdIXkt5Z1NVX2t0WGFoQW9IPWtJWmtHdVNmP0lWPFFSWkdyc0NlXWd2W2FYbW9EbEtCPUtnSmlYdztHSD9oZGl4dFtTRD1pWFtlPl1CTU9Eb19YcVNHZXFpbVtUW011VVFHak11a19HcD12WDtlakNnXjtEb2tYYl1WTkd3QnNkZ2F3ZkFzcz1DX3NoZFtkYHdCP2tTSGNkYVF4Wzt0WnFmOklFQ110TFFXS11UU1VJTkVub0FuSk1yPEhTX1xcdTpkT0hdS1lgSkg9WmV5ZXlRbUV3XFxeaHBqZm5PVmxKQW1WSWtnQWRgQWxuRmhOQWpeYGZhYXhaQWBuX2lXX3dmV1tiUGJxZ3haYGI8UWpkXmhReVtPaXN5cXl1eXV5UWtXZmlCdlxcWGlldz5fUUBwWk9kSElxQ15pPFlhVnFlU1hcXG9gbkM/YFBnampGbmNxdF8+eHY/ZGhGZls+dFpxdHRBd2pXeWVRXWZndTtfZE5veVtgc2p5bWJoeEtAbGhWdkZGZls+VFt2O09odj1lWGtYZlNpXW9EVj15PENydV1jVlV2QVlIQ2NJUmdDY09ZdWlTRF10bE9CeEFIakV2YT9TdT1EUE1JblVpVz1lTkFVam1ZTWd4T0d2PHlzTk1VaT94SE9Vc0NnUEtnSklJdztHUT9oWk9DX1N5WF9JZ0tieFllO3dIc0NURVFZWUNGcj94aEt3O0V3PmdCTU9kQFl2P19TOlNzU0lURUtnajtVdztHVD9oal15ZmNTSUtoSHVHXmNnUXVYTlF3bk1JUGNUWz9ybkNIZVl1W2dndUt2dkNWRztYdmFHQ1l3XnFXUGVycGNIcFdlYmdGcE95PktZSklWPFFiTWdIbD9GYFlXOltwdEVNVXhyTmBNaFRQZEBMQGV2SnBNTnBTUl1RZEBKUGBQdkhKVGxvbGB0PWxxRGVrcURVY1FSXXRuW0BtVmh3Sm1TaGBtTWBqP0lqQDxtTlRyakFYd0xVdm1ZQUl2ZFVtbEFUWj1qZmR0XUxTTHVMYGhQanVuY0FqcnVLSkxvSnFqWFxcdkhNa0BYbVRUbVF4akxYb3ZFbkFkbV5cXE9SYEw9YXY+cEtsRW9yYHlPUVNmXFxtWWBNbURrVF1vRGRWcElUa0FZdVxceFNAcEZoU3BsTEhUUE1IcG9lcEdodT1JVWd0S0dcXGtqYW5xRW9PUVc7WFVRVHlwcFNuRG5tRXJDXFxya1lwS2hLSlFTTkRXTFxcWEBQd1NJdVNcXFVydVFwWHJKPUtlaHRkZUpoTVRAXFx4WnRuU2VQVWhTS3VVdmVZd2VxZnF1Rl13PFlrZF1RaWVWdVxcbHltUWJhS1tFeGBVTWxQT15hSkVRcHdFTVNIV1lRcV1wVHNdbVxcRHFZZW07PHQ8UVFOYWxWSUx5PFBmZVRSbXV2RVVnVEpfbXhZdVZiQXNURVNDUFVmeXI/VFdXbVd3ZVlxbFFiRW9obGpqXVF4bFFQSHA7TFdBUVNIQXQ6SXdaSWpmaGxEZW5qWXBFQXJPRW4+cHZTbHFLbEx5XFxwcHVKV1h5Pm10XnB5PmxYaGxTYm1KX11yQTxxVW1jZ1hzc2JXSVg/U3Zzc1hKWWJzSXJXYWdkZWhUV2ZHaVRyYVlaP3VvQ0NQZUR0c3g/aWVzYWdbTWc8bXU6U2NMWWJUWVJrZWlnT2NwQURFT1NOUXZvbUhKb3hfaXlwPUM8UXljSVZFY3NeT0NWQUJvdVRvRXNraXhuX0RNPXZzXWk6YWdIc2hwV1JKa3RSU2RsPUd0O0dkWUdtWWhneXVkSVhIb1VbY0VvT0JOZWJoa1lfdWR4a1diTWdqP0RXT2Z1R1VzUVleRWZ5P1ZIUWQ6bVVndUlWeVNJZ0k6Y3ZWR1dAV2ZEU3hpPWI/S0laS2RbV0RvT1hkTWlaX1RbV2ZbVUlRYUU8QWRORVZYd0dlV3RmT3JjSUhXSXduTVhQUVJAY3Y8WUlUXVJjQXVha1hiT1NNUXZAO2d1R1VzZ2RgZWRZQ0lFbWZFTXNLaXJYeUVoQ1ZTX1dFY1ZRQ2VFbWlTaVNiXUhUQ3JIQWhcXGFSbV9XX0liQFFJZk9TUnFDV11DZU1JYllEdG9kc0tkc1lXYGdzd290Y21UUmNIXndSWWtmb0VUPUNUP293cGN0a3V3PXViWk9Dc1VCRmVGYmFYPnNGYldYaEdHSklkcmFUPW94ckdJPnd4ZT13aGV1QldZSW1ZQktnSldDd1V0eENlWztXU19oWklneUNnRG1mV0tHQnNDR3VDdENTUlVCcU15SXV2c1FiQ1N5cFF3clFJVFNkSU1iWGdXSz90XWVmT3d4VWlicU1ZWlNmTXdlVUF4OllHZVtiT19mW0NCQU1GdndTbU9HPlt2XmVGRm9ZbFdDaUl4TE9JV2lVSElzQXF1T0dFZEV1al1Zdl1lPm9jc0dXO1tWWk11P2dTTEtmRFVFc1FYQltFOj1YcXdZaVdoWEdmWU1nSm9FW3dyQXlSWGl0WWFFP0FlUFV2OlNyZWFzRXV0Z3FYTT9nPHFZeXdTcWl2c0l5U0tZSltiT0tpZFtmQUFiWFNlT2l0T0llU0dlZE9Ub2VmWGlyU1lSTVlJSjtYeG1Ed2VZQkFyRkFZbVdGUnlJeEl4SUt5O3d1eXF5cVlIa2lZW1dpbXF3V1lpT2dkT1dmXVdGUWl5dHV0YVNEdU95S0lVT0tpdUF0WF9lVl9UZWd0V2NmaF9kdE1GPUt5a0VkPTt0T01XS0VnX2l2X0lkeDtkdEdmREV1TXdnPD1yXm9jVF1oYGFSRl1oeHlGRGVZYFNCdUlYWW1VTk9pUE1XcWtmc3NYT1FGZUlyRVlzRT1EUGdld09idllVYXFJcEN4SGNJTFNXRGVJRkN4Tll3ZWFTY0d1W2N2PF1GP0NFUj15Rz9FS3diQXlyQWF2SWVlQGF4bkN3eF9JZGNoWHN0QlVpUldnX1FpWFtYVT9oVl1UP2d5eHVZa0VYa3VZZFlGW3dndUFVST9kRkNkc1tISnlDZm1XaE1YX1NEZ1dYd2t2XUdSPFdjaEF2VmF1VmN1Rz13Oz1EUE1JTz13UHlWaGVoVFVVQ0F1RHV3YVloa0dkc2N3QFlDQXN2a1t0XFxpRVxcPWRyUXVvPWg+XXM9U1JsXWVoZWVkV2Vda2JnXUM/Z1JMa1VhSVhueXhfaXY/W3NMbUV4QXhBd0lWXWZ2d0duV3dGWUlPaUV5Q1Z0X0NCU0Noa3d5SVJcXD14ZGN2TUVyUVFkTHVmYXdmWmdkTD9YcG1YcF9kY3FpblF2RF9JUW14THNDbkFmbWFiP2lSc3FTdl10aXNVeF9zX0dEPVdGSG10ZFF3ZDtlX19GZl1XZl1lX01paVtYS1dzRnVYUEtYPltiX1l1Zz1XcVd1WUtoeGNEPlVYT1FXT0lpSnNnTTt5eGl5dWVmTEV3YWVpb1Npa0lnQlt4WjtDRXlIQXVYdVVZdWFJZVlUO3V0Vj1ybV90RXF4dlVFc2t3RUlnTFVVVVVVcl1TOj1VeEdnPHFWbUdZTVd2O0FSeWtiTD9YbVVYbU9kXXFpVldJTD1TZkFXTHRLQ1RXWkFzW2Vnb2l4ZWFpWG50P2lyPz55X0Bodk95bklnc3Zyd0dxSF91Qj5zdHBdblluUFhzTU5yTHh3XkdsXl5hR3liUj9nX05lQG5dWG5dYFdoVnlsTXZcXHRoeXNXbkFmYVteX2FOWkRodWh3cE9oeGNAaW5HZlV2aFFWYG1WQG10VVVob3FUXXlCYklSSmt0cllVXFxbaT95c11Zdl1ZWV9vaV9NWWRrYz1BZXVHVkVTRVVTRWdhc2F3aFxceVZLT1hKd3RVb3VYa3lKa2R2QXVhQ2RISVdgd2Y8X3haeWZJdWU6YUdfQ3ZteXZJSXVMXXZIYVVCeWNtSVNJS3k9PVVIPWc8TVlqa1ZdcUJsQ2dYT2NJO3NUY0dZY3NgVUhnV2RvYUR1d1RseUhMc3NUZVV0XVJ3b0dua1l3S0l0S1VKTUdzTWVcXGlWVmNpTGtHdFtJOll0TVl0ZmF3Zk14PElneF11bV9XRHVlP0VUdD10YW9WXFxxVUtrZE1TZlBxWHBtUGNkeFZgU2s9bEhpWHFoeXBYVVp0VWNETmFFbElgcUx0WE15bFllUmJJbVhcXHhEQHBWTFdIbW5cXGVQa21RT21XZk1PP3VzSUx1b0ltPmRvcGVxWHV1UlBPVXlzXXFSbmxvPkhwd1lNTXB3SURWa1V5UUV5XUlOc11wYXlxeGl4aWhuX2huc0FRPmVYWHRYXFxNWV54S1l0eXNVUGhgTV5EcVt5eGpAVWtwVG49WGo9UmV5cVN0dlJldUB5eF9xT2hdc0pxa0VlbVF4bFF4eXd5d3lVUTtdSlhtS1FQeEVpVU50b0REcVFdbWhmY1VPYXNuamVXZ2VXaG1DZ2l3PkVWZ29UZWF3ZmFzYUdIZ2tHXFx3dWlZdFc9ZnVFUmBhUnFpVnhtWXhlWG9lZGhhZHA9WXNxSURzZ2k/eGxdWWF3VFl5UnhPR15xV3Y/Vj5zQzppWWVnRkVTUl9ZVnRxZVFdYj9ZVj9bclhHZ2txY0FHeFZtSXNdeE9PUz9LWUpbSlFoS2dgb2ZAa29xeUpAblp5dUBET21Nd1FEa1N1eW5BbkFgam94cHF4TmpxUUt0U3NhVElpSmI9WEBRcDpZclZFcHV0UEJUcztkVGJ5VXRcXEtqTG5uaVJ3XU54VExqUXRXeHhLSVdObHBxQHhuSVludGprQU1EPVV1ZEtZZXhaeG0+aHB4cHFodHZoRXg+cVZGZUxuWU1eREs/ZXNQPHhPdUt0SVNSXW9EZE5WeGtKeFQ/dW1eRVdjRUtJYHBxQU48QExcXFBycjxWZHRRPVBNPmh4TXFLXUROPWRKW1hvSmFqW2BqVWlzTkl3Z1FOdUV5Z2BOYlByR2lzR112a1xcSj9sWGdZVWdwbG9tdW5NbkU8SkJUV05hWGZMbD90TU1hbVdobVtJUEhMS2F5dmFxWGlZUVVtcUFpTXhcXHlvZU1nSW88bU89cVJRbHhqRHJhXFxYcFB3U1xcUldAUTtAcFZBVGxRc1dweF08UnNtSlpVd2dobVJYbEJMclRkSllobFJ4VD9obUh1cml1bVY8WU1cXFl0XFxXeF15UXh4dD10YU1yXFxpdUBBcEtBdWxgVDpNTXJYd1NIdkxoTWlpeFp4dj5oVnh0dVFEWUY8akBlb1BVanNJampQVDp4a2Rha09hckJ5V0pgSlJ4eGtZd29RcUNlUWJpWUdlamxxdVxcXXNCXFxQaERyO21NPTxQRnBVaXhuRmVLUUlsU3luPlxcal9EVE9mc2dIdWZPdktmWkA/cjthXz1uZ3g/XltBW0l5cVt2eFdfX1VvblteaD8+dW92azpfeFp4eT5oYGJ2aWxpb1ZQb1E/YmA+bUdPY0dXZnA/Z0BpXUJWd0debFR5ZUdYeURgbVl4bV1JcD5ubjpYYlZocVh3W3huYUJWc1RQX15RXFxWdnFNVms7UG46SXZOUWB0cF1raF1ESXdAaVo8UVxcZFBbS09qPT5jallqPEl0PUhaS25kW3loTlhjaj9gRG9dQm9rdVl5dVFgbGBdPFBhbUlbXFxZaVhvZVhvXFx1d2JzQGRrYHRSb2FaaV5EQV9TSVtkc05bQ2tzRFFLRWFBZDtLeFI7QkNDZD5rZW1rREhdVVxcO0Y8UUdkPVNpc1M7SVJYU0JKd3JUU2NkQ01UcXVTTHNRZXZtZXZ2eW9NaXdwRVA/dEpCSUtoRHVjXFxuSlhzUkV3STxLRVFycHBsbV1sQkxxQUFKP0VqVW15YWFPU0l2Z1lQYlhYZEFwQlRvS0FXOml5QFxcdlJcXFZIVVhEPHRaVEp0cXBzVHNTeWxQcGxqPHJTPE9KXFxZdFVsYV1XX2BqW2RRWlxcb2xld11UdVNFTmFsUj5MbEZdS1JUSmFVeF9VS0NQcEdNU1I8TUZMckxodj5YUE1pdk5YbDo8UD9xTm1cXHJbUE9PUFM6SEpEQHB4QFBBRE9HSG1OPEpOeHBJUEtTdFdITHJkZFVPbG5kTG1hYXJ2XFxWV0VKX0lqRW1YcHRQcVR0ZElyOlROZEh2c2BsY015ZTxYcUFNXklQOmRWPXhTPlBsST13RFRUSWxqQj1VY3BzRERsQUFKUmxMQEhLXXRLW013O0FMQ1RbZk9oPHl1dklwbFFdUkZaOllnXnZvS2dgdm5bRF5qX3dtanB1Rm9pW0FdO0dpZ05eOz5mTFZcXHdIdXRHam1gdj1meD1XWnZxc2dwZEVYc25PcVdxZ3VuckNJc0NBaEF5W2hxXU1ubkVpW1JpWk1IdGpQWlpWZ3ZAcXJEV29DU0t3W0l2W3NXX0dZTGlTOz1VaENiRkV2aXB5cUF1b3FtUU1rUlhvV3RVVVFTR3FQVGRrXVhuXWxNUzxqdmxKOlFuPDxOdmBxdmBtWHBtQEVYQ1BvTFVvRGVZQmh3bnVVY3BWbnlveUV5RXlVbG1MQFFqamBuPWBPWnVZWXBXcmR1eXFrTF1yRFVqUXV0YU1QR3hVdlF2UTxzXT1KZkxqPUhVeWB5X3lPT1FNQ0Rqa21YVHlUZEFVY3h4ZHVYcXVwWXl3PUBwdmFQPGhwb0xxeWFYd3RrbURqW1l3REBTR3BQcVxcUXM8ak9cXFJnQGxkSHBTbFNxWHRpSGxhaXB0UHFUXFxMYWVqPD1VZVl3ZUlwOlxcWXNVc0Q8eXRYTkhRcXhwcUBZcj08TUBddGRUV3BseG95SkNxb1BdbGtNU2Q/W0V5b2dWX0xweWlGa2dAamh4X21YUFl4bVlIWENGOkFFQnF1QlF3QFlzOklTUUNFb1FodFtJdltCW0VZPHdXWXFpT1FXbz91Y01FXl9peFtXaXVXXUlHPFtjW0tja293YHdoTXliYj9ZXTtkR2l0eU1yRFdDWHdYTFlVO2NVWVFnT1FHVl9HOmFDdGl5eGFzRmFjdF1zXk1nVUFFXk93RWtEUXNET093X01oPEtpcDtIQG9FanNEcj9VRVFXYXdoRF93VltiX1lSSj1SY0dlTkdMPXl0Y1xcVFs8VkBUcXVYcUttcUdtUHVkeWhgdHVkTDxJWFt4dj5oeGpBeFpgdFZtVGU8bmVxVmdlV0d0c0w8Vjpkc2BVUHVQTFpYVztlWXhheVNcXGpfcVBcXFF2ZmhuVmxUam1vOjxyUmxXbD1tZFBUUXRMUTxOZnRLdlxcb3RcXFFmPHJHdEtlUUtYbFRSYWpPdExAbHFBXUtFPGxJeEtZbFFabGpPTFFbRUxQeGxRWFhyUHVlPVFfXFxKRkFqZmRTZ2BWb1h0SUVubnlXanltalB2YGB3VUVtZkB2W21WYG1KR1xceTpUUFp0eWJQVWdwUk9MalNcXFNvaG50aHVoPEtFWUx1PGttZHVZTFBeVXY7dUs8bE5LcVdxWG5AdVJjWVBXWXJjVE5FdG5QQFhjbEx0SXNnQG5BUFU8PXJqPHNYUU5hVHdkZFZnRHZMUHduTVE7YE9LPU9XUU1cXHFPXVh3Q0hRRWB1a3h4YnF0OjxtQURVV1BTX3hKUEl0Z0hyQT10V2RrdUlWZ2xOamhKbHVyYFVSQkVXO1xcVlxcTHdqVFRHaHNqRFJ5XFxvb2l4b114PVF4UHRKQXRKa2VuSHF1Pkx1dGhUZEhRcXRQUUxSeFRLWkRNcXhwcVh4bVl4Sz1NXVFWVm1TSHlwclh2YmVUZ2l3Z2lqXVlVP0BTUlVaSXd4Z2l3Z0FfTD9uUE52UG93Z0FxV294UFBkb2lqP2hqTVhsTUB0Zj5aSlZvQz5zVFZeVFFvP0lyRlhqWVZwQW5kXXBmbGZvUFd3W0l2Wz5yX0dyTkBkOj5aOj9lOj5aOj5eZkI6OzxaOj5cXFA+Wjo+Pjo8Sj5oSjo8SkI6QjpDVjs7QjpLOlpKcFp5WVpYRmt1RmVRT1pyT2M6Plo6PlpDZ2JIX2JoUGJaT0o6OjQ6XCJce1x9LSUrQU5OT1RBVElPTkc2Jy0lKUJPVU5EU19YRzYjJCIjNSEiIi0lKUJPVU5EU19ZRzYjJCIiIUYqLSUtQk9VTkRTX1dJRFRIRzYjJCIlK1NGKi0lLkJPVU5EU19IRUlHSFRHRjItJSlDSElMRFJFTkc2Ig==A colouring of a graph is an assignment of colours to its vertices such that every two adjacent vertices are coloured differently. Above is a colouring of the Petersen Graph using three colours.The minimum number of colours necessary to colour a graph is known as the chromatic number of the graph. It can be computed (along with a colouring using the minimum number of colours) using the ChromaticNumber function of the GraphTheory package.Since Maple 2018, the chromatic number function accepts a LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYlLUkjbWlHRiQ2J1EnbWV0aG9kRicvJSVzaXplR1EjMTZGJy8lJ2l0YWxpY0dRJXRydWVGJy8lK2V4ZWN1dGFibGVHUSZmYWxzZUYnLyUsbWF0aHZhcmlhbnRHUSdpdGFsaWNGJ0Y1L0Y5USdub3JtYWxGJw== parameter that controls how the chromatic number is computed. For example, by using LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYnLUkjbWlHRiQ2J1EnbWV0aG9kRicvJSVzaXplR1EjMTZGJy8lJ2l0YWxpY0dRJXRydWVGJy8lK2V4ZWN1dGFibGVHUSZmYWxzZUYnLyUsbWF0aHZhcmlhbnRHUSdpdGFsaWNGJy1JI21vR0YkNi9RIj1GJ0YvRjUvRjlRJ25vcm1hbEYnLyUmZmVuY2VHRjcvJSpzZXBhcmF0b3JHRjcvJSlzdHJldGNoeUdGNy8lKnN5bW1ldHJpY0dGNy8lKGxhcmdlb3BHRjcvJS5tb3ZhYmxlbGltaXRzR0Y3LyUnYWNjZW50R0Y3LyUnbHNwYWNlR1EsMC4yNzc3Nzc4ZW1GJy8lJ3JzcGFjZUdGUS1GLDYnUSRzYXRGJ0YvRjJGNUY4RjVGPw== the chromatic number is found by encoding the problem in Boolean logic and finding the chromatic number using a SAT solver. This worksheet describes how the graph colouring problem can be encoded into Boolean logic.A SAT solver accepts a formula in Boolean logic and returns a satisfying assignment (if one exists). See the Satisfy command of the Logic package for more information.<Text-field style="Heading 1" layout="Heading 1">Generating the constraints</Text-field>We'll use the Boolean variables LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYlLUklbXN1YkdGJDYmLUkjbWlHRiQ2J1EieEYnLyUlc2l6ZUdRIzE2RicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRictRiM2KS1GLzYnUSJpRidGMkY1RjhGOy1JI21vR0YkNi9RIixGJ0YyRjgvRjxRJ25vcm1hbEYnLyUmZmVuY2VHRjovJSpzZXBhcmF0b3JHRjcvJSlzdHJldGNoeUdGOi8lKnN5bW1ldHJpY0dGOi8lKGxhcmdlb3BHRjovJS5tb3ZhYmxlbGltaXRzR0Y6LyUnYWNjZW50R0Y6LyUnbHNwYWNlR1EmMC4wZW1GJy8lJ3JzcGFjZUdRLDAuMzMzMzMzM2VtRictRi82J1EiakYnRjJGNUY4RjtGMkY1RjhGOy8lL3N1YnNjcmlwdHNoaWZ0R1EiMEYnL0krbXNlbWFudGljc0dGJFEnYXRvbWljRidGOEZH where LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYlLUkjbWlHRiQ2J1EiaUYnLyUlc2l6ZUdRIzE2RicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRidGNS9GOVEnbm9ybWFsRic= is the index of a colour and LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYlLUkjbWlHRiQ2J1EiakYnLyUlc2l6ZUdRIzE2RicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRidGNS9GOVEnbm9ybWFsRic= is a vertex of a graph LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYlLUkjbWlHRiQ2J1EiR0YnLyUlc2l6ZUdRIzE2RicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRidGNS9GOVEnbm9ybWFsRic= to represent that the vertex LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYlLUkjbWlHRiQ2J1EiakYnLyUlc2l6ZUdRIzE2RicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRidGNS9GOVEnbm9ybWFsRic= is coloured with colour LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYlLUkjbWlHRiQ2J1EiaUYnLyUlc2l6ZUdRIzE2RicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRidGNS9GOVEnbm9ybWFsRic=.First, we need to specify that each vertex has been assigned a colour. In Boolean logic we express that vertex LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYlLUkjbWlHRiQ2J1EiakYnLyUlc2l6ZUdRIzE2RicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRidGNS9GOVEnbm9ybWFsRic= has been coloured with one of LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYlLUkjbWlHRiQ2J1EiQ0YnLyUlc2l6ZUdRIzE2RicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRidGNS9GOVEnbm9ybWFsRic= colours by the clause LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYrLUklbXN1YkdGJDYmLUkjbWlHRiQ2J1EieEYnLyUlc2l6ZUdRIzE2RicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRictRiM2KS1JI21uR0YkNiZRIjFGJ0YyRjgvRjxRJ25vcm1hbEYnLUkjbW9HRiQ2L1EiLEYnRjJGOEZELyUmZmVuY2VHRjovJSpzZXBhcmF0b3JHRjcvJSlzdHJldGNoeUdGOi8lKnN5bW1ldHJpY0dGOi8lKGxhcmdlb3BHRjovJS5tb3ZhYmxlbGltaXRzR0Y6LyUnYWNjZW50R0Y6LyUnbHNwYWNlR1EmMC4wZW1GJy8lJ3JzcGFjZUdRLDAuMzMzMzMzM2VtRictRi82J1EiakYnRjJGNUY4RjtGMkY1RjhGOy8lL3N1YnNjcmlwdHNoaWZ0R1EiMEYnL0krbXNlbWFudGljc0dGJFEnYXRvbWljRictRkc2L1ElJm9yO0YnRjJGOEZERkovRk1GOi9GT0Y3RlBGUkZURlYvRllRLDAuMjIyMjIyMmVtRicvRmZuRmdvLUZHNi9RJyZzZG90O0YnRjJGOEZERkpGZG9GTkZQRlJGVEZWRlgvRmZuRlpGaW9GaW9GYW8tRiw2JkYuLUYjNiktRi82J1EiQ0YnRjJGNUY4RjtGRkZobkYyRjVGOEY7RltvRl5vRjhGRA==. These clauses are generated by the following function:# Return constraints saying that each of the vertices 1, ..., N in a graph have been coloured with one of C colours
colourConstraints := proc(N, C)
local i, j;
return seq(&or(seq(x[i,j], i=1..C)), j=1..N);
end proc:Next, we need to specify that each vertex has not been assigned two colours. In Boolean logic we express that vertex LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkjbWlHRiQ2J1Eia0YnLyUlc2l6ZUdRIzE2RicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRidGL0Y1L0Y5USdub3JtYWxGJw== has not been assigned two distinct colours by the clauses LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYrLUkjbW9HRiQ2L1EmJm5vdDtGJy8lJXNpemVHUSMxNkYnLyUrZXhlY3V0YWJsZUdRJmZhbHNlRicvJSxtYXRodmFyaWFudEdRJ25vcm1hbEYnLyUmZmVuY2VHRjQvJSpzZXBhcmF0b3JHRjQvJSlzdHJldGNoeUdGNC8lKnN5bW1ldHJpY0dGNC8lKGxhcmdlb3BHRjQvJS5tb3ZhYmxlbGltaXRzR0Y0LyUnYWNjZW50R0Y0LyUnbHNwYWNlR1EmMC4wZW1GJy8lJ3JzcGFjZUdRLDAuMjc3Nzc3OGVtRictSSVtc3ViR0YkNiYtSSNtaUdGJDYnUSJ4RidGLy8lJ2l0YWxpY0dRJXRydWVGJ0YyL0Y2USdpdGFsaWNGJy1GIzYpLUZQNidRImlGJ0YvRlNGMkZWLUYsNi9RIixGJ0YvRjJGNUY4L0Y7RlVGPEY+RkBGQkZERkYvRkpRLDAuMzMzMzMzM2VtRictRlA2J1Eia0YnRi9GU0YyRlZGL0ZTRjJGVi8lL3N1YnNjcmlwdHNoaWZ0R1EiMEYnL0krbXNlbWFudGljc0dGJFEnYXRvbWljRictRiw2L1ElJm9yO0YnRi9GMkY1RjhGOi9GPUZVRj5GQEZCRkQvRkdRLDAuMjIyMjIyMmVtRicvRkpGW3AtRiw2L1EifkYnRi9GMkY1RjhGOkY8Rj5GQEZCRkRGRi9GSkZIRistRk02JkZPLUYjNiktRlA2J1EiakYnRi9GU0YyRlZGZ25GXW9GL0ZTRjJGVkZgb0Zjb0YvRjJGNQ== for all distinct colour indices LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYlLUkjbWlHRiQ2J1EiaUYnLyUlc2l6ZUdRIzE2RicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRidGNS9GOVEnbm9ybWFsRic= and LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYlLUkjbWlHRiQ2J1EiakYnLyUlc2l6ZUdRIzE2RicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRidGNS9GOVEnbm9ybWFsRic=. These clauses are generated by the following function:# Return constraints saying that each of the vertices 1, ..., N in a graph have been coloured with at most one of C colours
distinctColourConstraints := proc(N, C)
local i, j, k;
return seq(seq(seq(¬(x[i,k]) &or ¬(x[j,k]), k=1..N), j=i+1..C), i=1..C);
end proc:Finally, we need to specify that adjacent vertices are not coloured using the same colour. In Boolean logic we express this through the clauses LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYqLUkjbW9HRiQ2L1EmJm5vdDtGJy8lJXNpemVHUSMxNkYnLyUrZXhlY3V0YWJsZUdRJmZhbHNlRicvJSxtYXRodmFyaWFudEdRJ25vcm1hbEYnLyUmZmVuY2VHRjQvJSpzZXBhcmF0b3JHRjQvJSlzdHJldGNoeUdGNC8lKnN5bW1ldHJpY0dGNC8lKGxhcmdlb3BHRjQvJS5tb3ZhYmxlbGltaXRzR0Y0LyUnYWNjZW50R0Y0LyUnbHNwYWNlR1EmMC4wZW1GJy8lJ3JzcGFjZUdRLDAuMjc3Nzc3OGVtRictSSVtc3ViR0YkNiYtSSNtaUdGJDYnUSJ4RidGLy8lJ2l0YWxpY0dRJXRydWVGJ0YyL0Y2USdpdGFsaWNGJy1GUDYnUSRpLGpGJ0YvRlNGMkZWLyUvc3Vic2NyaXB0c2hpZnRHUSIwRicvSSttc2VtYW50aWNzR0YkUSdhdG9taWNGJy1GLDYvUSUmb3I7RidGL0YyRjVGOEY6L0Y9RlVGPkZARkJGRC9GR1EsMC4yMjIyMjIyZW1GJy9GSkZgby1GLDYvUSJ+RidGL0YyRjVGOEY6RjxGPkZARkJGREZGL0ZKRkhGKy1GTTYmRk8tRiM2Jy1GUDYnUSJpRidGL0ZTRjJGVi1GUDYmUSMsa0YnRlNGMkZWRlNGMkZWRmVuRmhuRjJGNQ== for all colour indices LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYlLUkjbWlHRiQ2J1EiaUYnLyUlc2l6ZUdRIzE2RicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRidGNS9GOVEnbm9ybWFsRic= and all pairs of connected vertices LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkobWZlbmNlZEdGJDYmLUYjNictSSNtaUdGJDYnUSJqRicvJSVzaXplR1EjMTZGJy8lJ2l0YWxpY0dRJXRydWVGJy8lK2V4ZWN1dGFibGVHUSZmYWxzZUYnLyUsbWF0aHZhcmlhbnRHUSdpdGFsaWNGJy1JI21vR0YkNi9RIixGJ0Y0RjovRj5RJ25vcm1hbEYnLyUmZmVuY2VHRjwvJSpzZXBhcmF0b3JHRjkvJSlzdHJldGNoeUdGPC8lKnN5bW1ldHJpY0dGPC8lKGxhcmdlb3BHRjwvJS5tb3ZhYmxlbGltaXRzR0Y8LyUnYWNjZW50R0Y8LyUnbHNwYWNlR1EmMC4wZW1GJy8lJ3JzcGFjZUdRLDAuMzMzMzMzM2VtRictRjE2J1Eia0YnRjRGN0Y6Rj1GOkZERjRGOkZELUYxNiNRIUYnRjpGRA==. These clauses are generated by the following function:with(GraphTheory):
# Return constraints saying that each of the connected vertices in G are coloured differently (using C distinct colours)
graphConstraints := proc(G, C)
local i, j;
return seq(seq(¬(x[i,Edges(G)[l][1]]) &or ¬(x[i, Edges(G)[l][2]]), l=1..NumberOfEdges(G)), i=1..C);
end proc:JSFHLUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYjLUkjbWlHRiQ2I1EhRic=<Text-field style="Heading 1" layout="Heading 1">Generating and visualizing queen graphs</Text-field>We now demonstrate how the above encoding is used to colour the "queen graphs". The queen graph LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYlLUklbXN1YkdGJDYmLUkjbWlHRiQ2J1EiUUYnLyUlc2l6ZUdRIzE2RicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRictRiM2Jy1GLzYnUSJuRidGMkY1RjhGO0YyRjVGOEY7LyUvc3Vic2NyaXB0c2hpZnRHUSIwRicvSSttc2VtYW50aWNzR0YkUSdhdG9taWNGJ0Y4L0Y8USdub3JtYWxGJw== encodes the moves that queens can make on an LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYnLUkjbWlHRiQ2J1EibkYnLyUlc2l6ZUdRIzE2RicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRictSSNtb0dGJDYvUSgmdGltZXM7RidGL0Y1L0Y5USdub3JtYWxGJy8lJmZlbmNlR0Y3LyUqc2VwYXJhdG9yR0Y3LyUpc3RyZXRjaHlHRjcvJSpzeW1tZXRyaWNHRjcvJShsYXJnZW9wR0Y3LyUubW92YWJsZWxpbWl0c0dGNy8lJ2FjY2VudEdGNy8lJ2xzcGFjZUdRLDAuMjIyMjIyMmVtRicvJSdyc3BhY2VHRlFGK0Y1Rj8= chessboard. The vertices of the graph are the squares of the chessboard and two vertices are connected exactly when a queen can move between the two squares in a single move, i.e., when the squares are in the same row, column, or diagonal.The following function generates the queen graph LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUklbXN1YkdGJDYmLUkjbWlHRiQ2J1EiUUYnLyUlc2l6ZUdRIzE2RicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRictRiM2Jy1GLzYnUSJuRidGMkY1RjhGO0YyRjVGOEY7LyUvc3Vic2NyaXB0c2hpZnRHUSIwRicvSSttc2VtYW50aWNzR0YkUSdhdG9taWNGJy1GLzYjUSFGJ0Y4L0Y8USdub3JtYWxGJw==:# Return the queen graph of an n by n chessboard
queenGraph := proc(n)
local label, N, vertices, edges, i, j, k, l;
label := (i,j) -> n*(i-1)+j;
N := n^2:
vertices := [seq(i, i=1..N)]:
edges := Array(1..n, 1..n, 1..n, 1..n, x->NULL):
for i from 1 to n do
for j from 1 to n do
for k from 1 to n do
for l from 1 to n do
if (i = k or j = l or i - j = k - l or i + j = k + l) and label(i,j) <> label(k,l) then
edges[i,j,k,l] := {label(i,j), label(k,l)};
end if;
end do;
end do;
end do;
end do:
return Graph(vertices, {entries(edges, nolist)}):
end proc:To visualize the colouring of a queen graph we use functions that draw coloured queens on a chessboard. The visualizations make use of the drawing commands from the plots and plottools packages.with(plots):
with(plottools):
# Return commands that will draw a queen on square (x, y) with colour c
drawQueen := proc(x, y, c)
return
ellipse([x+.5, y+.35], .24, 0.05, filled = true, color=c, style=polygon),
ellipse([x+.5, y+.2], .25, 0.05, filled = true, color=c, style=polygon),
disk([x+.2, y+.7], 0.03, color=c, style=polygon),
disk([x+.35, y+.725], 0.03, color=c, style=polygon),
disk([x+.5, y+.75], 0.03, color=c, style=polygon),
disk([x+.65, y+.725], 0.03, color=c, style=polygon),
disk([x+.8, y+.7], 0.03, color=c, style=polygon),
polygon([[.25+x, .25+y], [.2+x, .7+y], [.325+x, .25+y], [.35+x, .725+y], [.4375+x, .25+y], [x+.5, .75+y], [.5625+x, .25+y], [.65+x, .725+y], [.675+x, .25+y], [.8+x, .7+y], [.75+x, .25+y]], color=c, style=polygon),
rectangle([x+.25, y+.35], [x+.75, y+.2], color=c, style=line),
ellipse([x+.5, y+.35], .24, 0.05, filled = true, color=c, style=line, thickness=0),
ellipse([x+.5, y+.2], .25, 0.05, filled = true, color=c, style=line, thickness=0),
disk([x+.2, y+.7], 0.03, color=c, style=line, thickness=0),
disk([x+.35, y+.725], 0.03, color=c, style=line, thickness=0),
disk([x+.5, y+.75], 0.03, color=c, style=line, thickness=0),
disk([x+.65, y+.725], 0.03, color=c, style=line, thickness=0),
disk([x+.8, y+.7], 0.03, color=c, style=line, thickness=0),
polygon([[.25+x, .25+y], [.2+x, .7+y], [.325+x, .25+y], [.35+x, .725+y], [.4375+x, .25+y], [x+.5, .75+y], [.5625+x, .25+y], [.65+x, .725+y], [.675+x, .25+y], [.8+x, .7+y], [.75+x, .25+y]], color=c, style=line, thickness=0),
rectangle([x+.25, y+.35], [x+.75, y+.2], color=c, style=polygon)
end proc:
# Return commands that will draw an n by n chessboard
drawChessboard := proc(n)
local i,j;
return seq(seq(rectangle([i,j+1], [i+1,j], color=`if`(type(i+j, 'even'), gray, white)), j=1..n), i=1..n);
end proc:LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYjLUkjbWlHRiQ2I1EhRic=<Text-field style="Heading 1" layout="Heading 1">Finding colourings of queen graphs</Text-field>We use the Satisfy command from the Logic package which finds a satisfying assignment of a logical formula if one exists.It is beneficial to initially assign colours to as many vertices as possible. In the queen graphs all squares in the first row are mutually connected, so each square in the first row must be coloured differently. Thus when colouring the queen graph LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYlLUklbXN1YkdGJDYmLUkjbWlHRiQ2J1EiUUYnLyUlc2l6ZUdRIzE2RicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRictRiM2Jy1GLzYnUSJuRidGMkY1RjhGO0YyRjVGOEY7LyUvc3Vic2NyaXB0c2hpZnRHUSIwRicvSSttc2VtYW50aWNzR0YkUSdhdG9taWNGJ0Y4L0Y8USdub3JtYWxGJw== we include the constraints LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYlLUklbXN1YkdGJDYmLUkjbWlHRiQ2J1EieEYnLyUlc2l6ZUdRIzE2RicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRictRiM2KS1GLzYnUSJpRidGMkY1RjhGOy1JI21vR0YkNi9RIixGJ0YyRjgvRjxRJ25vcm1hbEYnLyUmZmVuY2VHRjovJSpzZXBhcmF0b3JHRjcvJSlzdHJldGNoeUdGOi8lKnN5bW1ldHJpY0dGOi8lKGxhcmdlb3BHRjovJS5tb3ZhYmxlbGltaXRzR0Y6LyUnYWNjZW50R0Y6LyUnbHNwYWNlR1EmMC4wZW1GJy8lJ3JzcGFjZUdRLDAuMzMzMzMzM2VtRidGQEYyRjVGOEY7LyUvc3Vic2NyaXB0c2hpZnRHUSIwRicvSSttc2VtYW50aWNzR0YkUSdhdG9taWNGJ0Y4Rkc= for each LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYpLUkjbW5HRiQ2JlEiMUYnLyUlc2l6ZUdRIzE2RicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1Enbm9ybWFsRictSSNtb0dGJDYvUSYmbGVxO0YnRi9GMkY1LyUmZmVuY2VHRjQvJSpzZXBhcmF0b3JHRjQvJSlzdHJldGNoeUdGNC8lKnN5bW1ldHJpY0dGNC8lKGxhcmdlb3BHRjQvJS5tb3ZhYmxlbGltaXRzR0Y0LyUnYWNjZW50R0Y0LyUnbHNwYWNlR1EsMC4yNzc3Nzc4ZW1GJy8lJ3JzcGFjZUdGTC1JI21pR0YkNidRImlGJ0YvLyUnaXRhbGljR1EldHJ1ZUYnRjIvRjZRJ2l0YWxpY0YnRjgtRlA2J1EibkYnRi9GU0YyRlZGMkY1 which say that vertex LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYlLUkjbWlHRiQ2J1EiaUYnLyUlc2l6ZUdRIzE2RicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRidGNS9GOVEnbm9ybWFsRic= receives colour LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYlLUkjbWlHRiQ2J1EiaUYnLyUlc2l6ZUdRIzE2RicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRidGNS9GOVEnbm9ybWFsRic=.The following code finds a colouring using the fewest number of colours for all queen graphs up to size LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYnLUkjbW5HRiQ2JlEiOEYnLyUlc2l6ZUdRIzE2RicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1Enbm9ybWFsRictSSNtb0dGJDYvUSgmdGltZXM7RidGL0YyRjUvJSZmZW5jZUdGNC8lKnNlcGFyYXRvckdGNC8lKXN0cmV0Y2h5R0Y0LyUqc3ltbWV0cmljR0Y0LyUobGFyZ2VvcEdGNC8lLm1vdmFibGVsaW1pdHNHRjQvJSdhY2NlbnRHRjQvJSdsc3BhY2VHUSwwLjIyMjIyMjJlbUYnLyUncnNwYWNlR0ZMRitGMkY1; on Maple 2019 this takes less than 10 seconds. Conversely, the ChromaticNumber function required several hours to perform these computations prior to Maple 2019.The initial call to Satisfy tries to find a colouring of LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYlLUklbXN1YkdGJDYmLUkjbWlHRiQ2J1EiUUYnLyUlc2l6ZUdRIzE2RicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRictRiM2Jy1GLzYnUSJuRidGMkY1RjhGO0YyRjVGOEY7LyUvc3Vic2NyaXB0c2hpZnRHUSIwRicvSSttc2VtYW50aWNzR0YkUSdhdG9taWNGJ0Y4L0Y8USdub3JtYWxGJw== using LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYlLUkjbWlHRiQ2J1EibkYnLyUlc2l6ZUdRIzE2RicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRidGNS9GOVEnbm9ybWFsRic= colours. If such a colouring cannot be found then the number of colours used is increased by 1 until such a colouring exists. The colourings are plotted using the previously defined visualization commands and by reading the satisfying assignment produced by Satisfy.with(ColorTools):
colours := seq(GetPalette("Patchwork")[k], k=1..8), Color("black"):
for n from 1 to 8 do
G := queenGraph(n):
N := n^2:
for l from n to N do
allConstraints := graphConstraints(G, l), colourConstraints(N, l), distinctColourConstraints(N, l), seq(x[i,i], i=1..n);
startTime := time[real]():
result := Logic:-Satisfy(&and(allConstraints)):
timeUsed := time[real]() - startTime:
if result = NULL then
printf("The %a by %a queen graph is not colourable with %a colours. Time used: %.2f seconds\134n", n, n, l, timeUsed);
else
satisfyingAssignment := result;
printf("The %a by %a queen graph is colourable with %a colours. Time used: %.2f seconds\134n", n, n, l, timeUsed);
break;
end if;
end do:
# Array to hold the colour indices of square (i,j)
ent := Array(1..n, 1..n):
for eq in satisfyingAssignment do
if rhs(eq) and op(0, lhs(eq)) = x then
i := 1+floor((op(2, lhs(eq))-1)/n);
j := 1+((op(2, lhs(eq))-1) mod n);
ent[i,j] := op(1, lhs(eq));
end if;
end do:
# Display a visualization of the colouring of queen graph that was found
print(display(seq(seq(drawQueen(j, n-i+1, colours[ent[i, j]]), i=1..n), j=1..n), drawChessboard(n), scaling=constrained, axes=none));
end do:LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYjLUkjbWlHRiQ2I1EhRic=LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYjLUkjbWlHRiQ2I1EhRic=