435 lines
33 KiB
Plaintext
435 lines
33 KiB
Plaintext
{
|
|
"nbformat": 4,
|
|
"nbformat_minor": 0,
|
|
"metadata": {
|
|
"colab": {
|
|
"provenance": [],
|
|
"authorship_tag": "ABX9TyMDkDz3RrsH0nJVTdsejhO7",
|
|
"include_colab_link": true
|
|
},
|
|
"kernelspec": {
|
|
"name": "python3",
|
|
"display_name": "Python 3"
|
|
},
|
|
"language_info": {
|
|
"name": "python"
|
|
}
|
|
},
|
|
"cells": [
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {
|
|
"id": "view-in-github",
|
|
"colab_type": "text"
|
|
},
|
|
"source": [
|
|
"<a href=\"https://colab.research.google.com/github/udlbook/udlbook/blob/main/Trees/SAT_Sudoku_Answers.ipynb\" target=\"_parent\"><img src=\"https://colab.research.google.com/assets/colab-badge.svg\" alt=\"Open In Colab\"/></a>"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"source": [
|
|
"<img src=\"data:image/svg+xml;base64,PD94bWwgdmVyc2lvbj0iMS4wIiBlbmNvZGluZz0iVVRGLTgiPz4KPHN2ZyB3aWR0aD0iNzY0LjQ1IiBoZWlnaHQ9IjYzLjc1OSIgdmVyc2lvbj0iMS4xIiB2aWV3Qm94PSIwIDAgNzY0LjQ1IDYzLjc1OSIgeG1sbnM9Imh0dHA6Ly93d3cudzMub3JnLzIwMDAvc3ZnIj4KIDxnIHRyYW5zZm9ybT0ibWF0cml4KC43MzU0OCAwIDAgLjczNTQ4IDAgMy4zODgpIiBzdHJva2Utd2lkdGg9IjEuMzU5NyI+CiAgPHJlY3QgeD0iNWUtNyIgeT0iNWUtNyIgd2lkdGg9Ijc3LjM4NyIgaGVpZ2h0PSI3Ny4zODciIHJ5PSIxMS4zNSIgZmlsbD0iIzQ0NjlkOCIgb3BhY2l0eT0iLjk4IiBzdHJva2Utd2lkdGg9IjAiLz4KICA8dGV4dCB4PSIxMC4zMzA1NjciIHk9IjY1Ljc2MTcxOSIgZmlsbD0iI2ZmZmZmZiIgZm9udC1mYW1pbHk9IkNvdXJpZXIiIGZvbnQtc2l6ZT0iOTMuNDgzcHgiIHN0cm9rZS13aWR0aD0iMS4zNTk3IiBzdHlsZT0ibGluZS1oZWlnaHQ6MS4yNSIgeG1sOnNwYWNlPSJwcmVzZXJ2ZSI+PHRzcGFuIHg9IjEwLjMzMDU2NyIgeT0iNjUuNzYxNzE5IiBmaWxsPSIjZmZmZmZmIiBmb250LWZhbWlseT0iQ291cmllciIgc3Ryb2tlLXdpZHRoPSIxLjM1OTciPkkgPC90c3Bhbj48L3RleHQ+CiAgPHJlY3QgeD0iOTYiIHk9IjVlLTciIHdpZHRoPSI3Ny4zODciIGhlaWdodD0iNzcuMzg3IiByeT0iMTEuMzUiIGZpbGw9IiM0NDY5ZDgiIG9wYWNpdHk9Ii45OCIgc3Ryb2tlLXdpZHRoPSIwIi8+CiAgPHRleHQgeD0iMTA2LjMzMDU3IiB5PSI2NS43NjE3MTkiIGZpbGw9IiNmZmZmZmYiIGZvbnQtZmFtaWx5PSJDb3VyaWVyIiBmb250LXNpemU9IjkzLjQ4M3B4IiBzdHJva2Utd2lkdGg9IjEuMzU5NyIgc3R5bGU9ImxpbmUtaGVpZ2h0OjEuMjUiIHhtbDpzcGFjZT0icHJlc2VydmUiPjx0c3BhbiB4PSIxMDYuMzMwNTciIHk9IjY1Ljc2MTcxOSIgZmlsbD0iI2ZmZmZmZiIgZm9udC1mYW1pbHk9IkNvdXJpZXIiIHN0cm9rZS13aWR0aD0iMS4zNTk3Ij5DIDwvdHNwYW4+PC90ZXh0PgogIDxyZWN0IHg9IjE4MCIgeT0iNWUtNyIgd2lkdGg9Ijc3LjM4NyIgaGVpZ2h0PSI3Ny4zODciIHJ5PSIxMS4zNSIgZmlsbD0iIzQ0NjlkOCIgb3BhY2l0eT0iLjk4IiBzdHJva2Utd2lkdGg9IjAiLz4KICA8dGV4dCB4PSIxOTAuMzMwNTciIHk9IjY1Ljc2MTcxOSIgZmlsbD0iI2ZmZmZmZiIgZm9udC1mYW1pbHk9IkNvdXJpZXIiIGZvbnQtc2l6ZT0iOTMuNDgzcHgiIHN0cm9rZS13aWR0aD0iMS4zNTk3IiBzdHlsZT0ibGluZS1oZWlnaHQ6MS4yNSIgeG1sOnNwYWNlPSJwcmVzZXJ2ZSI+PHRzcGFuIHg9IjE5MC4zMzA1NyIgeT0iNjUuNzYxNzE5IiBmaWxsPSIjZmZmZmZmIiBmb250LWZhbWlseT0iQ291cmllciIgc3Ryb2tlLXdpZHRoPSIxLjM1OTciPkwgPC90c3Bhbj48L3RleHQ+CiAgPHJlY3QgeD0iMjY0IiB5PSI1ZS03IiB3aWR0aD0iNzcuMzg3IiBoZWlnaHQ9Ijc3LjM4NyIgcnk9IjExLjM1IiBmaWxsPSIjNDQ2OWQ4IiBvcGFjaXR5PSIuOTgiIHN0cm9rZS13aWR0aD0iMCIvPgogIDx0ZXh0IHg9IjI3NC4zMzA1NyIgeT0iNjUuNzYxNzE5IiBmaWxsPSIjZmZmZmZmIiBmb250LWZhbWlseT0iQ291cmllciIgZm9udC1zaXplPSI5My40ODNweCIgc3Ryb2tlLXdpZHRoPSIxLjM1OTciIHN0eWxlPSJsaW5lLWhlaWdodDoxLjI1IiB4bWw6c3BhY2U9InByZXNlcnZlIj48dHNwYW4geD0iMjc0LjMzMDU3IiB5PSI2NS43NjE3MTkiIGZpbGw9IiNmZmZmZmYiIGZvbnQtZmFtaWx5PSJDb3VyaWVyIiBzdHJva2Utd2lkdGg9IjEuMzU5NyI+SSA8L3RzcGFuPjwvdGV4dD4KICA8cmVjdCB4PSIzNDgiIHk9IjVlLTciIHdpZHRoPSI3Ny4zODciIGhlaWdodD0iNzcuMzg3IiByeT0iMTEuMzUiIGZpbGw9IiM0NDY5ZDgiIG9wYWNpdHk9Ii45OCIgc3Ryb2tlLXdpZHRoPSIwIi8+CiAgPHRleHQgeD0iMzU4LjMzMDU3IiB5PSI2NS43NjE3MTkiIGZpbGw9IiNmZmZmZmYiIGZvbnQtZmFtaWx5PSJDb3VyaWVyIiBmb250LXNpemU9IjkzLjQ4M3B4IiBzdHJva2Utd2lkdGg9IjEuMzU5NyIgc3R5bGU9ImxpbmUtaGVpZ2h0OjEuMjUiIHhtbDpzcGFjZT0icHJlc2VydmUiPjx0c3BhbiB4PSIzNTguMzMwNTciIHk9IjY1Ljc2MTcxOSIgZmlsbD0iI2ZmZmZmZiIgZm9udC1mYW1pbHk9IkNvdXJpZXIiIHN0cm9rZS13aWR0aD0iMS4zNTk3Ij5NIDwvdHNwYW4+PC90ZXh0PgogIDxyZWN0IHg9IjQzMiIgeT0iNWUtNyIgd2lkdGg9Ijc3LjM4NyIgaGVpZ2h0PSI3Ny4zODciIHJ5PSIxMS4zNSIgZmlsbD0iIzQ0NjlkOCIgb3BhY2l0eT0iLjk4IiBzdHJva2Utd2lkdGg9IjAiLz4KICA8dGV4dCB4PSI0NDIuMzMwNTciIHk9IjY1Ljc2MTcxOSIgZmlsbD0iI2ZmZmZmZiIgZm9udC1mYW1pbHk9IkNvdXJpZXIiIGZvbnQtc2l6ZT0iOTMuNDgzcHgiIHN0cm9rZS13aWR0aD0iMS4zNTk3IiBzdHlsZT0ibGluZS1oZWlnaHQ6MS4yNSIgeG1sOnNwYWNlPSJwcmVzZXJ2ZSI+PHRzcGFuIHg9IjQ0Mi4zMzA1NyIgeT0iNjUuNzYxNzE5IiBmaWxsPSIjZmZmZmZmIiBmb250LWZhbWlseT0iQ291cmllciIgc3Ryb2tlLXdpZHRoPSIxLjM1OTciPkIgPC90c3Bhbj48L3RleHQ+CiAgPGcgdHJhbnNmb3JtPSJ0cmFuc2xhdGUoMiAxLjUzNzYpIj4KICAgPHJlY3QgeD0iNjI0IiB5PSItMS41Mzc2IiB3aWR0aD0iNzcuMzg3IiBoZWlnaHQ9Ijc3LjM4NyIgcnk9IjExLjM1IiBmaWxsPSIjNDQ2OWQ4IiBvcGFjaXR5PSIuOTgiIHN0cm9rZS13aWR0aD0iMCIvPgogICA8dGV4dCB4PSI2MzQuMzMwNTciIHk9IjY0LjIyNDE2NyIgZmlsbD0iI2ZmZmZmZiIgZm9udC1mYW1pbHk9IkNvdXJpZXIiIGZvbnQtc2l6ZT0iOTMuNDgzcHgiIHN0cm9rZS13aWR0aD0iMS4zNTk3IiBzdHlsZT0ibGluZS1oZWlnaHQ6MS4yNSIgeG1sOnNwYWNlPSJwcmVzZXJ2ZSI+PHRzcGFuIHg9IjYzNC4zMzA1NyIgeT0iNjQuMjI0MTY3IiBmaWxsPSIjZmZmZmZmIiBmb250LWZhbWlseT0iQ291cmllciIgc3Ryb2tlLXdpZHRoPSIxLjM1OTciPlQgPC90c3Bhbj48L3RleHQ+CiAgIDxyZWN0IHg9IjcwOCIgeT0iLTEuNTM3NiIgd2lkdGg9Ijc3LjM4NyIgaGVpZ2h0PSI3Ny4zODciIHJ5PSIxMS4zNSIgZmlsbD0iIzQ0NjlkOCIgb3BhY2l0eT0iLjk4IiBzdHJva2Utd2lkdGg9IjAiLz4KICAgPHRleHQgeD0iNzE4LjMzMDU3IiB5PSI2NC4yMjQxNjciIGZpbGw9IiNmZmZmZmYiIGZvbnQtZmFtaWx5PSJDb3VyaWVyIiBmb250LXNpemU9IjkzLjQ4M3B4IiBzdHJva2Utd2lkdGg9IjEuMzU5NyIgc3R5bGU9ImxpbmUtaGVpZ2h0OjEuMjUiIHhtbDpzcGFjZT0icHJlc2VydmUiPjx0c3BhbiB4PSI3MTguMzMwNTciIHk9IjY0LjIyNDE2NyIgZmlsbD0iI2ZmZmZmZiIgZm9udC1mYW1pbHk9IkNvdXJpZXIiIHN0cm9rZS13aWR0aD0iMS4zNTk3Ij5SIDwvdHNwYW4+PC90ZXh0PgogICA8cmVjdCB4PSI3OTIiIHk9Ii0xLjUzNzYiIHdpZHRoPSI3Ny4zODciIGhlaWdodD0iNzcuMzg3IiByeT0iMTEuMzUiIGZpbGw9IiM0NDY5ZDgiIG9wYWNpdHk9Ii45OCIgc3Ryb2tlLXdpZHRoPSIwIi8+CiAgIDx0ZXh0IHg9IjgwMi4zMzA1NyIgeT0iNjQuMjI0MTY3IiBmaWxsPSIjZmZmZmZmIiBmb250LWZhbWlseT0iQ291cmllciIgZm9udC1zaXplPSI5My40ODNweCIgc3Ryb2tlLXdpZHRoPSIxLjM1OTciIHN0eWxlPSJsaW5lLWhlaWdodDoxLjI1IiB4bWw6c3BhY2U9InByZXNlcnZlIj48dHNwYW4geD0iODAyLjMzMDU3IiB5PSI2NC4yMjQxNjciIGZpbGw9IiNmZmZmZmYiIGZvbnQtZmFtaWx5PSJDb3VyaWVyIiBzdHJva2Utd2lkdGg9IjEuMzU5NyI+RTwvdHNwYW4+PC90ZXh0PgogICA8cmVjdCB4PSI4NzYiIHk9Ii0xLjUzNzYiIHdpZHRoPSI3Ny4zODciIGhlaWdodD0iNzcuMzg3IiByeT0iMTEuMzUiIGZpbGw9IiM0NDY5ZDgiIG9wYWNpdHk9Ii45OCIgc3Ryb2tlLXdpZHRoPSIwIi8+CiAgIDx0ZXh0IHg9Ijg4Ni4zMzA1NyIgeT0iNjQuMjI0MTY3IiBmaWxsPSIjZmZmZmZmIiBmb250LWZhbWlseT0iQ291cmllciIgZm9udC1zaXplPSI5My40ODNweCIgc3Ryb2tlLXdpZHRoPSIxLjM1OTciIHN0eWxlPSJsaW5lLWhlaWdodDoxLjI1IiB4bWw6c3BhY2U9InByZXNlcnZlIj48dHNwYW4geD0iODg2LjMzMDU3IiB5PSI2NC4yMjQxNjciIGZpbGw9IiNmZmZmZmYiIGZvbnQtZmFtaWx5PSJDb3VyaWVyIiBzdHJva2Utd2lkdGg9IjEuMzU5NyI+RSA8L3RzcGFuPjwvdGV4dD4KICAgPHJlY3QgeD0iOTYwIiB5PSItMS41Mzc2IiB3aWR0aD0iNzcuMzg3IiBoZWlnaHQ9Ijc3LjM4NyIgcnk9IjExLjM1IiBmaWxsPSIjNDQ2OWQ4IiBvcGFjaXR5PSIuOTgiIHN0cm9rZS13aWR0aD0iMCIvPgogICA8dGV4dCB4PSI5NzAuMzMwNTciIHk9IjY0LjIyNDE2NyIgZmlsbD0iI2ZmZmZmZiIgZm9udC1mYW1pbHk9IkNvdXJpZXIiIGZvbnQtc2l6ZT0iOTMuNDgzcHgiIHN0cm9rZS13aWR0aD0iMS4zNTk3IiBzdHlsZT0ibGluZS1oZWlnaHQ6MS4yNSIgeG1sOnNwYWNlPSJwcmVzZXJ2ZSI+PHRzcGFuIHg9Ijk3MC4zMzA1NyIgeT0iNjQuMjI0MTY3IiBmaWxsPSIjZmZmZmZmIiBmb250LWZhbWlseT0iQ291cmllciIgc3Ryb2tlLXdpZHRoPSIxLjM1OTciPlMgPC90c3Bhbj48L3RleHQ+CiAgPC9nPgogIDxnIHRyYW5zZm9ybT0ibWF0cml4KDEuMDQ5OSAwIDAgMS4wNDk5IC0yOC4wOTIgLS4yNzI5MykiIGZpbGw9IiM0NDY5ZDgiIHN0cm9rZT0iI2ZkZmZmZiI+CiAgIDxyZWN0IHg9IjUyOCIgeT0iLTEuNTM3NiIgd2lkdGg9Ijc3LjM4NyIgaGVpZ2h0PSI3Ny4zODciIHJ5PSIxMS4zNSIgb3BhY2l0eT0iLjk4IiBzdHJva2Utd2lkdGg9IjUuMTgiLz4KICAgPGcgdHJhbnNmb3JtPSJtYXRyaXgoLjc0NTkyIDAgMCAuNzQzNjcgNTMwLjg0IDEuNjc0NCkiIHN0cm9rZS13aWR0aD0iNS4yMTYyIiBmZWF0dXJlS2V5PSJpbmxpbmVTeW1ib2xGZWF0dXJlLTAiPgogICAgPGcgZmlsbD0iIzQ0NjlkOCIgc3Ryb2tlPSIjZmRmZmZmIiBzdHJva2Utd2lkdGg9IjUuMjE2MiI+CiAgICAgPGcgZmlsbD0iIzQ0NjlkOCIgc3Ryb2tlPSIjZmRmZmZmIiBzdHJva2Utd2lkdGg9IjUuMjE2MiI+CiAgICAgIDxwYXRoIGQ9Im00Ny42NTkgODEuNDI3YzAuMzU4LTcuOTgxIDEuMzMzLTE1LjkxNyAxLjE1Mi0yMy45MTctMC4wMS0wLjQyNS0wLjU0NC0wLjg0My0wLjk0LTAuNTQtMi4zNTYgMS44MDEtNC44MTEgMy4yMTktNy42NjQgNC4xMDQtMy42NDkgMS4xMzItNy43MDMtMi4zMjgtNS44MTQtNS45ODEgMC43NTgtMS40NjYgMi4xNDYtMi43MDggMy40NDctMy42NzIgMC40NjctMC4zNDYgMC4zNTgtMS4xNzYtMC4zMTUtMS4xNjUtMy4xNTQgMC4wNTQtMTAuODM1IDEuMTQ5LTEwLjA0Mi00LjM4NiAwLjQ4MS0zLjM2NSA2LjI5LTUuNDU4IDguOTE3LTYuODQgMC4zMzMtMC4xNzUgMC40MzUtMC43MyAwLjEyNy0wLjk4MS02LjY2My01LjQzMS0zLjA2OS0xNC42NDcgNS43MzEtMTIuNzg4IDAuMjcyIDAuMDU4IDAuNTYzLTAuMDMzIDAuNzA2LTAuMjg3IDIuMjM1LTMuOTk1IDQuMjc2LTguMDYzIDcuMTA2LTExLjY4OC0wLjM1Ni0wLjE0Ny0wLjcxMi0wLjI5NC0xLjA2Ny0wLjQ0MiAwLjI5NCAzLjExNiAyLjAzNiA1LjI2OSA0LjMzNyA3LjI3MiAyLjQ1OSAyLjE0MiA3LjYzNCA0LjI3IDguMDg1IDcuODQ1IDAuNDgxIDMuODIxLTYuNTQ5IDQuMzU2LTYuMDU0IDcuNTg4IDAuMzMgMi4xNDcgMS4zNTQgMy40MjMgMy4wMjEgNC43NCAxLjA1MiAwLjgzMSAxLjk2OCAxLjQwNSAzLjAxNyAyLjMyOSAxLjgxOCAyLjAzNiAxLjU5NiA0LjIyMy0wLjY2NyA2LjU2MS0xLjQ4NiAwLjI1Mi0yLjkyNyAwLjEzOC00LjMyLTAuMzQxLTAuNTU2LTAuMTQ0LTAuOTQ1IDAuNDM1LTAuNzA2IDAuOTE4IDEuNDEyIDIuODQyIDMuMjMgNS40NDkgMy41MjkgOC43MDcgMC44MjEgOC45NjktNy4yMzcgMS43NDgtOC4xMyAwLjg3NS0wLjgxMy0wLjc5My0xLjYtMS41NjEtMi40ODYtMi4yNy0wLjYyMy0wLjQ5OC0xLjUxNCAwLjM4LTAuODg1IDAuODg0IDMuMzk5IDIuNzE3IDYuNTA3IDcuNzgyIDExLjEzMiA0LjQyIDQuMzIzLTMuMTQyLTAuNTI0LTEwLjExNC0yLjA4LTEzLjI0Ni0wLjIzNSAwLjMwNi0wLjQ3MSAwLjYxMi0wLjcwNiAwLjkxOCAzLjkgMS4wMSA4LjIzMSAwLjQ0NyA3Ljk0MS00LjQ1Mi0wLjExNy0xLjk3My0xLjI1OS0zLjY0NC0yLjgtNC43NzgtMS40NjgtMS4wODEtNi43MjktNC4yMzQtMy42OC02LjQxIDEuMjYxLTAuODk5IDIuNDUzLTEuODI2IDMuNTQ4LTIuOTI5IDIuMjk0LTIuMzExIDEuNzI2LTQuOTQtMC4zMjYtNy4xMDUtMy41MzUtMy43MzItOS45Ny01LjY4Mi0xMC41MjEtMTEuNTI1LTAuMDQ0LTAuNDctMC42OTItMC45MjEtMS4wNjctMC40NDItMS4yNjcgMS42MjItNi4yNjUgMTEuNzI0LTcuODQxIDExLjM5MS0yLjIzNC0wLjQ3Mi00LjQ4NSAwLjA2LTYuNDE4IDEuMTg2LTQuMTA1IDIuMzkxLTMuOTE5IDcuOTAzLTEuNzM4IDExLjQ0OCAwLjEyMiAwLjE5OSAxLjUxNyAyLjA4NCAxLjc4MiAxLjk0NC0xLjY4MiAwLjg4NS0zLjM1MSAxLjczNy00Ljk1MSAyLjc2OC0xLjY2NCAxLjA3Mi00LjE3NyAzLjI2Mi0zLjkwNCA1LjU0IDAuNjcxIDUuNjE5IDcuMTQ0IDQuOTAyIDExLjQwOSA0LjgyOS0wLjEwNS0wLjM4OC0wLjIxLTAuNzc2LTAuMzE1LTEuMTY1LTMuNTYgMi42MzYtOC41OCAxMS4zODEtMC41NjIgMTIuMTc0IDIuMzQgMC4yMzEgNC4yNDctMC4yNTkgNi40MjMtMS4xNDIgMC44ODMtMC4zNTggMS42OTgtMC44NDUgMi41MjUtMS4zMTEgMC43NzUtMC40MzcgMS45NzYtMi4xMjIgMi4wMDgtMC42OTIgMC4xNjYgNy4zNTctMC44NjUgMTQuNzE0LTEuMTk0IDIyLjA1Ni0wLjAzNiAwLjgwNCAxLjIxNCAwLjgwMSAxLjI1LTJlLTN6IiBmaWxsPSIjNDQ2OWQ4IiBzdHJva2U9IiNmZGZmZmYiIHN0cm9rZS1saW5lam9pbj0icm91bmQiIHN0cm9rZS13aWR0aD0iNS4yMTYyIi8+CiAgICAgPC9nPgogICAgIDxnIGZpbGw9IiM0NDY5ZDgiIHN0cm9rZT0iI2ZkZmZmZiIgc3Ryb2tlLXdpZHRoPSI1LjIxNjIiPgogICAgICA8cGF0aCBkPSJtMjIuMzAxIDgzLjE1NmMtMC40NDEtNi4wMzItMS4wNzItMTIuNjE4IDAuMjY2LTE4LjU2NCAwLjEzOC0wLjYxMy0wLjU3OC0xLjA0Mi0xLjA0NS0wLjYwOC0xLjc0MyAxLjYyNS0zLjQ0MyAyLjgzMS01LjczMiAzLjYwNC02LjM0LTMuMzkzLTcuOTEzLTYuMzczLTQuNzE3LTguOTM5IDAuOTg4LTAuODU2IDIuMDM0LTEuNjMzIDMuMTM5LTIuMzI5IDAuMjg3LTAuMTkxIDAuMzk3LTAuNTQ0IDAuMjI1LTAuODU1LTAuNjU4LTEuMTc4LTEuMzkyLTIuMTYzLTIuMjUxLTMuMTkxLTQuMzk3LTUuMjY0LTAuMzgyLTkuNDE0IDQuNzU5LTEwLjg3NSAwLjI3MS0wLjA3NyAwLjQ1NS0wLjMyMiAwLjQ1OS0wLjYwMyAwLjAzNi0yLjg2NCAwLjMxMy01LjY0MiAxLjA5NC04LjQwNyAxLjg2NS02LjYwNiAxMC4yNTUtOS4xODEgMTMuMTQzLTEuNDg3IDAuMjggMC43NDggMS40ODkgMC40MjQgMS4yMDUtMC4zMzItMi41MTctNi43MDYtOS41NzQtNy42NDktMTMuOTE4LTIuMDAzLTIuMzA1IDIuOTk2LTIuNjEgNy40NjYtMi43NTkgMTEuMDg0LTAuMDM1IDAuODUtMy44MzkgMi4yNjktNC40OTYgMi42OTQtMS4wMzQgMC42NjktMi4yMTkgMi4wOTgtMi40NSAzLjMxMi0wLjgwOCA0LjIzMyAxLjEwMyA2LjA1NiAzLjUxMiA5LjMyMyAwLjQwNSAwLjU0OC01LjMyNyA1LjI1Mi01LjMxNyA3LjI3OSAwLjAxNiAzLjQ2OCAyLjQ1NSA1LjY0IDUuNjA1IDYuNjQ1IDMuNDA0IDEuMDg2IDcuMTI3LTEuOTMyIDkuMzg2LTQuMDM3LTAuMzQ5LTAuMjAzLTAuNjk3LTAuNDA1LTEuMDQ1LTAuNjA4LTEuMzY4IDYuMDc5LTAuNzYyIDEyLjczNC0wLjMxMSAxOC44OTYgMC4wNTYgMC44IDEuMzA2IDAuODA2IDEuMjQ4IDFlLTN6IiBmaWxsPSIjNDQ2OWQ4IiBzdHJva2U9IiNmZGZmZmYiIHN0cm9rZS1saW5lam9pbj0icm91bmQiIHN0cm9rZS13aWR0aD0iNS4yMTYyIi8+CiAgICAgPC9nPgogICAgIDxnIGZpbGw9IiM0NDY5ZDgiIHN0cm9rZT0iI2ZkZmZmZiIgc3Ryb2tlLXdpZHRoPSI1LjIxNjIiPgogICAgICA8cGF0aCBkPSJtMjEuNDI0IDY0Ljc0MWMxLjk4MyAyLjcwNyA0Ljk4MSA0LjE5OSA4LjM0OSAzLjYzNyAzLjU5NC0wLjYgNS4xOTEtNC4xMyA1LjI5MS03LjQxMSAwLjAyNC0wLjgwNy0xLjIyNi0wLjgwNC0xLjI1IDAtMC4yMDIgNi42Ny03LjUyMyA4LjMxMy0xMS4zMSAzLjE0My0wLjQ3Mi0wLjY0My0xLjU1Ny0wLjAyLTEuMDggMC42MzF6IiBmaWxsPSIjNDQ2OWQ4IiBzdHJva2U9IiNmZGZmZmYiIHN0cm9rZS13aWR0aD0iNS4yMTYyIi8+CiAgICAgPC9nPgogICAgIDxnIGZpbGw9IiM0NDY5ZDgiIHN0cm9rZT0iI2ZkZmZmZiIgc3Ryb2tlLXdpZHRoPSI1LjIxNjIiPgogICAgICA8cGF0aCBkPSJtNzQuNjYxIDgwLjg3OGMyLjg2OS01LjQwNiAzLjI1MS0xMi4xOTEgMi42NzktMTguMTgyLTAuMDM2LTAuMzgxLTAuMzc1LTAuNzQyLTAuNzkxLTAuNjAzLTEuNDgyIDAuNDk2LTkuNjc3IDEuODQtNS42MzQtNC41NTcgMC4yNTEtMC4zOTctMC4wNzUtMC45NTItMC41NC0wLjk0LTQuOTEzIDAuMTIzLTkuMjMzLTAuOTM3LTkuNTctNi42ODMtMC4wNDctMC44MDEtMS4yOTctMC44MDYtMS4yNSAwIDAuMjAxIDMuNDI2IDEuMzc1IDUuODI4IDQuNjIyIDcuMjE0IDEuNTE0IDAuNjQ2IDMuMjc4IDAuNyA0Ljg5NCAwLjc1MS0wLjY1OC0wLjAyMS0wLjMzOCAzLjA3NC0wLjIxNiAzLjQ4OSAwLjYyNSAyLjEzIDQuMTAxIDIuNzczIDUuODk2IDIuNDY2IDIuNjA2LTAuNDQ2IDEuNTUxIDMuMjg4IDEuNDc3IDUuMTc3LTAuMTUgMy44MzMtMC44MzIgNy44Mi0yLjY0NiAxMS4yMzYtMC4zNzggMC43MTMgMC43MDEgMS4zNDUgMS4wNzkgMC42MzJ6IiBmaWxsPSIjNDQ2OWQ4IiBzdHJva2U9IiNmZGZmZmYiIHN0cm9rZS13aWR0aD0iNS4yMTYyIi8+CiAgICAgPC9nPgogICAgIDxnIGZpbGw9IiM0NDY5ZDgiIHN0cm9rZT0iI2ZkZmZmZiIgc3Ryb2tlLXdpZHRoPSI1LjIxNjIiPgogICAgICA8cGF0aCBkPSJtNzYuODgxIDYzLjI5OWMzLjM0MS0wLjYxOCA3LjQyNS0xLjM3MiA3LjQyMy01LjY3IDAtMS40NzMtMC4xNDEtMy40NjItMS40MDMtNC40ODYgMC41MjQgMC40MjUgMi43MDMtMS4yODcgMy4zODEtMS44ODUgNS4wOTctNC40OTkgMS42MDctMTIuNTg1LTQuMzAxLTEzLjg1LTAuMjIyLTAuMDQ3IDIuMjE2LTQuNSAyLjUxNS01LjE1NyAwLjgzMi0xLjgzNCAwLjYxNC0zLjYzNC04ZS0zIC01LjQ3Mi0xLjEzMy0zLjM0Ny02LjMyNy05LjA2LTEwLjE1My05LjI4My0xLjQxMS0wLjA4Mi0yLjQ0OS0wLjA3Ny0zLjUxNSAwLjg4MS0xLjIxMiAxLjA5IDAuODQyIDMuOTgtMS45NjMgMi40ODQtNC44Mi0yLjU3My01LjEyNSAyLjI1LTcuODU2IDQuODUyLTAuNTg0IDAuNTU3IDAuMzAxIDEuNDM5IDAuODg1IDAuODg0IDEuMTk5LTEuMTQzIDAuOTYxLTAuNzM2IDEuNTc0LTIuMDI2IDIuMjAyLTQuNjQxIDQuNzY4LTIuNTg5IDcuMTc4LTEuMzg4IDAuMzM0IDAuMTY3IDAuODM5IDAuMDQ3IDAuOTE4LTAuMzc0IDAuMjA4LTEuMDk4IDAuMjA1LTEuMDI1IDAuMTg2LTIuMTY5IDIuNzg3LTEuODQgNS4wODQtMS41OTYgNi44OTEgMC43MzEgMC43NDUgMC43MTUgMS40NDkgMS40NjkgMi4xMTMgMi4yNjEgNC44NzQgNS41MDcgMi4wOTcgOC44MzMtMC41MzUgMTMuOTY4LTAuMjI4IDAuNDQ1IDAuMDYgMC44OTcgMC41NCAwLjk0IDguMzY4IDAuNzQ5IDguNjg0IDExLjk4MyAwLjY5OCAxMy43NTctMC40MzIgMC4wOTYtMC42NCAwLjc1LTAuMjc2IDEuMDQ0IDQuOTkgNC4wNDYtMC4zODYgNy45NjktNC42MjIgOC43NTMtMC43OTQgMC4xNDctMC40NTggMS4zNTEgMC4zMyAxLjIwNXoiIGZpbGw9IiM0NDY5ZDgiIHN0cm9rZT0iI2ZkZmZmZiIgc3Ryb2tlLWxpbmVqb2luPSJyb3VuZCIgc3Ryb2tlLXdpZHRoPSI1LjIxNjIiLz4KICAgICA8L2c+CiAgICA8L2c+CiAgIDwvZz4KICA8L2c+CiA8L2c+Cjwvc3ZnPgo=\">"
|
|
],
|
|
"metadata": {
|
|
"id": "QjHXD27ieTS-"
|
|
}
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"source": [
|
|
"# Graph coloring\n",
|
|
"\n",
|
|
"The purpose of this Python notebook is to use investigate using SAT to solve Sudoku problems. \n",
|
|
"\n",
|
|
"You should have completed the notebook on SAT constructions before attempting this notebook.\n",
|
|
"\n",
|
|
"You can save a local copy of this notebook in your Google account and work through it in Colab (recommended) or you can download the notebook and run it locally using Jupyter notebook or similar.\n",
|
|
"\n",
|
|
"Contact me at iclimbtreesmail@gmail.com if you find any mistakes or have any suggestions."
|
|
],
|
|
"metadata": {
|
|
"id": "jtMs90veeZIn"
|
|
}
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"source": [
|
|
"# Install relevant packages\n",
|
|
"!pip install z3-solver\n",
|
|
"from z3 import *\n",
|
|
"import numpy as np\n",
|
|
"import geopandas as gpd\n",
|
|
"import matplotlib.pyplot as plt"
|
|
],
|
|
"metadata": {
|
|
"id": "mF6ngqCses3n",
|
|
"colab": {
|
|
"base_uri": "https://localhost:8080/"
|
|
},
|
|
"outputId": "fad1115b-b146-46bc-b298-7c0885fe75ac"
|
|
},
|
|
"execution_count": 1,
|
|
"outputs": [
|
|
{
|
|
"output_type": "stream",
|
|
"name": "stdout",
|
|
"text": [
|
|
"Collecting z3-solver\n",
|
|
" Downloading z3_solver-4.14.1.0-py3-none-manylinux_2_17_x86_64.manylinux2014_x86_64.whl.metadata (602 bytes)\n",
|
|
"Downloading z3_solver-4.14.1.0-py3-none-manylinux_2_17_x86_64.manylinux2014_x86_64.whl (29.5 MB)\n",
|
|
"\u001b[2K \u001b[90m━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━\u001b[0m \u001b[32m29.5/29.5 MB\u001b[0m \u001b[31m17.6 MB/s\u001b[0m eta \u001b[36m0:00:00\u001b[0m\n",
|
|
"\u001b[?25hInstalling collected packages: z3-solver\n",
|
|
"Successfully installed z3-solver-4.14.1.0\n"
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"source": [
|
|
"Now let's define a Sudoku problem. We'll make a 9x9 matrix use zeros to represent unknown values."
|
|
],
|
|
"metadata": {
|
|
"id": "3A5_7mByYrur"
|
|
}
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"source": [
|
|
"puzzle = [[0,0,9,4,2,0,0,6,0],\n",
|
|
" [0,7,0,9,0,5,3,0,2],\n",
|
|
" [5,0,0,0,0,3,0,9,0],\n",
|
|
" [0,0,0,8,0,1,0,2,0],\n",
|
|
" [2,6,0,0,0,0,0,5,1],\n",
|
|
" [0,1,8,2,0,0,4,0,0],\n",
|
|
" [3,8,0,0,0,4,0,1,9],\n",
|
|
" [0,9,4,0,3,0,6,8,5],\n",
|
|
" [0,2,1,0,0,8,0,3,0]]"
|
|
],
|
|
"metadata": {
|
|
"id": "cvGNbKkf-Qix"
|
|
},
|
|
"execution_count": 2,
|
|
"outputs": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"source": [
|
|
"def expandLine(line):\n",
|
|
" return line[0]+line[5:9].join([line[1:5]*2]*3)+line[9:13]\n",
|
|
"\n",
|
|
"def drawPuzzle(puzzle):\n",
|
|
" line0 = expandLine(\"╔═══╤═══╦═══╗\")\n",
|
|
" line1 = expandLine(\"║ . │ . ║ . ║\")\n",
|
|
" line2 = expandLine(\"╟───┼───╫───╢\")\n",
|
|
" line3 = expandLine(\"╠═══╪═══╬═══╣\")\n",
|
|
" line4 = expandLine(\"╚═══╧═══╩═══╝\")\n",
|
|
"\n",
|
|
" symbol = \" 123456789\"\n",
|
|
" nums = [ [\"\"]+[symbol[n] for n in row] for row in puzzle ]\n",
|
|
" print(line0)\n",
|
|
" for r in range(1,9+1):\n",
|
|
" print( \"\".join(n+s for n,s in zip(nums[r-1],line1.split(\".\"))) )\n",
|
|
" print([line2,line3,line4][(r%9==0)+(r%3==0)])"
|
|
],
|
|
"metadata": {
|
|
"id": "0EkPFukj_-qc"
|
|
},
|
|
"execution_count": 3,
|
|
"outputs": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"source": [
|
|
"drawPuzzle(puzzle)"
|
|
],
|
|
"metadata": {
|
|
"colab": {
|
|
"base_uri": "https://localhost:8080/"
|
|
},
|
|
"id": "CB0QFnLODWTu",
|
|
"outputId": "3698caa2-e0a2-466a-a542-5e141d7b6bce"
|
|
},
|
|
"execution_count": 4,
|
|
"outputs": [
|
|
{
|
|
"output_type": "stream",
|
|
"name": "stdout",
|
|
"text": [
|
|
"╔═══╤═══╤═══╦═══╤═══╤═══╦═══╤═══╤═══╗\n",
|
|
"║ │ │ 9 ║ 4 │ 2 │ ║ │ 6 │ ║\n",
|
|
"╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n",
|
|
"║ │ 7 │ ║ 9 │ │ 5 ║ 3 │ │ 2 ║\n",
|
|
"╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n",
|
|
"║ 5 │ │ ║ │ │ 3 ║ │ 9 │ ║\n",
|
|
"╠═══╪═══╪═══╬═══╪═══╪═══╬═══╪═══╪═══╣\n",
|
|
"║ │ │ ║ 8 │ │ 1 ║ │ 2 │ ║\n",
|
|
"╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n",
|
|
"║ 2 │ 6 │ ║ │ │ ║ │ 5 │ 1 ║\n",
|
|
"╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n",
|
|
"║ │ 1 │ 8 ║ 2 │ │ ║ 4 │ │ ║\n",
|
|
"╠═══╪═══╪═══╬═══╪═══╪═══╬═══╪═══╪═══╣\n",
|
|
"║ 3 │ 8 │ ║ │ │ 4 ║ │ 1 │ 9 ║\n",
|
|
"╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n",
|
|
"║ │ 9 │ 4 ║ │ 3 │ ║ 6 │ 8 │ 5 ║\n",
|
|
"╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n",
|
|
"║ │ 2 │ 1 ║ │ │ 8 ║ │ 3 │ ║\n",
|
|
"╚═══╧═══╧═══╩═══╧═══╧═══╩═══╧═══╧═══╝\n"
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"source": [
|
|
"# Takes a list of z3.Bool variables and returns constraints\n",
|
|
"# ensuring that there is exactly one true\n",
|
|
"def exactly_one(x):\n",
|
|
" return PbEq([(i,1) for i in x],1)\n",
|
|
"\n",
|
|
"def solve_soduku(puzzle):\n",
|
|
" # Create a 9 x 9 x 9 structure containing Boolean variables\n",
|
|
" # If position (i,j,k) is true, this means position (i,j) in the puzzle matrix\n",
|
|
" # takes color k\n",
|
|
" x = [[[ z3.Bool(\"x_{%d,%d,%d}\"%((i,j,k))) for k in range(0,9)] for j in range(0,9) ] for i in range(0,9) ]\n",
|
|
" # Set up the sat solver\n",
|
|
" s = Solver()\n",
|
|
"\n",
|
|
" # Add constraint one: each position where the entry is already known\n",
|
|
" # should be set to true.\n",
|
|
" for i in range(0,9):\n",
|
|
" for j in range(0,9):\n",
|
|
" if puzzle[i][j] > 0:\n",
|
|
" s.add(x[i][j][puzzle[i][j]-1] == True)\n",
|
|
"\n",
|
|
"\n",
|
|
" # Add constraint two: each position in the matrix can have only one color\n",
|
|
" # For fixed i and j, only one value of k can be true\n",
|
|
" for i in range(0,9):\n",
|
|
" for j in range(0,9):\n",
|
|
" s.add(exactly_one([x[i][j][k] for k in range(0,9)]))\n",
|
|
"\n",
|
|
" # Add constraint three: each row of the table can only have each value once\n",
|
|
" for i in range(0,9):\n",
|
|
" for k in range(0,9):\n",
|
|
" s.add(exactly_one([x[i][j][k] for j in range(0,9)]))\n",
|
|
"\n",
|
|
" # Add constraint four: each column of the table can only have each value once\n",
|
|
" for j in range(0,9):\n",
|
|
" for k in range(0,9):\n",
|
|
" s.add(exactly_one([x[i][j][k] for i in range(0,9)]))\n",
|
|
"\n",
|
|
" # Add constraint five: each 3x3 region can only have each value once\n",
|
|
" for i in range(0,9,3):\n",
|
|
" for j in range(0,9,3):\n",
|
|
" for k in range(0,9):\n",
|
|
" s.add(exactly_one([x[i+a][j+b][k] for a in range(0,3) for b in range(0,3)]))\n",
|
|
"\n",
|
|
" # Check if it's SAT (creates the model)\n",
|
|
" sat_result = s.check()\n",
|
|
" print(sat_result)\n",
|
|
"\n",
|
|
" # If it isn't then return\n",
|
|
" if sat_result == z3.sat:\n",
|
|
" result = s.model()\n",
|
|
" x_vals = np.array([[[int(bool(result[z3.Bool(\"x_{%d,%d,%d}\" % (i, j, k))])) for k in range(9)] for j in range(9)] for i in range(9)] )\n",
|
|
" solution = np.argmax(x_vals, axis=2) + 1\n",
|
|
" drawPuzzle(solution)\n",
|
|
" else:\n",
|
|
" print(\"No solution\")\n",
|
|
"\n"
|
|
],
|
|
"metadata": {
|
|
"id": "dRmdNKGdZRks"
|
|
},
|
|
"execution_count": 23,
|
|
"outputs": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"source": [
|
|
"# Call the routine to solve the Soduku puzzle\n",
|
|
"solve_soduku(puzzle)"
|
|
],
|
|
"metadata": {
|
|
"id": "0HeFo62NZfBp",
|
|
"colab": {
|
|
"base_uri": "https://localhost:8080/"
|
|
},
|
|
"outputId": "8840695c-8ce0-4ce1-93ef-d68d1c7098ed"
|
|
},
|
|
"execution_count": 24,
|
|
"outputs": [
|
|
{
|
|
"output_type": "stream",
|
|
"name": "stdout",
|
|
"text": [
|
|
"sat\n",
|
|
"╔═══╤═══╤═══╦═══╤═══╤═══╦═══╤═══╤═══╗\n",
|
|
"║ 1 │ 3 │ 9 ║ 4 │ 2 │ 7 ║ 5 │ 6 │ 8 ║\n",
|
|
"╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n",
|
|
"║ 8 │ 7 │ 6 ║ 9 │ 1 │ 5 ║ 3 │ 4 │ 2 ║\n",
|
|
"╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n",
|
|
"║ 5 │ 4 │ 2 ║ 6 │ 8 │ 3 ║ 1 │ 9 │ 7 ║\n",
|
|
"╠═══╪═══╪═══╬═══╪═══╪═══╬═══╪═══╪═══╣\n",
|
|
"║ 4 │ 5 │ 3 ║ 8 │ 7 │ 1 ║ 9 │ 2 │ 6 ║\n",
|
|
"╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n",
|
|
"║ 2 │ 6 │ 7 ║ 3 │ 4 │ 9 ║ 8 │ 5 │ 1 ║\n",
|
|
"╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n",
|
|
"║ 9 │ 1 │ 8 ║ 2 │ 5 │ 6 ║ 4 │ 7 │ 3 ║\n",
|
|
"╠═══╪═══╪═══╬═══╪═══╪═══╬═══╪═══╪═══╣\n",
|
|
"║ 3 │ 8 │ 5 ║ 7 │ 6 │ 4 ║ 2 │ 1 │ 9 ║\n",
|
|
"╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n",
|
|
"║ 7 │ 9 │ 4 ║ 1 │ 3 │ 2 ║ 6 │ 8 │ 5 ║\n",
|
|
"╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n",
|
|
"║ 6 │ 2 │ 1 ║ 5 │ 9 │ 8 ║ 7 │ 3 │ 4 ║\n",
|
|
"╚═══╧═══╧═══╩═══╧═══╧═══╩═══╧═══╧═══╝\n"
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"source": [
|
|
"Now let's try it with a more difficult example. Try to solve this yourself and you'll see that it's pretty hard."
|
|
],
|
|
"metadata": {
|
|
"id": "vL-sDmF7tnxa"
|
|
}
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"source": [
|
|
"puzzle2 = [[0,5,0,0,0,9,0,8,0],\n",
|
|
" [7,0,0,0,0,3,6,0,5],\n",
|
|
" [0,0,0,0,6,0,0,1,0],\n",
|
|
" [0,0,0,0,0,0,0,6,0],\n",
|
|
" [0,1,0,0,3,0,4,0,9],\n",
|
|
" [0,0,2,0,0,7,0,0,0],\n",
|
|
" [0,9,0,0,4,0,5,0,3],\n",
|
|
" [1,0,0,9,0,0,0,0,0],\n",
|
|
" [0,0,0,0,0,0,0,0,8]]\n",
|
|
"drawPuzzle(puzzle2)\n",
|
|
"solve_soduku(puzzle2)"
|
|
],
|
|
"metadata": {
|
|
"colab": {
|
|
"base_uri": "https://localhost:8080/"
|
|
},
|
|
"id": "3SWS2QUqtlNI",
|
|
"outputId": "8c7419ff-70b2-4322-81c0-2f8d8727de72"
|
|
},
|
|
"execution_count": 32,
|
|
"outputs": [
|
|
{
|
|
"output_type": "stream",
|
|
"name": "stdout",
|
|
"text": [
|
|
"╔═══╤═══╤═══╦═══╤═══╤═══╦═══╤═══╤═══╗\n",
|
|
"║ │ 5 │ ║ │ │ 9 ║ │ 8 │ ║\n",
|
|
"╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n",
|
|
"║ 7 │ │ ║ │ │ 3 ║ 6 │ │ 5 ║\n",
|
|
"╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n",
|
|
"║ │ │ ║ │ 6 │ ║ │ 1 │ ║\n",
|
|
"╠═══╪═══╪═══╬═══╪═══╪═══╬═══╪═══╪═══╣\n",
|
|
"║ │ │ ║ │ │ ║ │ 6 │ ║\n",
|
|
"╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n",
|
|
"║ │ 1 │ ║ │ 3 │ ║ 4 │ │ 9 ║\n",
|
|
"╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n",
|
|
"║ │ │ 2 ║ │ │ 7 ║ │ │ ║\n",
|
|
"╠═══╪═══╪═══╬═══╪═══╪═══╬═══╪═══╪═══╣\n",
|
|
"║ │ 9 │ ║ │ 4 │ ║ 5 │ │ 3 ║\n",
|
|
"╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n",
|
|
"║ 1 │ │ ║ 9 │ │ ║ │ │ ║\n",
|
|
"╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n",
|
|
"║ │ │ ║ │ │ ║ │ │ 8 ║\n",
|
|
"╚═══╧═══╧═══╩═══╧═══╧═══╩═══╧═══╧═══╝\n",
|
|
"sat\n",
|
|
"╔═══╤═══╤═══╦═══╤═══╤═══╦═══╤═══╤═══╗\n",
|
|
"║ 6 │ 5 │ 1 ║ 7 │ 2 │ 9 ║ 3 │ 8 │ 4 ║\n",
|
|
"╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n",
|
|
"║ 7 │ 8 │ 9 ║ 4 │ 1 │ 3 ║ 6 │ 2 │ 5 ║\n",
|
|
"╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n",
|
|
"║ 3 │ 2 │ 4 ║ 8 │ 6 │ 5 ║ 9 │ 1 │ 7 ║\n",
|
|
"╠═══╪═══╪═══╬═══╪═══╪═══╬═══╪═══╪═══╣\n",
|
|
"║ 9 │ 3 │ 5 ║ 1 │ 8 │ 4 ║ 7 │ 6 │ 2 ║\n",
|
|
"╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n",
|
|
"║ 8 │ 1 │ 7 ║ 2 │ 3 │ 6 ║ 4 │ 5 │ 9 ║\n",
|
|
"╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n",
|
|
"║ 4 │ 6 │ 2 ║ 5 │ 9 │ 7 ║ 8 │ 3 │ 1 ║\n",
|
|
"╠═══╪═══╪═══╬═══╪═══╪═══╬═══╪═══╪═══╣\n",
|
|
"║ 2 │ 9 │ 8 ║ 6 │ 4 │ 1 ║ 5 │ 7 │ 3 ║\n",
|
|
"╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n",
|
|
"║ 1 │ 7 │ 3 ║ 9 │ 5 │ 8 ║ 2 │ 4 │ 6 ║\n",
|
|
"╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n",
|
|
"║ 5 │ 4 │ 6 ║ 3 │ 7 │ 2 ║ 1 │ 9 │ 8 ║\n",
|
|
"╚═══╧═══╧═══╩═══╧═══╧═══╩═══╧═══╧═══╝\n"
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"source": [
|
|
"Finally, let's modify the last puzzle so it is (non-obviously) impossible to solve. I've just added a 3 to position (3,3) on the grid. It looks innoccuous, but actually makes the puzzle unsolvable."
|
|
],
|
|
"metadata": {
|
|
"id": "opc4hxI2ugU7"
|
|
}
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"source": [
|
|
"puzzle3 = [[0,5,0,0,0,9,0,8,0],\n",
|
|
" [7,0,0,0,0,3,6,0,5],\n",
|
|
" [0,0,3,0,6,0,0,1,0],\n",
|
|
" [0,0,0,0,0,0,0,6,0],\n",
|
|
" [0,1,0,0,3,0,4,0,9],\n",
|
|
" [0,0,2,0,0,7,0,0,0],\n",
|
|
" [0,9,0,0,4,0,5,0,3],\n",
|
|
" [1,0,0,9,0,0,0,0,0],\n",
|
|
" [0,0,0,0,0,0,0,0,8]]\n",
|
|
"drawPuzzle(puzzle3)\n",
|
|
"solve_soduku(puzzle3)"
|
|
],
|
|
"metadata": {
|
|
"colab": {
|
|
"base_uri": "https://localhost:8080/"
|
|
},
|
|
"id": "0lfUKX66ubj0",
|
|
"outputId": "e74941c8-addd-46fd-d908-34b0d975fd71"
|
|
},
|
|
"execution_count": 34,
|
|
"outputs": [
|
|
{
|
|
"output_type": "stream",
|
|
"name": "stdout",
|
|
"text": [
|
|
"╔═══╤═══╤═══╦═══╤═══╤═══╦═══╤═══╤═══╗\n",
|
|
"║ │ 5 │ ║ │ │ 9 ║ │ 8 │ ║\n",
|
|
"╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n",
|
|
"║ 7 │ │ ║ │ │ 3 ║ 6 │ │ 5 ║\n",
|
|
"╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n",
|
|
"║ │ │ 3 ║ │ 6 │ ║ │ 1 │ ║\n",
|
|
"╠═══╪═══╪═══╬═══╪═══╪═══╬═══╪═══╪═══╣\n",
|
|
"║ │ │ ║ │ │ ║ │ 6 │ ║\n",
|
|
"╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n",
|
|
"║ │ 1 │ ║ │ 3 │ ║ 4 │ │ 9 ║\n",
|
|
"╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n",
|
|
"║ │ │ 2 ║ │ │ 7 ║ │ │ ║\n",
|
|
"╠═══╪═══╪═══╬═══╪═══╪═══╬═══╪═══╪═══╣\n",
|
|
"║ │ 9 │ ║ │ 4 │ ║ 5 │ │ 3 ║\n",
|
|
"╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n",
|
|
"║ 1 │ │ ║ 9 │ │ ║ │ │ ║\n",
|
|
"╟───┼───┼───╫───┼───┼───╫───┼───┼───╢\n",
|
|
"║ │ │ ║ │ │ ║ │ │ 8 ║\n",
|
|
"╚═══╧═══╧═══╩═══╧═══╧═══╩═══╧═══╧═══╝\n",
|
|
"unsat\n",
|
|
"No solution\n"
|
|
]
|
|
}
|
|
]
|
|
}
|
|
]
|
|
} |