Instantly share code, notes, and snippets.

# barrbrain/Sudoku.ipynb Created Jan 9, 2018

Exploring Sudoku solving in Python
 { "cells": [ { "cell_type": "code", "execution_count": 1, "metadata": { "collapsed": false, "scrolled": true }, "outputs": [ { "data": { "text/html": [ "
4 2
1 9 3
1 5 9 4
24 168
6 9 7 3 1
543 82
3 6 7 5
9 8 2
5 9
" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" }, { "name": "stdout", "output_type": "stream", "text": [ "[(0, 0, 4), (0, 8, 2), (1, 3, 1), (1, 5, 9), (1, 8, 3), (2, 1, 1), (2, 3, 5), (2, 6, 9), (2, 8, 4), (3, 2, 2), (3, 3, 4), (3, 5, 1), (3, 6, 6), (3, 7, 8), (4, 0, 6), (4, 2, 9), (4, 4, 7), (4, 6, 3), (4, 8, 1), (5, 1, 5), (5, 2, 4), (5, 3, 3), (5, 5, 8), (5, 6, 2), (6, 0, 3), (6, 2, 6), (6, 5, 7), (6, 7, 5), (7, 0, 9), (7, 3, 8), (7, 5, 2), (8, 0, 5), (8, 8, 9)]\n" ] } ], "source": [ "from IPython.display import HTML, display\n", "\n", "def display_table(data):\n", " display(HTML('
{}'.format(\n", " '
{}'.join(str(_) for _ in row)) for row in data))))\n", "\n", "puzzle = \"\"\"\n", "4 2\n", " 1 9 3\n", " 1 5 9 4\n", " 24 168 \n", "6 9 7 3 1\n", " 543 82 \n", "3 6 7 5 \n", "9 8 2 \n", "5 9\n", "\"\"\".splitlines()[1:];\n", "\n", "def base_units():\n", " return [(i, j, int(v)) for i in range(9) for j, v in enumerate(puzzle[i]) if v != ' ']\n", "\n", "display_table(puzzle)\n", "print(base_units())" ] }, { "cell_type": "code", "execution_count": 2, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/html": [ "
49 2
1 9 3
1 5 9 4
24 168
6 9 7 3 1
543 82
3 6 7 5
9 8 2
5 9
" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "def apply_label(v):\n", " global puzzle\n", " i, j, n = v\n", " puzzle[i] = puzzle[i][:j] + str(n) + puzzle[i][j + 1:]\n", "\n", "apply_label((0,1,9))\n", "display_table(puzzle)" ] }, { "cell_type": "code", "execution_count": 3, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/plain": [ "(324, 34)" ] }, "execution_count": 3, "metadata": {}, "output_type": "execute_result" } ], "source": [ "# Each square has a number 1..9\n", "unit_rules = [\n", " [(i, j, n) for n in range(1, 10)]\n", " for i in range(9) for j in range(9)]\n", "# Each row has a square with a number 1..9\n", "row_rules = [\n", " [(i, j, n) for j in range(9)]\n", " for i in range(9) for n in range(1, 10)]\n", "# Each column has a square with a number 1..9\n", "column_rules = [\n", " [(i, j, n) for i in range(9)]\n", " for j in range(9) for n in range(1, 10)]\n", "# Each 3x3 block has a square with a number 1..9\n", "block_rules = [\n", " [(i, j, n) for i in range(3 * i_, 3 * i_ + 3) for j in range(3 * j_, 3 * j_ + 3)]\n", " for n in range(1, 10) for i_ in range(3) for j_ in range(3)]\n", "base_rules = unit_rules + row_rules + column_rules + block_rules\n", "rules = [set(r) for r in base_rules]\n", "units = set(base_units())\n", "counter_units = set()\n", "len(rules), len(units)" ] }, { "cell_type": "code", "execution_count": 4, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/html": [ "
493 2
1 9 3
1 5 9 4
24 168
6 9 7 3 1
543 82
3 6 7 5
9 8 2
5 9
" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "apply_label((0,2,3))\n", "display_table(puzzle)" ] }, { "cell_type": "code", "execution_count": 5, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/html": [ "
4937 2
1 9 3
1 5 9 4
24 168
6 9 7 3 1
543 82
3 6 7 5
9 8 2
5 9
" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "apply_label((0,3,7))\n", "display_table(puzzle)" ] }, { "cell_type": "code", "execution_count": 6, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/html": [ "
49378 2
1 9 3
1 5 9 4
24 168
6 9 7 3 1
543 82
3 6 7 5
9 8 2
5 9
" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "apply_label((0,4,8))\n", "display_table(puzzle)" ] }, { "cell_type": "code", "execution_count": 7, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/html": [ "
493786 2
1 9 3
1 5 9 4
24 168
6 9 7 3 1
543 82
3 6 7 5
9 8 2
5 9
" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "apply_label((0,5,6))\n", "display_table(puzzle)" ] }, { "cell_type": "code", "execution_count": 8, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/html": [ "
4937865 2
1 9 3
1 5 9 4
24 168
6 9 7 3 1
543 82
3 6 7 5
9 8 2
5 9
" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "apply_label((0,6,5))\n", "display_table(puzzle)" ] }, { "cell_type": "code", "execution_count": 9, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/html": [ "
493786512
1 9 3
1 5 9 4
24 168
6 9 7 3 1
543 82
3 6 7 5
9 8 2
5 9
" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "apply_label((0,7,1))\n", "display_table(puzzle)" ] }, { "cell_type": "code", "execution_count": 10, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/html": [ "
493786512
2 1 9 3
1 5 9 4
24 168
6 9 7 3 1
543 82
3 6 7 5
9 8 2
5 9
" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "apply_label((1,0,2))\n", "display_table(puzzle)" ] }, { "cell_type": "code", "execution_count": 11, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/html": [ "
493786512
26 1 9 3
1 5 9 4
24 168
6 9 7 3 1
543 82
3 6 7 5
9 8 2
5 9
" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "apply_label((1,1,6))\n", "display_table(puzzle)" ] }, { "cell_type": "code", "execution_count": 12, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/html": [ "
493786512
2651 9 3
1 5 9 4
24 168
6 9 7 3 1
543 82
3 6 7 5
9 8 2
5 9
" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "apply_label((1,2,5))\n", "display_table(puzzle)" ] }, { "cell_type": "code", "execution_count": 13, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/html": [ "
493786512
265149 3
1 5 9 4
24 168
6 9 7 3 1
543 82
3 6 7 5
9 8 2
5 9
" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "apply_label((1,4,4))\n", "display_table(puzzle)" ] }, { "cell_type": "code", "execution_count": 14, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/html": [ "
493786512
2651498 3
1 5 9 4
24 168
6 9 7 3 1
543 82
3 6 7 5
9 8 2
5 9
" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "apply_label((1,6,8))\n", "display_table(puzzle)" ] }, { "cell_type": "code", "execution_count": 15, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/html": [ "
493786512
265149873
1 5 9 4
24 168
6 9 7 3 1
543 82
3 6 7 5
9 8 2
5 9
" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "apply_label((1,7,7))\n", "display_table(puzzle)" ] }, { "cell_type": "code", "execution_count": 16, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/html": [ "
493786512
265149873
81 5 9 4
24 168
6 9 7 3 1
543 82
3 6 7 5
9 8 2
5 9
" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "apply_label((2,0,8))\n", "display_table(puzzle)" ] }, { "cell_type": "code", "execution_count": 17, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/html": [ "
493786512
265149873
8175 9 4
24 168
6 9 7 3 1
543 82
3 6 7 5
9 8 2
5 9
" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "apply_label((2,2,7))\n", "display_table(puzzle)" ] }, { "cell_type": "code", "execution_count": 18, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/html": [ "
493786512
265149873
81752 9 4
24 168
6 9 7 3 1
543 82
3 6 7 5
9 8 2
5 9
" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "apply_label((2,4,2))\n", "display_table(puzzle)" ] }, { "cell_type": "code", "execution_count": 19, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/html": [ "
493786512
265149873
81752 9 4
324 1685
68927 341
15436829
3 69 7 58
9 852
5 29
" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/html": [ "
493786512
265149873
81752 9 4
732491685
689275341
154368297
3269 7 58
9 852 36
5 86 4 29
" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/html": [ "
493786512
265149873
81752 9 4
732491685
689275341
154368297
326917458
941852 36
5 8634 29
" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/html": [ "
493786512
265149873
817523964
732491685
689275341
154368297
326917458
941852736
578634129
" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "def propagate_units():\n", " global rules\n", " global units\n", " global counter_units\n", " rules_ = []\n", " for rule in rules:\n", " # If any fact covered by this rule is true,\n", " # everything else in the rule is not true\n", " hit = units & rule\n", " if any(hit):\n", " counter_units |= rule - hit\n", " continue\n", " # Any fact in this rule already known to be false,\n", " # can be removed until the last is proven by elimination.\n", " rule -= counter_units\n", " if len(rule) == 1:\n", " units |= rule\n", " # Add this fact to the puzzle\n", " [apply_label(l) for l in rule]\n", " continue\n", " # If there are still multiple unknowns,\n", " # keep the rule for the next round.\n", " rules_.append(rule)\n", " rules = rules_\n", "\n", "while len(units) < 81:\n", " propagate_units()\n", " display_table(puzzle)" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "collapsed": true }, "outputs": [], "source": [] } ], "metadata": { "anaconda-cloud": {}, "kernelspec": { "display_name": "Python [conda root]", "language": "python", "name": "conda-root-py" }, "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.5.2" } }, "nbformat": 4, "nbformat_minor": 1 }
'.join(''.format(\n", " '