{"id":325,"date":"2021-03-23T20:31:32","date_gmt":"2021-03-23T19:31:32","guid":{"rendered":"https:\/\/ca.rstenpresser.de\/blag\/?p=325"},"modified":"2021-03-23T20:32:19","modified_gmt":"2021-03-23T19:32:19","slug":"solving-greater-than-sudoku-with-python-and-z3","status":"publish","type":"post","link":"https:\/\/ca.rstenpresser.de\/blag\/2021\/03\/solving-greater-than-sudoku-with-python-and-z3\/","title":{"rendered":"Solving &#8216;Greater-than sudoku&#8217; with python and z3"},"content":{"rendered":"\n<p>In one of my pen&#8217;n&#8217;paper groups we are playing &#8220;<a href=\"https:\/\/de.wiki-aventurica.de\/wiki\/Niobaras_Verm%C3%A4chtnis\">Niobaras Verm\u00e4chtnis<\/a>&#8220;. One of the riddles given in it involves solving a sudoku. <\/p>\n\n\n\n<p>Its a variant of a regular sudoku called &#8220;greater than sudoku&#8221;, or in german &#8220;Vergleichssudoku&#8221;. Since I am to lazy to solve such a thing manually, I looked for a constraints solver to do that for me. I have never used something like that, so I started looking into different options:<\/p>\n\n\n\n<ul><li>prolog  -&gt; I checked the wikipedia page and decided its to complicated for me^^<\/li><li>clasp -&gt; there was a python binding, I played around with that, but its python2 only<\/li><li>z3 -&gt; it has python3 bindings and a sudoku example. So lets use that.<\/li><\/ul>\n\n\n\n<p>I started from the <a href=\"https:\/\/ericpony.github.io\/z3py-tutorial\/guide-examples.htm\">example<\/a> and added the greater-than constraints. They are encoded as strings, in horizontal and vertical direction.<\/p>\n\n\n\n<p>Because the solver did not work, I added a hacky visualization to check the constraints visually. Then used some image processing to overlay that with the original riddle<\/p>\n\n\n\n<figure class=\"wp-block-image\"><img loading=\"lazy\" decoding=\"async\" width=\"715\" height=\"693\" src=\"https:\/\/ca.rstenpresser.de\/wp-files\/2021\/03\/image-1.png\" alt=\"\" class=\"wp-image-327\"\/><figcaption>Constraints visually overlayed<\/figcaption><\/figure>\n\n\n\n<p>I did quite some more checking, and finally decided to test a known good sudoku. I found <a href=\"https:\/\/plus.maths.org\/content\/puzzle-page-77\">this one<\/a> which solves fine<\/p>\n\n\n\n<p>Thus, the reasonable explanation was that my solver is fine, but the riddle is not. Turns out, somebody already made the same discovery as me. <\/p>\n\n\n\n<p>The people over at a DSA fanpage <a href=\"https:\/\/asboran.de\/2018\/12\/23\/zum-4-advent-niobaras-sudoku\/\">asboran.de<\/a> already figured that out more than two years ago. After applying their proposed fix, the solver finally returns <strong>sat<\/strong> and produces an output:<\/p>\n\n\n\n<figure class=\"wp-block-image\"><img loading=\"lazy\" decoding=\"async\" width=\"735\" height=\"719\" src=\"https:\/\/ca.rstenpresser.de\/wp-files\/2021\/03\/image-2.png\" alt=\"\" class=\"wp-image-328\"\/><figcaption>The solved(?) sudoku<\/figcaption><\/figure>\n\n\n\n<p>Here is my code if you like to laugh about it, or copy it. License is the same as the example I copied it from<\/p>\n\n\n\n<pre class=\"wp-block-code\"><code>from z3 import Int, Solver, And, Distinct, If, sat;\n\ndebug = False\n\n# most of this code was taken and copied from the example at\n# https:\/\/ericpony.github.io\/z3py-tutorial\/guide-examples.htm\n\n# other reference for 'greater than sudokus'\n# https:\/\/github.com\/kit1980\/grid-puzzle-solver\/blob\/master\/greater-than-sudoku.ecl\n\n# From niobaras verm\u00e4chtnis (does not work)\n# Horizontal constraints\nGH = [\">&lt;>&lt;&lt;>\",\n      \">&lt;&lt;>&lt;>\",\n      \"&lt;&lt;&lt;>>&lt;\",\n      \">>>&lt;>>\",\n      \">&lt;&lt;&lt;&lt;&lt;\",\n      \">&lt;>>&lt;>\",\n      \"&lt;>>&lt;>&lt;\",\n      \"&lt;>&lt;>>&lt;\",\n      \"&lt;&lt;>&lt;&lt;&lt;\"]\n\n# vertical\nGV = [\"&lt;>>>>&lt;\",\n      \">&lt;>>>&lt;\",\n      \"&lt;>&lt;>&lt;&lt;\",\n      \">&lt;>&lt;&lt;>\",\n      \">&lt;&lt;&lt;&lt;>\",\n      \">&lt;&lt;>>&lt;\",\n      \"&lt;&lt;>&lt;&lt;>\",\n      \">&lt;>&lt;>&lt;\", # original constraints with error\n      \"&lt;&lt;&lt;>>&lt;\"]\n\n#         | this char was changed\nGV[7] = \">>>&lt;>&lt;\"\n\n# from: https:\/\/plus.maths.org\/content\/puzzle-page-77\n# we know a solution for this!\n# Horizontal constraints\nGH1 = [\">&lt;>&lt;&lt;>\",\n      \"&lt;&lt;>&lt;&lt;&lt;\",\n      \"&lt;&lt;&lt;&lt;&lt;>\",\n      \">>>&lt;&lt;>\",\n      \"&lt;>>>&lt;>\",\n      \">>>>&lt;&lt;\",\n      \"&lt;&lt;&lt;>>&lt;\",\n      \">&lt;&lt;&lt;>&lt;\",\n      \"&lt;>>&lt;>&lt;\"]\n\n# vertical\nGV1 = [\"&lt;>>&lt;&lt;&lt;\",\n      \"&lt;>&lt;>&lt;&lt;\",\n      \"&lt;>>&lt;&lt;>\",\n      \">&lt;&lt;>>&lt;\",\n      \">&lt;&lt;>>>\",\n      \">>>>>>\",\n      \">&lt;&lt;>&lt;>\",\n      \">&lt;>&lt;>>\",\n      \"&lt;>>&lt;&lt;&lt;\"]\n\n# very hacky visualization\ndef print_matrix(m):\n  print(\"\\n?????????????????????????????????????\")\n  lineidx=0\n  for line in range(9):\n    print(\"?\", end='')\n    colidx = 0\n    for col in range(9):\n      print(\" {} \".format(str(m[line][col])), end='')\n      if (col+1) % 3 != 0:\n        ch = u\"\\u140a\"\n        if GH[line][colidx] == \">\":\n          ch = u\"\\u1405\"\n        print(ch, end='')\n        colidx+=1\n      else:\n        print(\"?\", end='')\n    if (line+1) % 3 == 0:\n      if (line != 8):\n        print(\"\\n?????????????????????????????????????\")\n    else:\n      a = [\"i\"]*9\n      for foo in range(9):\n        a[foo] = u\"\\u25bc\" \n        if GV[foo][lineidx] == \"&lt;\":\n          a[foo] = u\"\\u25b2\"\n      print(\"\\n? {}   {}   {} ? {}   {}   {} ? {}   {}   {} ?\".format(a[0], a[1], a[2], a[3], a[4], a[5], a[6], a[7], a[8]))\n      lineidx+=1\n  print(\"\\n?????????????????????????????????????\")\n\n\n\n\n## Begin adding constraints\n\n###Jede Zahl nur eine Stelle; jede Spalte, jede Zeile, jedes Quadrat darin einmal jede Zahl.\n\n# 9x9 matrix of integer variables\nX = [ [ Int(\"x_%s_%s\" % (i, j)) for j in range(9) ]\n      for i in range(9) ]\n\n#Jede Zahl nur eine Stelle;\n# each cell contains a value in {1, ..., 9}\ncells_c  = [ And(1 &lt;= X[i][j], X[i][j] &lt;= 9)\n             for i in range(9) for j in range(9) ]\n\n\ncols_c = []\nrows_c = []\nfor i in range(9):\n  # jede Zeile, \n  # each row contains a digit at most once\n  rows_c.append(Distinct([X[i][j] for j in range(9)]))\n\n  # jede Spalte, \n  # each column contains a digit at most once\n  cols_c.append(Distinct([X[j][i] for j in range(9)]))\n\n\n#jedes Quadrat darin einmal jede Zahl.\n# each 3x3 square contains a digit at most once\nsq_c     = [ Distinct([ X[3*i0 + i][3*j0 + j]\n                        for i in range(3) for j in range(3) ])\n             for i0 in range(3) for j0 in range(3) ]\n\n# the basic sudoku constraints\nsudoku_c = cells_c + cols_c + rows_c + sq_c\n\n# build our DSA horizontal constraints\nxl= [0,1,3,4,6,7] # have a stupid lookup-thingy, only 6 out of 9 items have a constraint\nh_c = []\nfor lidx, line in enumerate(GH, start=0):\n  for cidx, c in enumerate(line, start=0):\n    if c == \">\":\n      h_c.append(X[lidx][xl[cidx]] > X[lidx][xl[cidx]+1])\n      #print(\"X{}_{} > X{}_{}\".format(lidx, xl[cidx], lidx, xl[cidx]+1))\n    else:\n      h_c.append(X[lidx][xl[cidx]] &lt; X[lidx][xl[cidx]+1])\n      #print(\"X{}_{} &lt; X{}_{}\".format(lidx, xl[cidx], lidx, xl[cidx]+1))\n\n# build our DSA vertical constraints\nv_c = []\nfor ridx, row in enumerate(GV, start=0):\n  for cidx, c in enumerate(row, start=0):\n    if c == \">\":\n      v_c.append(X[xl[cidx]][ridx] > X[xl[cidx]+1][ridx])\n      #print(\"X{}_{} > X{}_{}\".format(xl[cidx], ridx, xl[cidx]+1, ridx))\n    else:\n      v_c.append(X[xl[cidx]][ridx] &lt; X[xl[cidx]+1][ridx])\n      #print(\"X{}_{} &lt; X{}_{}\".format(xl[cidx], ridx, xl[cidx]+1, ridx))\n\nif debug:\n  print(\"Cells 1..9:\", cells_c)\n  print(\"Rows:\", rows_c)\n  print(\"Cols:\", cols_c)\n  print(\"SubSquares:\", sq_c)\n  print(\"Horizontal:\", h_c)\n  print(\"Vertical:\", v_c)\n  for co in sudoku_c + h_c + v_c:\n    print (co)\n\n# print a empty matrix so we van visually inspect the constraints\nempty = [[\"?\"]*9]*9\nprint_matrix(empty)\n\n# create a solver, add all constraints\ns = Solver()\n\n\ns.add(sudoku_c + h_c + v_c)\nif s.check() == sat:\n    print(\"done\")\n    m = s.model()\n    r = [ [ m.evaluate(X[i][j]) for j in range(9) ]\n          for i in range(9) ]\n    print_matrix(r)\nelse:\n    print (\"failed to solve\")\n\nprint (s.statistics())\n\n<\/code><\/pre>\n","protected":false},"excerpt":{"rendered":"<p>In one of my pen&#8217;n&#8217;paper groups we are playing &#8220;Niobaras Verm\u00e4chtnis&#8220;. One of the riddles given in it involves solving a sudoku. Its a variant of a regular sudoku called &#8220;greater than sudoku&#8221;, or in german &#8220;Vergleichssudoku&#8221;. Since I am to lazy to solve such a thing manually, I looked for a constraints solver to &hellip; <a href=\"https:\/\/ca.rstenpresser.de\/blag\/2021\/03\/solving-greater-than-sudoku-with-python-and-z3\/\" class=\"more-link\">Continue reading <span class=\"screen-reader-text\">Solving &#8216;Greater-than sudoku&#8217; with python and z3<\/span><\/a><\/p>\n","protected":false},"author":1,"featured_media":326,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[56],"tags":[138,137,35,135,136,131,134,133,139,132],"_links":{"self":[{"href":"https:\/\/ca.rstenpresser.de\/blag\/wp-json\/wp\/v2\/posts\/325"}],"collection":[{"href":"https:\/\/ca.rstenpresser.de\/blag\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/ca.rstenpresser.de\/blag\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/ca.rstenpresser.de\/blag\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/ca.rstenpresser.de\/blag\/wp-json\/wp\/v2\/comments?post=325"}],"version-history":[{"count":4,"href":"https:\/\/ca.rstenpresser.de\/blag\/wp-json\/wp\/v2\/posts\/325\/revisions"}],"predecessor-version":[{"id":332,"href":"https:\/\/ca.rstenpresser.de\/blag\/wp-json\/wp\/v2\/posts\/325\/revisions\/332"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/ca.rstenpresser.de\/blag\/wp-json\/wp\/v2\/media\/326"}],"wp:attachment":[{"href":"https:\/\/ca.rstenpresser.de\/blag\/wp-json\/wp\/v2\/media?parent=325"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/ca.rstenpresser.de\/blag\/wp-json\/wp\/v2\/categories?post=325"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/ca.rstenpresser.de\/blag\/wp-json\/wp\/v2\/tags?post=325"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}