271 lines
23 KiB
Plaintext
271 lines
23 KiB
Plaintext
{
|
|
"nbformat": 4,
|
|
"nbformat_minor": 0,
|
|
"metadata": {
|
|
"colab": {
|
|
"provenance": [],
|
|
"authorship_tag": "ABX9TyO6l9I4bne2b2Eu/ICYArIt",
|
|
"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_Construction2.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": "jv83sxEU2Ig0"
|
|
}
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"source": [
|
|
"# SAT Constructions 2\n",
|
|
"\n",
|
|
"The purpose of this Python notebook is to investigate the SAT construction that tests if a graph is connected.\n",
|
|
"\n",
|
|
"Work through the cells below, running each cell in turn. In various places you will see the words \"TODO\". Follow the instructions at these places and write code to complete the functions.\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. If you are using CoLab, we recommend that turn off AI autocomplete (under cog icon in top-right corner), which will give you the answers and defeat the purpose of the exercise.\n",
|
|
"\n",
|
|
"A fully working version of this notebook with the complete answers can be found [here](https://github.com/udlbook/udlbook/blob/main/Trees/SAT_Construction2_Answers.ipynb).\n",
|
|
"\n",
|
|
"Contact me at iclimbtreesmail@gmail.com if you find any mistakes or have any suggestions."
|
|
],
|
|
"metadata": {
|
|
"id": "IsBSW40O20Hv"
|
|
}
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"metadata": {
|
|
"id": "WZYb15hc19es"
|
|
},
|
|
"outputs": [],
|
|
"source": [
|
|
"!pip install z3-solver\n",
|
|
"from z3 import *\n",
|
|
"import numpy as np\n",
|
|
"from itertools import combinations"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"source": [
|
|
"# Connected components\n",
|
|
"\n",
|
|
"Finally, let's develop a construction that tells us if the elements of an undirected graph are connected. Consider the two adjacency matrices:\n",
|
|
"\n",
|
|
"\\begin{equation}\n",
|
|
"A_1 = \\begin{bmatrix}1 & 1 & 0 & 0 & 0 & 0 & 0 & 0 \\\\\n",
|
|
" 1 & 1 & 1 & 0 & 0 & 0 & 0 & 0 \\\\\n",
|
|
" 0 & 1 & 1 & 1 & 0 & 0 & 0 & 0 \\\\\n",
|
|
" 0 & 0 & 1 & 1 & 1 & 0 & 0 & 0 \\\\\n",
|
|
" 0 & 0 & 0 & 1 & 1 & 1 & 0 & 0 \\\\\n",
|
|
" 0 & 0 & 0 & 0 & 1 & 1 & 1 & 0 \\\\\n",
|
|
" 0 & 0 & 0 & 0 & 0 & 1 & 1 & 1 \\\\\n",
|
|
" 0 & 0 & 0 & 0 & 0 & 0 & 1 & 1 \\\\\n",
|
|
" \\end{bmatrix} \\quad\\quad\n",
|
|
" A_2 = \\begin{bmatrix}1 & 1 & 0 & 1 & 0 & 0 & 0 & 0 \\\\\n",
|
|
" 1 & 1 & 1 & 0 & 0 & 0 & 0 & 0 \\\\\n",
|
|
" 0 & 1 & 1 & 1 & 0 & 0 & 0 & 0 \\\\\n",
|
|
" 1 & 0 & 1 & 1 & 1 & 0 & 0 & 0 \\\\\n",
|
|
" 0 & 0 & 0 & 1 & 1 & 1 & 0 & 0 \\\\\n",
|
|
" 0 & 0 & 0 & 0 & 1 & 1 & 0 & 0 \\\\\n",
|
|
" 0 & 0 & 0 & 0 & 0 & 0 & 1 & 1 \\\\\n",
|
|
" 0 & 0 & 0 & 0 & 0 & 0 & 1 & 1 \\\\\n",
|
|
" \\end{bmatrix}\n",
|
|
"\\end{equation}\n",
|
|
"\n",
|
|
"Each matrix represents the edges in a graph containing eight nodes. Elements $(i,j)$ and $(j,i)$ will be set to one if there is an edge between nodes $i$ and $j$. The diagonal elements are all set to one.\n",
|
|
"\n",
|
|
"For matrix $A_{1}$ the nodes are all connected; node 1 connects to node 2, which connects to node 3, and so on up to node 8. \n",
|
|
"\n",
|
|
"For matrix $A_{2}$ however, the nodes are not all connected. Nodes 7 and 8 are connected to each other but not connected any of the other nodes.\n"
|
|
],
|
|
"metadata": {
|
|
"id": "CZQygtit0D9Q"
|
|
}
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"source": [
|
|
"# Test for connected components"
|
|
],
|
|
"metadata": {
|
|
"id": "SzoAO6PBnEux"
|
|
}
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"source": [
|
|
"We can test for the connectivity of the graph implied by an $8\\times 8$ matrix $\\mathbf{A}$ by computing new adjacency matrices $\\mathbf{B},\\mathbf{C},\\mathbf{D}$ where:\n",
|
|
"\n",
|
|
"$$\\begin{aligned}\n",
|
|
"B_{ij} &\\Leftrightarrow \\bigvee_k (A_{ik} \\land A_{kj})\\\\\n",
|
|
"C_{ij} &\\Leftrightarrow \\bigvee_k (B_{ik} \\land B_{kj})\\\\\n",
|
|
"D_{ij} &\\Leftrightarrow \\bigvee_k (C_{ik} \\land C_{kj})\n",
|
|
"\\end{aligned}\n",
|
|
"$$\n",
|
|
"\n",
|
|
"and then enforcing the constraint that the first row of $\\mathbf{D}$ contains all true elements:\n",
|
|
"\n",
|
|
"$$ \\bigvee_k D_{0,k}$$\n",
|
|
"\n",
|
|
"In general, if the initial matrix $\\mathbf{A}$ is of size $N\\times N$, we will need to compute $\\log_2[N]$ intermediate matrices $\\mathbf{B},\\mathbf{C},\\mathbf{D}$."
|
|
],
|
|
"metadata": {
|
|
"id": "2brsB9m54aGo"
|
|
}
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"source": [
|
|
"Now let's write a SAT routine to check if an adjacency matrix represents a fully-connected graph"
|
|
],
|
|
"metadata": {
|
|
"id": "TxctcAsX8rh0"
|
|
}
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"source": [
|
|
"def is_fully_connected(s, adjacency):\n",
|
|
" # Size of the adjacency matrix\n",
|
|
" n_components = len(adjacency)\n",
|
|
" # We'll construct a N x N x log[N] array of variables\n",
|
|
" # The NxN variables in the first layer represent A, the variables in the second layer represent B and so on\n",
|
|
" n_layers = math.ceil(math.log(n_components,2))+1\n",
|
|
" connected = [[[ z3.Bool(\"conn_{%d,%d,%d}\"%((i,j,n))) for n in range(0, n_layers)] for j in range(0, n_components) ] for i in range(0, n_components) ]\n",
|
|
"\n",
|
|
" # Constraint 1\n",
|
|
" # The value in the top layer of the connected structure is equal to the adjacency matrix\n",
|
|
" # TODO -- replace this line\n",
|
|
" s.add(connected[0][0][0])\n",
|
|
"\n",
|
|
" # Constraint 2\n",
|
|
" # Value at position [i,j] in layer n is true if there is a k such that position[i,k] and positions [k,j] in layer n-1 are true\n",
|
|
" for n in range(1,n_layers):\n",
|
|
" for i in range(n_components):\n",
|
|
" for j in range(n_components):\n",
|
|
" # TODO -- replace this line\n",
|
|
" s.add(connected[i][j][n])\n",
|
|
"\n",
|
|
" # Constraint 3 -- any row of column of the matrix should be full of ones at the end (everything is connected)\n",
|
|
" # TODO -- replace this line\n",
|
|
" s.add(connected[0][0][n_layers-1])\n",
|
|
"\n",
|
|
" return s"
|
|
],
|
|
"metadata": {
|
|
"id": "JpfVC-Rg0LiC"
|
|
},
|
|
"execution_count": null,
|
|
"outputs": []
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"source": [
|
|
"Finally, let's write a routine that tests the adjacency of the two matrices above using a SAT solver."
|
|
],
|
|
"metadata": {
|
|
"id": "slbVVZH6-_Jl"
|
|
}
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"source": [
|
|
"def test_is_fully_connected(A):\n",
|
|
" # Set up the SAT solver\n",
|
|
" s = Solver()\n",
|
|
"\n",
|
|
" # Convert the input matrix to z3 Boolean values\n",
|
|
" n_components = A.shape[0]\n",
|
|
" adjacency= [[ z3.Bool(\"a_{%d,%d}\"%((i,j))) for j in range(0, n_components) ] for i in range(0, n_components) ]\n",
|
|
" for i in range(n_components):\n",
|
|
" for j in range(n_components):\n",
|
|
" if A[i,j]!=0:\n",
|
|
" s.add(adjacency[i][j])\n",
|
|
" else:\n",
|
|
" s.add(Not(adjacency[i][j]))\n",
|
|
"\n",
|
|
" # Run the routine\n",
|
|
" s = is_fully_connected(s, adjacency)\n",
|
|
"\n",
|
|
" # Check if it's SAT (creates the model)\n",
|
|
" sat_result = s.check()\n",
|
|
" print(sat_result)\n",
|
|
"\n",
|
|
" # If it was SAT then print out the layers of the 3D structure\n",
|
|
" if sat_result == z3.sat:\n",
|
|
" result = s.model()\n",
|
|
" c_vals = np.array([[[int(bool(result[z3.Bool(\"conn_{%d,%d,%d}\" % (i, j,n))])) for n in range(0, n_components-1)] for j in range(0,n_components) ] for i in range(0,n_components) ] )\n",
|
|
" for n in range(math.ceil(math.log(n_components,2))+1):\n",
|
|
" print(\"Layer:\",n)\n",
|
|
" print(c_vals[:,:,n])"
|
|
],
|
|
"metadata": {
|
|
"id": "0veuGhg_--EJ"
|
|
},
|
|
"execution_count": null,
|
|
"outputs": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"source": [
|
|
"A1 = np.array([[1, 1, 0, 0, 0, 0, 0, 0],\n",
|
|
" [1, 1, 1, 0, 0, 0, 0, 0],\n",
|
|
" [0, 1, 1, 1, 0, 0, 0, 0],\n",
|
|
" [0, 0, 1, 1, 1, 0, 0, 0],\n",
|
|
" [0, 0, 0, 1, 1, 1, 0, 0],\n",
|
|
" [0, 0, 0, 0, 1, 1, 1, 0],\n",
|
|
" [0, 0, 0, 0, 0, 1, 1, 1],\n",
|
|
" [0, 0, 0, 0, 0, 0, 1, 1]])\n",
|
|
"test_is_fully_connected(A1)"
|
|
],
|
|
"metadata": {
|
|
"id": "rk83toMaAkQX"
|
|
},
|
|
"execution_count": null,
|
|
"outputs": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"source": [
|
|
"A2 = np.array([[1, 1, 0, 1, 0, 0, 0, 0],\n",
|
|
" [1, 1, 1, 0, 0, 0, 0, 0],\n",
|
|
" [0, 1, 1, 1, 0, 0, 0, 0],\n",
|
|
" [1, 0, 1, 1, 1, 0, 0, 0],\n",
|
|
" [0, 0, 0, 1, 1, 1, 0, 0],\n",
|
|
" [0, 0, 0, 0, 1, 1, 0, 0],\n",
|
|
" [0, 0, 0, 0, 0, 0, 1, 1],\n",
|
|
" [0, 0, 0, 0, 0, 0, 1, 1]])\n",
|
|
"test_is_fully_connected(A2)"
|
|
],
|
|
"metadata": {
|
|
"id": "DRzo_XrCAlrz"
|
|
},
|
|
"execution_count": null,
|
|
"outputs": []
|
|
}
|
|
]
|
|
} |