Solving the World's Hardest Sudoku Curtis Bright, Maplesoft TUZOV3RLVWI8b2I8Uj1NRExDZE5GWkpsOj5bPEo6eGpoQXRHQz9xUkxDVEpjRFhvWHV1eGxdZXJTdEBHQk5hZFdfcmZxRkdzbnI8S1xcTW92RXVyXFxKdUBVTGVyQElVclVQVXRWWnhRO0xQU3hVRnRNQk1yQnRTcVVTZEVqSFlxVWxQdGBxSWFNcXVwVD1YbXlSY2RuaFxcbmhddTxkbk48cE5QVEQ8VURFT1pFT19gTGo6Tl9leXZJeW1xTmNjZmxjcGl2QXlLYl9xWWNjZmxxVGo7VVNzQnh1WHF1WFl3ZVlHaUhvVVhLaXZDYlZXdlh5aW95aXZlWHVVWXVxeXhxZWVBd19JZkVZREJBWXNReHlrYnZZQkU7VTpRQlA7aG5bQ1I9ckx3WVpFQkU7VTpiOmdCZjtWO1NTPUFiP1tHc3lCUDtoOlpaO19AOko7OlU6eFFYPXB4dXl0TFk9SHhReVdHVEpQPHBeeVluPVZnbVRtcWxRcW89SXRMQVBaRUpFTmk+Vm9XWG9nZ3NRV11HVlpQWl4+Zk9hcWRIdk5nY0pWWj9RdGo+RlFqeEFydDx0bl1Qd1lXdWFVPUFqP1xcT3M7PFY/XFxzQ1RPVFBvSWFvW0VKRTxVbF9iWmdtVW9oSWZ2RFdyOmhaZj5mb2FbUFdoT2hhWFZfR1Y6dnFxP3B4UGZPdnFLVmM9QWo/WkJuZD9pdGNoYGZAZGxgYEY+ZTpRWlB3aVpHaUQ/W2Y+ZjtaPG48O1ZvZUNQZ2VoQXI8a0Rqb0dhZUNFWWk+P3I8a0RqXFxLUnVZSGFRYFxceGdlSzpRSlBgeUloS2ZYVD1kb3JoV1JNTUBcXD9nUGpgUEY8VTpRbHk9VjtUO0VKakA6REpFVXI6aFpsPT5SZzpGZ1I6OkY6RElVcjpyQTpFV1I7UEVteWl0SmZYcXZlVFhkWXBUbV9RUXRFWWJhd1F4VVBpV3hQdVd5eVZ1UllpdXlhcVF4T3lJdW15TUZsdGFtcWR0V1NZd2VZV2hYbml0bEVReD5MUFhteWhxeXl4dmVQeGx5TVl0TW1lTXdJd2NJb3ZEakZ4bGl2ckp4aU1PYk1PYk1bZT9lVG5aZmpZPFU6UTpCajpqO2hKZjpFOk49Ojo7QFBEOlpPcHRqeHV5cGdkZ2BZZ2dAeFplQGVpTndhQXBSd1xcOlFaUEJHU0lJZ1RMS1VrPVZPY3JBWXN3SWdtPVVmR2I/W0daRW9pRXFEYE5lbEtmcHZKUXdgZFZWaEpmRGlmWGdoP2VfaXRpeHV1eGNwVm9zX3BSR1xcWmd0QHdkcXlfWWZya0ZmO1hqZj5mQ01RXXVqWGpRZVhWcEtZbHdHVHdNXFxvPXhUb0lyTmVTa1B4XVFKUj1yPGZbZUdvPUFcXGU/bEtudHg/YE9uWk0+cDpoOl5zQlZqQXlkW0FmT1dzZ2l2bj9wa1B4WGdjSUZqP14/TUVwaXN0WVlWcXNAP1hqb3NmO2lpRXQ8a0RqVFM9cXFTVFU/VWxPaU9SbW1MTEpFPFVUbHRdYW9qREtmaHdmPHBybHVQaHZjRE5qQGpfTmlUd2hJeGU9UWdoTmVzT2NCam5cXE9cXEVRZVxcV0ZobDpsVD1sblRBc0U8VTpROnFjW01XSGNmXFx1Rj9HQ1VRRUY/aDpnQmZseElRVk9Bc2RoUWdcXEtWXXJESHVjcVVnUFZ3eVZQaEBqT1RvPXhwQ1RWOlFXdVV4c0xXcWxMamBGbHVqWG5nYUtrWG5lQFNqcHNmbVdqeEtFPFU6c3lbQ25PVnk/RGVjdnVBaFRXQmc/c3FjWDpnRnlBckxBaFtodENFSkVtSTxCbXk7Z0JmO1Y7PGBSOkRXUnJMd0FAOm86TWBuXjtEc3k8cDpoWjpdO0JQX1FQOnlTPVN3bXNVR3FWbXdocXdoVnVSWW1HUWd2Q1tWdl95V2l5eXVzUWV2X3lJdltJXlFJdFl4bVlYc01CU2xxdnlrW3R5O0FWV2l2ZVB4Yml2Z1Rzb114bEF0U3lPeWBvVWFZb1hxeUlxSHBxdXh5c3VPWW15bXh2WWFsSmFsSmE8UE1QcGo7akliOmdKOkNSQmpfQDpKOzpVOjpKalpMPTp2XFxEbmRteXhQWGx5b19YUlY7VT9FaFhddW5rWXBNWWw9VmdtVG1hZF5JQkU7VTpRRUBbZ0l3ZHVZVHFtWWtvR0RHYzpndFRPcmpdaDpnSGM9aGBZZ0dHR1t1Z1plRGdbVWdVd3hpdl07dGZXYz5Td2ZtQj1VREJbZ2NpZ1tlRTxbRHh5eEc7VVs/Vk9VVDtpSUlleGNJVnNLc3RvWGpPV01FclRtdWRbcjxjcjxrdE5BckQ9dkQ7VTs/Vk9hV1RRWG9NVlJpRHI/ZW9FYlplRWxxdE5HZ2xdR2ZzYjpRZVA7VUNdVTtTR1hbZ0BRY09leHM9dmY/eERvZUxrUmBDRFJVVDxTd2p5VmdbWF9BQlJlSUc/aGBTQ1Bdd1ltU1plU0JbZz5Jdk87aHRLVT1RZ2lXckFnSWVbaVA7aGRnRmY/dGJLQmVNSFplRklzZzpnRG1hZGpHaTtTR2tVWD1pVDpnVFVtYklzY1xcO2hgT0JQdURYRUJlV3J3PVVNYUJlb2lBSUZgPWZJW2dDP2JPSWNRPXJEZ3VjcXU6VWdWX0VoeXl3Y2dvW2dUb1RrR0g+a3RuO3JkcXJlO1ZvVXhoQ1ZvP0V5ZXlVUUVIRVdPY2lAT0NmR2c6Z2hJVVNUd1Q6UXdiSUdbZVdRVXJuaEx3SFROPFVNYEplZHlzQU5qUG46V21EbndBVmRveHNUTmtHT3ZXT3I+YXk7VmdUPmZvX2BbXlpQd3BJR1s9eXFtSHZ0cXVfXnBrX1xcUndmOlFjd1laQV5vQmhgZlh0XmdqeUh5dkduWmdpcWlqWz5yPG5kWVdgPD9mP29fdHhgcW9gPnZzPnZvXFxpZTw/ZjtWZ2RoW3VgeGFgaktpdlV2Yl95XVI/Uj5qX0RqVFN4c2paRUJqP1puXjt2STo8cjxsPFF0ajtec106TGpWO0pUWnlJcjpRZERHb1ZnWmZmbk5peDxoZkRPZkRPZkRvX3lZbkR5YWpASmBpUHBqO0pzQ1JCal9QakBaeFVjPUVqPzpRSlpFOlp5U1RrOk46PEJVOmJARzp5SWs9aERvdkljZlFRV2tvR0Q7bmQ9cHRseV9AWVpFSmV4WWpwdEVYTVpFSkVSV11SPVFVQTtVOlFldjtVbWl0QGFkSnBSTkFwXFxwUFtcXE93TXBAaFZHVG88XU9mXVg/XFxPWmVLO2x0W01Scmd2PT5lOlFjWlFbUj9yZGldZlBzZVh5VGFzak5cXGk+ZldPYVJHY1ZHWkU+ZXd3YGZoaTtWZ0VwXFxqcG4/bnRgZ2BJWGV1UFpQYltNRVBReT4/SGRdZT9bZ0VvQmVDWHJlQmY7Vm9ZdWpPdTxrVG9rZWR3WXJVaFJVQmVNR1plPmdCZl9JR1NnWF9FaHVyUmVCam9mOmtUUWtNUDxwbEBqT2VLbFBycFBWO1R3XFxFcmRhcmU8VjtCWmVLZnBXdlA6VUJnR1Zva3RRWWVZU0JlTUJaZXdRWXVNYWk8a0RqYHVqcHI8VHlZVW1IbW8+WUplUXE7UVN5bVFCXFxPWmVLS0FwXFxhdXhwSmlRTEhdSmZwa2BcXGo6UUpQQUpHVFdTWVFUVHBTaU1SdUxIbFRcXEFKRTxVOj9jPXFreVBcXGU+aGNRW1J3XFxIbmRRV2A8P2Y7VmM9VUdjaE1pSXdfdlk7PTtueTtFOl5Wa2RAalk+aj9CUj1yTGZaZkZZWmw9UUpaRUduWUpFOz9ib2NFam9XbWlUc114U2FXUFd3Yml2W1doWW1ZU3VYc1FXcXV5bWVFd3VYeVl4WG1pdnlWSXlZajtVaUl5ZF9pX3VjSXdjc29rY1dEcllpdXl5c3ZlVFhteWVZd2VtZ113R1FXc2xhQmxrVXhfeUlHRnlxZj5vZj5vZj5OZT1RdGo+Rjo6bjxjOzo6TEg6TD1ESkVVQkRpZmY7WjplPzxyTGN0Q0JlQ3dRVXZdQ3JUYWdgeUhhU0dyYUU8VXhZXURlaXJHSXlUXWdFT1J4SWI/VFY+VHc6aXRaQFZPcWtEXFxPWkU6P0Nya2I9U2dvPWJvS0Jqb3dZbUleeUVSPXJUQ0ZSdVJdYWU7QXJkX2lER0ledUNzeWdKU1VmZ3ZZO1U6bFJqcHFGVXNAVEplQVheSXlkVWxZXFxvXFxwc089c149VHhJaj9WYjtocEFXZnhQZUdmcWJxZXNnYGloc0ZWXmtRY0l5aVdYX3N5WlBiS0tiT0VQbTx5TU1ycGlKZkBNblBMbXlVdl1xVnlNUHFvRDxWO1RbQHlaUGdtZUh2cWhgbnBhW15rXFxWX2t2eUNYcmVGeUFKd1RqT2F2ZD1YalBPaVBXcmRyaW1vQkVzeU15alFTeElqP2ZxPGh4T3huVlZdQXdzRl9cXD12clJHX3N5b3VnXnlBUmdIdDtoSEV2bmtDak9WSVVGdHN5P1VYdmVGeXJSQXJ0U2l2XURfaXI/U2JPaXJ2PVR4SWI/dHRHbFRFcU5mQHV3SFVrQVZneXRVWVRgWWpseTtvZ3ZdYm9NVztneV5RU3Z1aVplZnlzRU53WVpFQmU9c1FVWGxjZ1tlZV1VaHF5WENTaVc9ckx3cTxWZ0FWb293d2Jfc2B3eF4/cFxcb2VBSWx5P2Y7Yko7VWE7dERnWWc/SFBbZ153eEFjdlk7VTpRcz9rVExFeUBJPEQ6Oz4/SnhXQ1pQQlpFQkU7VVRrOk5UOlNrOmJAOlpQcEpRSnN5cXY9cFhZaFNhZ3BBeGpBTFpDQmlzYXlhc1Fndl95cXdocV9RYXRRaHNgX0k/Xl1pVk54WV5bUGlneFBfSXBlWFFwVndiaXZbV2R2UWhoUXhPcXd4eXZ0S3locXlhaWl2RXlJcWV5VVQ8VVQ8VTxVV1JNRUBbPzo6Tj06Yl5GWkVidlk6WlRaO1ZjPV1zZV86PGBFQmpfSGZRUzpRdXlReGxdc0lzRz1TdzxVeFlleWxheFlRaXlFeTpOcT4+cEh2YU52W2ZIczpodD5Rb0BwZEs/WkU+ZV1uWmVQdEQ+ZU1HWmVAYUdpZF5BYUVCam9iO1NXbU9lWWNyTztVTT9CZU94ZEVoWGlZbEl4bHVFdztzPGtEajxKUFVWXmVKZkh3OmhUTlV2ZWhPSHVVeFxcVWZIaj9cXG9rUWpvdFVnTU92QGpvRHRhYGo/SVZCaFY+aEpmSHA8aHBvUG9zTHU8bHRORHJkTE9ocHBdWU9lP2pvTnY/d2haZ2NVXm90UXl1X3VIcVpaR1pFPkVEbHlReVJRd2JlVEU8VTpRWlpna29nW2VGZlA/W2Y+ZjtqW1h4WWRxaHFLZjxWO1RbQHZaZW5oYVdaakBKZnhPeHlNWHlqUF1dXl9aRzo8ZklveWV4Xj1YeVN5ZUt3aVV3ZnloeVc+RWJ2SXl5U3hoQ1Y+WWI8PVY7U2s6aHRpbXlJcHBtXFx0QHVUcGhgUD5wOmhgeGB5UXZleUBcXGVeeXVoZjpoWmZIdjtRY2c+ZkN5QTpaPG5sQFxcbG1ASmxDalRbOmhOQnlBaltrdm88O1Y7PHBuOjp3QUBqb0RMamBsTE1PUUVKRUVPb2VxWkVtTEBtTEBtTEBzeW1vdlk6am46REpFOj1yPDxmUHBKTlg8QDxmUDpgQDpaOzpnPkRpZkhscV5neVlka0lseWBcXEleX1pnYmB5aVlgcU5geT95dnlIaW5Bd01ib1tHUmVUVUFaQFZzeXFmb3Zhb2luQUZ2U15rRHlpRUl0XXBDa3Q6P1Zva3lCQUJFO1U9Y3Z5WXNacUZ4Y2JLQ3lpdXZkVW1lPmZHQFxcZnhvV1daUGpeeXFEcFU/WFJuQVJ5XFxReWlwXnl0ak1vSD1OSl1PWj9aZlhseUd2OmhaZkhebHlpOlZuSz5xREhsamBdQHh2eUFcXHhZbj1mcHdvW2ZIeDpocHdZZkxGdWE+ZjtWX2h2eUN4W3M/am9mY2pwWz12ZVpzVEtIeVl5W19UU2hrX0VrSmlwXXBPUEFwZEBzWVBtYFBKZV1rSUVLO3JaR3l5U2hacUU9b1RBeVNDU3JJQUJSPXI8SGs8aFBGWVQ8cXBtQWtVVHY7VEtSPXJUcEpSZWxKZHBbdFNpeVNDdHluTXFnUEpSPXI8bHRObHRqcGtAXFxQPWlRX1xcUXNoalxcbFVGPVY7VFtgQFpQd2BJRnd2Zl4+SjpRd2t0eW9pUW9EUUA9VTpRSlByREdlTGdFRlFFbGVDRXFTcT1WO1NrXFxBc0JtWUx1dldNUlpFSkVOeUh5eWN5dm5XYmdZcmR3aUY/d1VFWmxcXHdZckJ3XmxuaWtJeXluXWJnYmhncEFudDpBZl9wXFxqQGpfOjxyPGY7XlY6PmY7Vjs7aG5bW0U7Wjw6cDo6Wlo7X0B2ajtWd2h2ZU94Ylloc2BHcUhwZVhOYXVpdlFoaFV4b3B3eHl2dEt5aHF5YWlpdkV5aXBheUFWam9JbWlQc1VveHRReVRYd2JZc19RcHZGakZ4bHlYcXl5d3NRb3ZgeUF5ckFhZUF3aXRPaWR2Y1pWVmpxZE5uZE5uZD5wal9IVjpTeD5wOkxqWjxKVDpWO0o6W0VXUkZZWlpzPFpuOjpibm9iV2tZXW9JZ3lyPFl2OlFHeGtVaHlXSG10XFxlVU47clRvQ1JVeVJrQ3hZVG9BcnRfRWpvSGVYdFRdUj5xTkxcXG9vUXZAPFU6UW94UVc8VFs8SHFUcXR2Z3BTQmVnWDpnQmZHdzpndFJTdj1TQ1J1dXRlVD1JZ0RzU1o/VUs7Vk9jaENDVmNZZG9bZ2NJYm9peElvRmo/Ym9pc1lpaF0/Y25nWVh5QlJ1YkNDdndZc0E7aGBvQlB5ZE9ZVFpFQmVddFplVFhldVFxVkBHZHJFQmVRVDtRdUhndl1TVEFbZ0NtZ1tlVFtDZ3hTRVplQ2VnWTtTV0VvRGpvRjprdFtjVjpRQlBNc2xXWWJzVEs9Vm9vSVtbY1RzVjtTd0xXeElbR1plcmhbRj5XVk9TQlBlVztTZ1RzU095SXZHVWZHYj9CZWF5ZHdWXm1XdE91Y3FVd0NJVnFja09DWkU6UVdsZVhkZUtiTVh0VEplUE1eZWpnZXI8bExqVndESHJEeXlOQFxcUj9Sbl89Xm9waGNSZ3NJSGo/Xj8+Z3B5bGN3bnVXZjtoeWloY2F2ZFxcSWo/Xj9obHlpVTxRdlZxcUBmXj5uPDtWb2dndXdWdHFoQG9kd1dma1NlV0liP1tvdFBYanBTR1xccFxccXBbZXJpTHFZdFlfbFRaUXRPPHA6aFpNT1plWHRAaGZ2eV1FXl9zeVpQXFxST3hJXl9aR1pFQmpfQHR5OlFkOlE6c3E/PnI8SlQ+RVJUOkJaRUJFVTpiQFJseWVAa3RhbWlUZ3NgdVdpdVdzb2N4X01QPj54WHF5eXd0VU94bHlBeGpBbGVBd0l5c0lpdkNcXEZuSklqdFhzUWV2S1lzVW1sZUF3X0lubXhVeEVVcUh5ZHVYeVlYV2RZcXV5bXFVeGB5YXVzeUhPW0hfTVtlY0BqWT5qP0JSOmZuWzs6ZjpKRzo6PlJSYzo6V1NBU2dzWVhrSWR5W1lFW0daZWZheUljeXZRR2JvZXlaZUV5UVN2TVJWPWI/W2c+YXlRcXlsTUJFO1V5YXNPcWhgWWdHO2g6Z0heO1VHR2J4O2g6YFM8TU9YUG9JUVJdVEpmPFZfXFx2eUhxaERKZjxWb3hSXkhRVFBRRlRxPFRQPVxcX0Rwc3lJXFxRP3I8bnR5eF9qb3d5dltWaFxcPFZbUkdsc3lvTHZwbEB3SF5vUklcXFA+cDpoYD4+ZW95YUpwbUxOWmVeZ0dWb3h0QWdiQDtVOlFjQnlZbV1JSVtHWmViZl9FXl9nXTtCRTtVO0l5eWtVeD1CUDtoSHF0U2djR2had1Zqb2lsYT5mO0I9VWd2WVRxd3lxZ0hmO1ZvSUNQSUdWP2I/W2diaVJKVXVUO2JPWUZSdXVmd1I+XVJKO1VNX1lEPUVzV2c7Oz1keFJBcFRhVGpBTEZQd21AdnFVWDpoWjpRWlB3bUdWYU1IbWppQDtVOlF4Z2VDOlF3cUdWYUdzRHNZbUlFUj1yPE5dXFxUbXVWPV1kTz1yPE5aUHBKUWVSO1VseTs8YEVaUEJaRT9sSTpFOk49OmpfSEZTU3hUQ1FKc18/aFo6UVRieVlzOlNTY2NmbGVUOjtVeXNZeGFYeV9kTEVpZF9GYjtCZmNmTk9FW0VCRUVHP1tHX2RKZmRuTjxwTl48WmNIb095eTt2ZFhwbElXaXJwXlhEOjtCOk1US1dES1dnSjtlWjE6XCJce1x9LSUrQU5OT1RBVElPTkc2Jy0lKUJPVU5EU19YRzYjJCIjNSEiIi0lKUJPVU5EU19ZRzYjJCIiIUYqLSUtQk9VTkRTX1dJRFRIRzYjJCIlK1NGKi0lLkJPVU5EU19IRUlHSFRHRjItJSlDSElMRFJFTkc2Ig== Sudoku is a popular puzzle that appears in many puzzle books and newspapers. Given a 9 by 9 grid whose squares are either blank or contain a number between 1 and 9, the objective is to fill in the blank squares in such a way so that each row and column contains exactly one digit between 1 and 9. Additionally, each of the nine 3 by 3 subgrids which compose the grid (called blocks) must also contain exactly one digit between 1 and 9. The mathematician Arto Inkala published the "world's hardest Sudoku" (shown above). The puzzle has been estimated to have a difficulty rating of 11 stars, whereas the most challenging Sudoku puzzles that are usually published are given a difficulty of 5 stars. Using Maple's built-in efficient SAT solver we can quickly solve this puzzle without any knowledge of Sudoku solving techniques. A SAT solver takes as input a formula in Boolean logic and returns an assignment to the variables that makes the formula true (if one exists). See the Satisfy command for more information.

We'll use the Boolean variables LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYnLUkjbWlHRiQ2JlEiU0YnLyUnaXRhbGljR1EldHJ1ZUYnLyUrZXhlY3V0YWJsZUdRJmZhbHNlRicvJSxtYXRodmFyaWFudEdRJ2l0YWxpY0YnLUkobWZlbmNlZEdGJDYnLUYjNiotRiw2JlEiaUYnRi9GMkY1LUkjbW9HRiQ2LlEiLEYnRjIvRjZRJ25vcm1hbEYnLyUmZmVuY2VHRjQvJSpzZXBhcmF0b3JHRjEvJSlzdHJldGNoeUdGNC8lKnN5bW1ldHJpY0dGNC8lKGxhcmdlb3BHRjQvJS5tb3ZhYmxlbGltaXRzR0Y0LyUnYWNjZW50R0Y0LyUnbHNwYWNlR1EmMC4wZW1GJy8lJ3JzcGFjZUdRLDAuMzMzMzMzM2VtRictRiw2JlEiakYnRi9GMkY1RkAtRiw2JlEia0YnRi9GMkY1LyUlc2l6ZUdRIzEyRidGMkZERjJGRC8lJW9wZW5HUSJbRicvJSZjbG9zZUdRIl1GJ0ZqbkYyRkQ= for LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYuLUkjbW5HRiQ2JVEiMUYnLyUrZXhlY3V0YWJsZUdRJmZhbHNlRicvJSxtYXRodmFyaWFudEdRJ25vcm1hbEYnLUkjbW9HRiQ2LlEmJmxlcTtGJ0YvRjIvJSZmZW5jZUdGMS8lKnNlcGFyYXRvckdGMS8lKXN0cmV0Y2h5R0YxLyUqc3ltbWV0cmljR0YxLyUobGFyZ2VvcEdGMS8lLm1vdmFibGVsaW1pdHNHRjEvJSdhY2NlbnRHRjEvJSdsc3BhY2VHUSwwLjI3Nzc3NzhlbUYnLyUncnNwYWNlR0ZJLUkjbWlHRiQ2JlEiaUYnLyUnaXRhbGljR1EldHJ1ZUYnRi8vRjNRJ2l0YWxpY0YnLUY2Ni5RIixGJ0YvRjJGOS9GPEZSRj1GP0ZBRkNGRS9GSFEmMC4wZW1GJy9GS1EsMC4zMzMzMzMzZW1GJy1GTTYmUSJqRidGUEYvRlNGVS1GTTYmUSJrRidGUEYvRlNGNS1GLDYlUSI5RidGL0YyLyUlc2l6ZUdRIzEyRidGL0Yy to denote that the square LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkobWZlbmNlZEdGJDYlLUYjNigtSSNtaUdGJDYmUSJpRicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRictSSNtb0dGJDYuUSIsRidGNy9GO1Enbm9ybWFsRicvJSZmZW5jZUdGOS8lKnNlcGFyYXRvckdGNi8lKXN0cmV0Y2h5R0Y5LyUqc3ltbWV0cmljR0Y5LyUobGFyZ2VvcEdGOS8lLm1vdmFibGVsaW1pdHNHRjkvJSdhY2NlbnRHRjkvJSdsc3BhY2VHUSYwLjBlbUYnLyUncnNwYWNlR1EsMC4zMzMzMzMzZW1GJy1GMTYmUSJqRidGNEY3RjovJSVzaXplR1EjMTJGJ0Y3RkFGN0ZBRlpGN0ZB contains the digit LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkjbWlHRiQ2JlEia0YnLyUnaXRhbGljR1EldHJ1ZUYnLyUrZXhlY3V0YWJsZUdRJmZhbHNlRicvJSxtYXRodmFyaWFudEdRJ2l0YWxpY0YnLyUlc2l6ZUdRIzEyRidGMi9GNlEnbm9ybWFsRic=. We'll also use a few simple functions to compute the set of variables which appear in the same row, column, or block as the square LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkobWZlbmNlZEdGJDYlLUYjNigtSSNtaUdGJDYmUSJpRicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRictSSNtb0dGJDYuUSIsRidGNy9GO1Enbm9ybWFsRicvJSZmZW5jZUdGOS8lKnNlcGFyYXRvckdGNi8lKXN0cmV0Y2h5R0Y5LyUqc3ltbWV0cmljR0Y5LyUobGFyZ2VvcEdGOS8lLm1vdmFibGVsaW1pdHNHRjkvJSdhY2NlbnRHRjkvJSdsc3BhY2VHUSYwLjBlbUYnLyUncnNwYWNlR1EsMC4zMzMzMzMzZW1GJy1GMTYmUSJqRidGNEY3RjovJSVzaXplR1EjMTJGJ0Y3RkFGN0ZBRlpGN0ZB and concern the digit LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkjbWlHRiQ2JlEia0YnLyUnaXRhbGljR1EldHJ1ZUYnLyUrZXhlY3V0YWJsZUdRJmZhbHNlRicvJSxtYXRodmFyaWFudEdRJ2l0YWxpY0YnLyUlc2l6ZUdRIzEyRidGMi9GNlEnbm9ybWFsRic=: rowVars := proc(i, j, k) return {seq(S[x, j, k], x=1..9)} minus {S[i, j, k]}; end proc: colVars := proc(i, j, k) return {seq(S[i, y, k], y=1..9)} minus {S[i, j, k]}; end proc: blockVars := proc(i, j, k) local block_x, block_y; block_x := 3*floor((i-1)/3)+1; block_y := 3*floor((j-1)/3)+1; return {seq(seq(S[x, y, k], y=block_y..block_y+2), x=block_x..block_x+2)} minus {S[i, j, k]}; end proc: allVars := proc(i, j, k) return rowVars(i, j, k) union colVars(i, j, k) union blockVars(i, j, k); end proc: LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYjLUkjbWlHRiQ2I1EhRic=LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYjLUkjbWlHRiQ2I1EhRic=

To encode the rules of Sudoku in Boolean logic we want to encode both positive and negative constraints. Positive constraints say that each square must contain some digit. Negative constraints say that each square cannot contain more than one digit and that squares in the same row, column, or block do not contain the same digit twice.

For each square LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkobWZlbmNlZEdGJDYlLUYjNigtSSNtaUdGJDYmUSJpRicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRictSSNtb0dGJDYuUSIsRidGNy9GO1Enbm9ybWFsRicvJSZmZW5jZUdGOS8lKnNlcGFyYXRvckdGNi8lKXN0cmV0Y2h5R0Y5LyUqc3ltbWV0cmljR0Y5LyUobGFyZ2VvcEdGOS8lLm1vdmFibGVsaW1pdHNHRjkvJSdhY2NlbnRHRjkvJSdsc3BhY2VHUSYwLjBlbUYnLyUncnNwYWNlR1EsMC4zMzMzMzMzZW1GJy1GMTYmUSJqRidGNEY3RjovJSVzaXplR1EjMTJGJ0Y3RkFGN0ZBRlpGN0ZB at least one digit LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkjbWlHRiQ2JlEia0YnLyUnaXRhbGljR1EldHJ1ZUYnLyUrZXhlY3V0YWJsZUdRJmZhbHNlRicvJSxtYXRodmFyaWFudEdRJ2l0YWxpY0YnLyUlc2l6ZUdRIzEyRidGMi9GNlEnbm9ybWFsRic= appears in the square. These clauses have the form LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYxLUkjbWlHRiQ2JlEiU0YnLyUnaXRhbGljR1EldHJ1ZUYnLyUrZXhlY3V0YWJsZUdRJmZhbHNlRicvJSxtYXRodmFyaWFudEdRJ2l0YWxpY0YnLUkobWZlbmNlZEdGJDYnLUYjNiotRiw2JlEiaUYnRi9GMkY1LUkjbW9HRiQ2LlEiLEYnRjIvRjZRJ25vcm1hbEYnLyUmZmVuY2VHRjQvJSpzZXBhcmF0b3JHRjEvJSlzdHJldGNoeUdGNC8lKnN5bW1ldHJpY0dGNC8lKGxhcmdlb3BHRjQvJS5tb3ZhYmxlbGltaXRzR0Y0LyUnYWNjZW50R0Y0LyUnbHNwYWNlR1EmMC4wZW1GJy8lJ3JzcGFjZUdRLDAuMzMzMzMzM2VtRictRiw2JlEiakYnRi9GMkY1RkAtSSNtbkdGJDYlUSIxRidGMkZELyUlc2l6ZUdRIzEyRidGMkZERjJGRC8lJW9wZW5HUSJbRicvJSZjbG9zZUdRIl1GJy1GQTYuUSUmb3I7RidGMkZERkYvRklGNC9GS0YxRkxGTkZQRlIvRlVRLDAuMjIyMjIyMmVtRicvRlhGam9GKy1GOTYnLUYjNipGPUZARlpGQC1GaG42JVEiMkYnRjJGREZbb0YyRkRGMkZERl5vRmFvRmRvLUZBNi5RJyZzZG90O0YnRjJGREZGRmdvRkpGTEZORlBGUkZUL0ZYRlZGY3BGY3BGZG9GKy1GOTYnLUYjNipGPUZARlpGQC1GaG42JVEiOUYnRjJGREZbb0YyRkRGMkZERl5vRmFvRltvRjJGRA== for each LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYsLUkjbW5HRiQ2JVEiMUYnLyUrZXhlY3V0YWJsZUdRJmZhbHNlRicvJSxtYXRodmFyaWFudEdRJ25vcm1hbEYnLUkjbW9HRiQ2LlEmJmxlcTtGJ0YvRjIvJSZmZW5jZUdGMS8lKnNlcGFyYXRvckdGMS8lKXN0cmV0Y2h5R0YxLyUqc3ltbWV0cmljR0YxLyUobGFyZ2VvcEdGMS8lLm1vdmFibGVsaW1pdHNHRjEvJSdhY2NlbnRHRjEvJSdsc3BhY2VHUSwwLjI3Nzc3NzhlbUYnLyUncnNwYWNlR0ZJLUkjbWlHRiQ2JlEiaUYnLyUnaXRhbGljR1EldHJ1ZUYnRi8vRjNRJ2l0YWxpY0YnLUY2Ni5RIixGJ0YvRjJGOS9GPEZSRj1GP0ZBRkNGRS9GSFEmMC4wZW1GJy9GS1EsMC4zMzMzMzMzZW1GJy1GTTYmUSJqRidGUEYvRlNGNS1GLDYlUSI5RidGL0YyLyUlc2l6ZUdRIzEyRidGL0Yy. atLeastOneDigit := seq(seq(&or(seq(S[i,j,k], k=1..9)), j=1..9), i=1..9):

For each square LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkobWZlbmNlZEdGJDYlLUYjNigtSSNtaUdGJDYmUSJpRicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRictSSNtb0dGJDYuUSIsRidGNy9GO1Enbm9ybWFsRicvJSZmZW5jZUdGOS8lKnNlcGFyYXRvckdGNi8lKXN0cmV0Y2h5R0Y5LyUqc3ltbWV0cmljR0Y5LyUobGFyZ2VvcEdGOS8lLm1vdmFibGVsaW1pdHNHRjkvJSdhY2NlbnRHRjkvJSdsc3BhY2VHUSYwLjBlbUYnLyUncnNwYWNlR1EsMC4zMzMzMzMzZW1GJy1GMTYmUSJqRidGNEY3RjovJSVzaXplR1EjMTJGJ0Y3RkFGN0ZBRlpGN0ZB if the digit LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkjbWlHRiQ2JlEia0YnLyUnaXRhbGljR1EldHJ1ZUYnLyUrZXhlY3V0YWJsZUdRJmZhbHNlRicvJSxtYXRodmFyaWFudEdRJ2l0YWxpY0YnLyUlc2l6ZUdRIzEyRidGMi9GNlEnbm9ybWFsRic= appears in that square then no other digit appears in that square. These clauses have the form LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYsLUkjbWlHRiQ2JlEiU0YnLyUnaXRhbGljR1EldHJ1ZUYnLyUrZXhlY3V0YWJsZUdRJmZhbHNlRicvJSxtYXRodmFyaWFudEdRJ2l0YWxpY0YnLUkobWZlbmNlZEdGJDYnLUYjNiotRiw2JlEiaUYnRi9GMkY1LUkjbW9HRiQ2LlEiLEYnRjIvRjZRJ25vcm1hbEYnLyUmZmVuY2VHRjQvJSpzZXBhcmF0b3JHRjEvJSlzdHJldGNoeUdGNC8lKnN5bW1ldHJpY0dGNC8lKGxhcmdlb3BHRjQvJS5tb3ZhYmxlbGltaXRzR0Y0LyUnYWNjZW50R0Y0LyUnbHNwYWNlR1EmMC4wZW1GJy8lJ3JzcGFjZUdRLDAuMzMzMzMzM2VtRictRiw2JlEiakYnRi9GMkY1RkAtRiw2JlEia0YnRi9GMkY1LyUlc2l6ZUdRIzEyRidGMkZERjJGRC8lJW9wZW5HUSJbRicvJSZjbG9zZUdRIl1GJy1GQTYuUSomSW1wbGllcztGJ0YyRkRGRi9GSUY0L0ZLRjFGTEZORlBGUi9GVVEsMC4yNzc3Nzc4ZW1GJy9GWEZpby1GQTYuUSJ+RidGMkZERkZGZm9GSkZMRk5GUEZSRlQvRlhGVi1GQTYuUSYmbm90O0YnRjJGREZGRmZvRkpGTEZORlBGUkZURmpvRistRjk2Jy1GIzYqRj1GQEZaRkAtRiw2JlEibEYnRi9GMkY1RmpuRjJGREYyRkRGXW9GYG9Gam5GMkZE (alternatively, LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYtLUkjbW9HRiQ2LlEmJm5vdDtGJy8lK2V4ZWN1dGFibGVHUSZmYWxzZUYnLyUsbWF0aHZhcmlhbnRHUSdub3JtYWxGJy8lJmZlbmNlR0YxLyUqc2VwYXJhdG9yR0YxLyUpc3RyZXRjaHlHRjEvJSpzeW1tZXRyaWNHRjEvJShsYXJnZW9wR0YxLyUubW92YWJsZWxpbWl0c0dGMS8lJ2FjY2VudEdGMS8lJ2xzcGFjZUdRJjAuMGVtRicvJSdyc3BhY2VHUSwwLjI3Nzc3NzhlbUYnLUkjbWlHRiQ2JlEiU0YnLyUnaXRhbGljR1EldHJ1ZUYnRi8vRjNRJ2l0YWxpY0YnLUkobWZlbmNlZEdGJDYnLUYjNiotRko2JlEiaUYnRk1GL0ZQLUYsNi5RIixGJ0YvRjJGNS9GOEZPRjlGO0Y9Rj9GQUZDL0ZHUSwwLjMzMzMzMzNlbUYnLUZKNiZRImpGJ0ZNRi9GUEZaLUZKNiZRImtGJ0ZNRi9GUC8lJXNpemVHUSMxMkYnRi9GMkYvRjIvJSVvcGVuR1EiW0YnLyUmY2xvc2VHUSJdRictRiw2LlElJm9yO0YnRi9GMkY1RjcvRjpGT0Y7Rj1GP0ZBL0ZEUSwwLjIyMjIyMjJlbUYnL0ZHRl5wLUYsNi5RIn5GJ0YvRjJGNUY3RjlGO0Y9Rj9GQUZDL0ZHRkVGK0ZJLUZTNictRiM2KkZXRlpGam5GWi1GSjYmUSJsRidGTUYvRlBGYG9GL0YyRi9GMkZjb0Zmb0Zgb0YvRjI=) where LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkjbWlHRiQ2JlEibEYnLyUnaXRhbGljR1EldHJ1ZUYnLyUrZXhlY3V0YWJsZUdRJmZhbHNlRicvJSxtYXRodmFyaWFudEdRJ2l0YWxpY0YnLyUlc2l6ZUdRIzEyRidGMi9GNlEnbm9ybWFsRic= is a digit with LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYoLUkjbWlHRiQ2JlEia0YnLyUnaXRhbGljR1EldHJ1ZUYnLyUrZXhlY3V0YWJsZUdRJmZhbHNlRicvJSxtYXRodmFyaWFudEdRJ2l0YWxpY0YnLUkjbW9HRiQ2LlElJm5lO0YnRjIvRjZRJ25vcm1hbEYnLyUmZmVuY2VHRjQvJSpzZXBhcmF0b3JHRjQvJSlzdHJldGNoeUdGNC8lKnN5bW1ldHJpY0dGNC8lKGxhcmdlb3BHRjQvJS5tb3ZhYmxlbGltaXRzR0Y0LyUnYWNjZW50R0Y0LyUnbHNwYWNlR1EsMC4yNzc3Nzc4ZW1GJy8lJ3JzcGFjZUdGTi1GLDYmUSJsRidGL0YyRjUvJSVzaXplR1EjMTJGJ0YyRjw=. atMostOneDigit := seq(seq(seq(seq(S[i, j, k] &implies &not(S[i, j, l]), l=k+1..9), k=1..9), j=1..9), i=1..9): For each square LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkobWZlbmNlZEdGJDYlLUYjNigtSSNtaUdGJDYmUSJpRicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRictSSNtb0dGJDYuUSIsRidGNy9GO1Enbm9ybWFsRicvJSZmZW5jZUdGOS8lKnNlcGFyYXRvckdGNi8lKXN0cmV0Y2h5R0Y5LyUqc3ltbWV0cmljR0Y5LyUobGFyZ2VvcEdGOS8lLm1vdmFibGVsaW1pdHNHRjkvJSdhY2NlbnRHRjkvJSdsc3BhY2VHUSYwLjBlbUYnLyUncnNwYWNlR1EsMC4zMzMzMzMzZW1GJy1GMTYmUSJqRidGNEY3RjovJSVzaXplR1EjMTJGJ0Y3RkFGN0ZBRlpGN0ZB if the digit LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkjbWlHRiQ2JlEia0YnLyUnaXRhbGljR1EldHJ1ZUYnLyUrZXhlY3V0YWJsZUdRJmZhbHNlRicvJSxtYXRodmFyaWFudEdRJ2l0YWxpY0YnLyUlc2l6ZUdRIzEyRidGMi9GNlEnbm9ybWFsRic= appears in that square then the digit LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkjbWlHRiQ2JlEia0YnLyUnaXRhbGljR1EldHJ1ZUYnLyUrZXhlY3V0YWJsZUdRJmZhbHNlRicvJSxtYXRodmFyaWFudEdRJ2l0YWxpY0YnLyUlc2l6ZUdRIzEyRidGMi9GNlEnbm9ybWFsRic= does not appear in any other square in the same row, column, or block. These clauses have the form LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYrLUkjbWlHRiQ2JlEiU0YnLyUnaXRhbGljR1EldHJ1ZUYnLyUrZXhlY3V0YWJsZUdRJmZhbHNlRicvJSxtYXRodmFyaWFudEdRJ2l0YWxpY0YnLUkobWZlbmNlZEdGJDYnLUYjNiotRiw2JlEiaUYnRi9GMkY1LUkjbW9HRiQ2LlEiLEYnRjIvRjZRJ25vcm1hbEYnLyUmZmVuY2VHRjQvJSpzZXBhcmF0b3JHRjEvJSlzdHJldGNoeUdGNC8lKnN5bW1ldHJpY0dGNC8lKGxhcmdlb3BHRjQvJS5tb3ZhYmxlbGltaXRzR0Y0LyUnYWNjZW50R0Y0LyUnbHNwYWNlR1EmMC4wZW1GJy8lJ3JzcGFjZUdRLDAuMzMzMzMzM2VtRictRiw2JlEiakYnRi9GMkY1RkAtRiw2JlEia0YnRi9GMkY1LyUlc2l6ZUdRIzEyRidGMkZERjJGRC8lJW9wZW5HUSJbRicvJSZjbG9zZUdRIl1GJy1GQTYuUSomSW1wbGllcztGJ0YyRkRGRi9GSUY0L0ZLRjFGTEZORlBGUi9GVVEsMC4yNzc3Nzc4ZW1GJy9GWEZpby1GQTYuUSJ+RidGMkZERkZGZm9GSkZMRk5GUEZSRlQvRlhGVi1GQTYuUSYmbm90O0YnRjJGREZGRmZvRkpGTEZORlBGUkZURmpvLUYsNiZRIkFGJ0YvRjJGNUZqbkYyRkQ= where LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkjbWlHRiQ2JlEiQUYnLyUnaXRhbGljR1EldHJ1ZUYnLyUrZXhlY3V0YWJsZUdRJmZhbHNlRicvJSxtYXRodmFyaWFudEdRJ2l0YWxpY0YnLyUlc2l6ZUdRIzEyRidGMi9GNlEnbm9ybWFsRic= is in the set LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYnLUkjbWlHRiQ2JlEoYWxsVmFyc0YnLyUnaXRhbGljR1EldHJ1ZUYnLyUrZXhlY3V0YWJsZUdRJmZhbHNlRicvJSxtYXRodmFyaWFudEdRJ2l0YWxpY0YnLUkobWZlbmNlZEdGJDYlLUYjNiotRiw2JlEiaUYnRi9GMkY1LUkjbW9HRiQ2LlEiLEYnRjIvRjZRJ25vcm1hbEYnLyUmZmVuY2VHRjQvJSpzZXBhcmF0b3JHRjEvJSlzdHJldGNoeUdGNC8lKnN5bW1ldHJpY0dGNC8lKGxhcmdlb3BHRjQvJS5tb3ZhYmxlbGltaXRzR0Y0LyUnYWNjZW50R0Y0LyUnbHNwYWNlR1EmMC4wZW1GJy8lJ3JzcGFjZUdRLDAuMzMzMzMzM2VtRictRiw2JlEiakYnRi9GMkY1RkAtRiw2JlEia0YnRi9GMkY1LyUlc2l6ZUdRIzEyRidGMkZERjJGREZqbkYyRkQ=. distinctnessConstraints := seq(seq(seq(seq(S[i, j, k] &implies &not(A), A in allVars(i, j, k)), k=1..9), j=1..9), i=1..9):

We also need to specify the 21 numbers which are given to us as a part of the puzzle; if LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkobWZlbmNlZEdGJDYlLUYjNigtSSNtaUdGJDYmUSJpRicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRictSSNtb0dGJDYuUSIsRidGNy9GO1Enbm9ybWFsRicvJSZmZW5jZUdGOS8lKnNlcGFyYXRvckdGNi8lKXN0cmV0Y2h5R0Y5LyUqc3ltbWV0cmljR0Y5LyUobGFyZ2VvcEdGOS8lLm1vdmFibGVsaW1pdHNHRjkvJSdhY2NlbnRHRjkvJSdsc3BhY2VHUSYwLjBlbUYnLyUncnNwYWNlR1EsMC4zMzMzMzMzZW1GJy1GMTYmUSJqRidGNEY3RjovJSVzaXplR1EjMTJGJ0Y3RkFGN0ZBRlpGN0ZB contains LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkjbWlHRiQ2JlEia0YnLyUnaXRhbGljR1EldHJ1ZUYnLyUrZXhlY3V0YWJsZUdRJmZhbHNlRicvJSxtYXRodmFyaWFudEdRJ2l0YWxpY0YnLyUlc2l6ZUdRIzEyRidGMi9GNlEnbm9ybWFsRic= then we need to include the unit clause LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYnLUkjbWlHRiQ2JlEiU0YnLyUnaXRhbGljR1EldHJ1ZUYnLyUrZXhlY3V0YWJsZUdRJmZhbHNlRicvJSxtYXRodmFyaWFudEdRJ2l0YWxpY0YnLUkobWZlbmNlZEdGJDYnLUYjNiotRiw2JlEiaUYnRi9GMkY1LUkjbW9HRiQ2LlEiLEYnRjIvRjZRJ25vcm1hbEYnLyUmZmVuY2VHRjQvJSpzZXBhcmF0b3JHRjEvJSlzdHJldGNoeUdGNC8lKnN5bW1ldHJpY0dGNC8lKGxhcmdlb3BHRjQvJS5tb3ZhYmxlbGltaXRzR0Y0LyUnYWNjZW50R0Y0LyUnbHNwYWNlR1EmMC4wZW1GJy8lJ3JzcGFjZUdRLDAuMzMzMzMzM2VtRictRiw2JlEiakYnRi9GMkY1RkAtRiw2JlEia0YnRi9GMkY1LyUlc2l6ZUdRIzEyRidGMkZERjJGRC8lJW9wZW5HUSJbRicvJSZjbG9zZUdRIl1GJ0ZqbkYyRkQ= in our SAT instance. The clauses resulting from the world's hardest Sudoku are as follows: givenNumbers := {S[1,9,8], S[2,1,9], S[2,6,5], S[2,7,7], S[3,2,8], S[3,3,1], S[3,8,3], S[4,2,5], S[4,4,1], S[4,8,6], S[5,5,4], S[5,7,9], S[6,5,5], S[6,6,7], S[7,1,4], S[7,5,7], S[7,7,2], S[8,2,1], S[8,3,6], S[8,4,3], S[9,3,8]}: We use the Satisfy command from the Logic package which finds a satisfying assignment of a logical formula if one exists. We use the Usage command from the CodeTools package to measure how quickly the solution is found. allConstraints := atLeastOneDigit, atMostOneDigit, distinctnessConstraints, givenNumbers[]: satisfyingAssignment := CodeTools:-Usage(Logic:-Satisfy(&and(allConstraints))):

The following functions use commands from the plots and plottools packages to draw a Sudoku grid and fill in numbers on the grid. with(plots): with(plottools): drawSudokuGrid := proc() local squares, blocks; squares := seq(seq(rectangle([i,j+1], [i+1,j], style=line, thickness=0), j=1..9), i=1..9); blocks := seq(seq(rectangle([3*(i-1)+1,3*j+1], [3*i+1,3*(j-1)+1], thickness=2, color=`if`(type(i+j, even), "White", "LightGray")), j=1..3), i=1..3); return squares, blocks; end proc: # Draw the digit k in the square at (i, j) (in bold if given is true) drawDigit := proc(i, j, k, given) textplot([i+0.5, j+0.5, k], font=[Arial, `if`(given, bold, roman), 18]); end proc: The following code draws the Sudoku grid with the digits from the solution found by the SAT solver. digits := Array(1..9*9): i := 1: for eq in satisfyingAssignment do if rhs(eq) then digits[i] := drawDigit(op(lhs(eq)), lhs(eq) in givenNumbers); i := i + 1; end if; end do: display(drawSudokuGrid(), entries(digits, nolist), scaling=constrained, axes=none);

JSFH