989 lines
51 KiB
Plaintext
989 lines
51 KiB
Plaintext
{
|
|
"nbformat": 4,
|
|
"nbformat_minor": 0,
|
|
"metadata": {
|
|
"colab": {
|
|
"provenance": [],
|
|
"authorship_tag": "ABX9TyMjeWJ3+JkP3KO4xuarMyeL",
|
|
"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_Construction_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": "jv83sxEU2Ig0"
|
|
}
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"source": [
|
|
"# SAT Constructions\n",
|
|
"\n",
|
|
"The purpose of this Python notebook is to use investigate SAT constructions that impose constraints on sets of variables. We'll build constructions for ensuring all of the variables are the same, that only one of the variables is true, that at leats $K$ of the variables are true, that fewer than $K$ of the variables are true and that exactly $K$ of the variables are true.\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": "IsBSW40O20Hv"
|
|
}
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"metadata": {
|
|
"id": "WZYb15hc19es",
|
|
"colab": {
|
|
"base_uri": "https://localhost:8080/"
|
|
},
|
|
"outputId": "d95ed66f-a8f7-422a-c6f4-1401d6bd06a5"
|
|
},
|
|
"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[31m20.4 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"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"!pip install z3-solver\n",
|
|
"from z3 import *\n",
|
|
"import numpy as np\n",
|
|
"from itertools import combinations"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"source": [
|
|
"# Same\n",
|
|
"\n",
|
|
"Let's write a subroutine that returns a Boolean logic formula that constrains $N$ variables to be the same.\n",
|
|
"\n",
|
|
"$$ \\textrm{Same}[x_{1},x_{2},x_{3},\n",
|
|
"\\ldots x_{N}]:= (x_{1}\\land x_{2}\\land x_{3},\\ldots,x_N)\\lor(\\overline{x}_{1}\\land \\overline{x}_{2}\\land \\overline{x}_{3},\\ldots,\\overline{x}_N).$$"
|
|
],
|
|
"metadata": {
|
|
"id": "aVj9RmuB3ZWJ"
|
|
}
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"source": [
|
|
"First let's define the variables. We'll choose $N=10$"
|
|
],
|
|
"metadata": {
|
|
"id": "Amv5G3VR3zIJ"
|
|
}
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"source": [
|
|
"N=10\n",
|
|
"x = [ z3.Bool(\"x_{i}\".format(i=i)) for i in range(0,N) ]\n",
|
|
"print(x)"
|
|
],
|
|
"metadata": {
|
|
"id": "J-y3uhTs-LU7"
|
|
},
|
|
"execution_count": null,
|
|
"outputs": []
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"source": [
|
|
"Now let's write the main routine. We can make use of the fact that the Z3 command 'Or' which combines together a list of literals with Or operations."
|
|
],
|
|
"metadata": {
|
|
"id": "4pY5yiDo-esv"
|
|
}
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"source": [
|
|
"# Routine that returns the SAT construction (a Boolean logic formula) for all literals in x being the same.\n",
|
|
"def same(x):\n",
|
|
" return Or(And(x), And([Not(xi) for xi in x]))"
|
|
],
|
|
"metadata": {
|
|
"id": "f0esE71E94fm"
|
|
},
|
|
"execution_count": null,
|
|
"outputs": []
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"source": [
|
|
"Finally, let's test that our routine works. Here's generic routine that evaluates a vector of concrete values against a provided Boolean logic formula\n"
|
|
],
|
|
"metadata": {
|
|
"id": "EWTuxEvrAfnK"
|
|
}
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"source": [
|
|
"def check_expression(x, formula, literals):\n",
|
|
" # Create the solver\n",
|
|
" s = Solver()\n",
|
|
" # Add the constraint\n",
|
|
" s.add(formula(x))\n",
|
|
" # Add the literals\n",
|
|
" s.add(And([x[i] if literal else Not(x[i]) for i, literal in enumerate(literals)]))\n",
|
|
" # Check if it's SAT (creates the model)\n",
|
|
" sat_result = s.check()\n",
|
|
" if(sat_result==sat):\n",
|
|
" print(\"True\")\n",
|
|
" else:\n",
|
|
" print(\"False\")"
|
|
],
|
|
"metadata": {
|
|
"id": "vY5CD6lRArNP"
|
|
},
|
|
"execution_count": null,
|
|
"outputs": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"source": [
|
|
"check_expression(x, same, [False,False,False,False,False,False,False,False,False,False])\n",
|
|
"check_expression(x, same, [True,False,False,False,False,False,False,False,False,False])\n",
|
|
"check_expression(x, same, [False,False,False,True,False,False,True,False,True,False])\n",
|
|
"check_expression(x, same, [True,True,True,True,True,True,True,True,True,True])"
|
|
],
|
|
"metadata": {
|
|
"id": "Q3VMIDqfHEei"
|
|
},
|
|
"execution_count": null,
|
|
"outputs": []
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"source": [
|
|
"# Exactly One\n",
|
|
"\n",
|
|
"Now let's write a subroutine that returns a Boolean logic formula that is true when only one of the provided variables are the same.\n",
|
|
"\n",
|
|
"First, we write a formula that ensures at least one of the variables is true:\n",
|
|
"\n",
|
|
"$$\\textrm{AtLeastOne}[x_1,x_2,x_3]:= x_{1}\\lor x_{2} \\lor x_{3}, \\ldots, x_{N}.$$\n",
|
|
"\n",
|
|
"Then, we write a formula that ensures that no more than one is true. For each possible pair of literals, we ensure that they are not both true:\n",
|
|
"\n",
|
|
"$$\\textrm{NoMoreThanOne}[x_{1},x_{2},x_{3}]:= \\lnot (x_{1}\\land x_{2}) \\land \\lnot (x_{1}\\land x_{3}),\\ldots, \\land \\lnot (x_{n-1}\\land x_{N}) $$\n",
|
|
"\n",
|
|
"Finally, we **AND** together these two formulae:\n",
|
|
"\n",
|
|
"$$\\textrm{ExactlyOne}[x_1,x_2,x_3,\\ldots, x_N] = \\textrm{AtLeastOne}[x_1,x_2,x_3, \\ldots, x_N]\\land\\textrm{NoMoreThanOne}[x_1,x_2,x_3, \\ldots x_N]$$\n",
|
|
"\n",
|
|
"You might want to use the function \"combinations\" from itertools (imported above). Example usage:"
|
|
],
|
|
"metadata": {
|
|
"id": "0IIRG5ZWIZV6"
|
|
}
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"source": [
|
|
"test = [ z3.Bool(\"x_{i}\".format(i=i)) for i in range(0,4) ]\n",
|
|
"for comb in combinations(test, 2):\n",
|
|
" print(comb[0], comb[1])"
|
|
],
|
|
"metadata": {
|
|
"id": "joeZiDT3LV-r"
|
|
},
|
|
"execution_count": null,
|
|
"outputs": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"source": [
|
|
"def at_least_one(x):\n",
|
|
" return Or(x)\n",
|
|
"\n",
|
|
"def no_more_than_one(x):\n",
|
|
" clauses = True ;\n",
|
|
" for comb in combinations(x, 2):\n",
|
|
" clauses = And([clauses, Or([Not(comb[0]), Not(comb[1])]) ])\n",
|
|
" return clauses\n",
|
|
"\n",
|
|
"def exactly_one(x):\n",
|
|
" return And(at_least_one(x), no_more_than_one(x))"
|
|
],
|
|
"metadata": {
|
|
"id": "C0HGBOjI99Ex"
|
|
},
|
|
"execution_count": null,
|
|
"outputs": []
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"source": [
|
|
"Let's test if this works:"
|
|
],
|
|
"metadata": {
|
|
"id": "2Y_1zYOZIoZI"
|
|
}
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"source": [
|
|
"check_expression(x, exactly_one, [False,False,False,False,False,False,False,False,False,False])\n",
|
|
"check_expression(x, exactly_one, [True,False,False,False,False,False,False,False,False,False])\n",
|
|
"check_expression(x, exactly_one, [False,False,False,True,False,False,True,False,True,False])\n",
|
|
"check_expression(x, exactly_one, [True,True,True,True,True,True,True,True,True,True])"
|
|
],
|
|
"metadata": {
|
|
"id": "31gqasHnM3c3"
|
|
},
|
|
"execution_count": null,
|
|
"outputs": []
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"source": [
|
|
"# At least K\n",
|
|
"\n",
|
|
"Finally, we'll build the construction that ensures that there at at least K elements that are true in a vector of length N.\n",
|
|
"\n",
|
|
"This one is a bit more complicated. We construct an NxK matrix of new literals $r_{i,j}$ Then we add the following constraints.\n",
|
|
"\n",
|
|
"1. Top left element $r_{0,0}$ is the first data element\n",
|
|
"\n",
|
|
"$$ r_{00} \\Leftrightarrow x_{1}$$\n",
|
|
"\n",
|
|
"2. Remaining elements $r_{0,1:}$ must be false\n",
|
|
"\n",
|
|
"$$ \\overline{r}_{0,j} \\quad\\quad \\forall j\\in\\{1,2,\\ldots K-1\\}$$\n",
|
|
"\n",
|
|
"3. Remaining elements $r_{i,0}$ in first column are true where x_i is true\n",
|
|
"\n",
|
|
"$$x_i \\Rightarrow r_{i,0} \\quad\\quad \\forall i\\in\\{1,2,\\ldots N-1\\}$$\n",
|
|
"\n",
|
|
"4. For rows 1:N-1, if the element above is true, this must be true\n",
|
|
"\n",
|
|
"$$ r_{i-1,j} \\Rightarrow r_{i,j}\\quad\\quad \\quad\\quad \\forall i\\in\\{1,2,\\ldots N-1\\}, j\\in\\{0,1,\\ldots,K-1\\}$$\n",
|
|
"\n",
|
|
"5. If x is true for this row and the element above and to the left is true then set this element to true.\n",
|
|
"\n",
|
|
"$$ (x_i \\land r_{i-1,j-1})\\Rightarrow r_{i,j} \\quad\\quad \\forall i\\in\\{1,2,\\ldots N-1\\}, j\\in\\{1,2,\\ldots,K-1\\} $$\n",
|
|
"\n",
|
|
"6. If x is false for this row and the element above is false then set to false\n",
|
|
"\n",
|
|
"$$ (\\overline{x}_{i} \\land \\overline{r}_{i-1,j}) \\Rightarrow \\overline{r}_{i,j} \\quad\\quad \\forall i\\in\\{1,2,\\ldots N-1\\}, j\\in\\{1,2,\\ldots,K-1\\} $$\n",
|
|
"\n",
|
|
"7. if x is false for this row and the element above and to the left is false then set to false:\n",
|
|
"\n",
|
|
"$$ (\\overline{x}_i \\land \\overline{r}_{i-1,j-1})\\Rightarrow \\overline{r}_{i,j} \\quad\\quad \\forall i\\in\\{1,2,\\ldots N-1\\}, j\\in\\{1,2,\\ldots,K-1\\} $$\n",
|
|
"\n",
|
|
"8. The bottom-right element of r must be true\n",
|
|
"\n",
|
|
"$$ r_{N-1,K-1}$$"
|
|
],
|
|
"metadata": {
|
|
"id": "MJqWOMBsQrCI"
|
|
}
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"source": [
|
|
"def at_least_k(x, K):\n",
|
|
" # Create nxk table of literals r_{i,j}\n",
|
|
" N = len(x) ;\n",
|
|
" r = [[ z3.Bool(\"r_{%d,%d}\"%((i,j))) for j in range(0,K) ] for i in range(0,N) ]\n",
|
|
"\n",
|
|
" #1. Top left element $r_{0,0}$ is the first data element\n",
|
|
"\n",
|
|
" clauses = (r[0][0] == x[0])\n",
|
|
"\n",
|
|
" #2. Remaining elements $r_{0,1:}$ must be false\n",
|
|
"\n",
|
|
" clauses = And(clauses, And([ Not(r[0][j]) for j in range(1,K) ]))\n",
|
|
"\n",
|
|
" #3. Remaining elements $r_{i,0}$ in first column are true where x_i is true\n",
|
|
" clauses = And(clauses, And([Implies(x[i],r[i][0]) for i in range(1,N)]))\n",
|
|
"\n",
|
|
" #4. For rows 1:n-1, if the element above is true, this must be true\n",
|
|
"\n",
|
|
" for i in range(1,N):\n",
|
|
" for j in range(0,K):\n",
|
|
" clauses = And(clauses, Implies(r[i-1][j], r[i][j]))\n",
|
|
"\n",
|
|
" #5. If x is true for this row and the element above and to the left is true then set this element to true.\n",
|
|
" #6. If x is false for this row and the element above is false then set to false\n",
|
|
" #7. if x is false for this row and the element above and to the left is false then set to false:\n",
|
|
" for i in range(1,N):\n",
|
|
" for j in range(1,K):\n",
|
|
" clauses = And(clauses, Implies(And(x[i], r[i-1][j-1]), r[i][j]))\n",
|
|
" clauses = And(clauses, Implies(And(Not(x[i]), Not(r[i-1][j])), Not(r[i][j])))\n",
|
|
" clauses = And(clauses, Implies(And(Not(x[i]), Not(r[i-1][j-1])), Not(r[i][j])))\n",
|
|
"\n",
|
|
" #8. The bottom-right element of r must be true\n",
|
|
" clauses = And(clauses, r[N-1][K-1])\n",
|
|
"\n",
|
|
" return clauses"
|
|
],
|
|
"metadata": {
|
|
"id": "aTcc1Ad0M9NX"
|
|
},
|
|
"execution_count": null,
|
|
"outputs": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"source": [
|
|
"#This function defined for convenience so that check_expression works\n",
|
|
"def at_least_three(x):\n",
|
|
" return at_least_k(x,3)\n",
|
|
"\n",
|
|
"check_expression(x, at_least_three, [False,False,False,False,False,False,False,False,False,False])\n",
|
|
"check_expression(x, at_least_three, [True,False,False,False,False,False,False,False,False,False])\n",
|
|
"check_expression(x, at_least_three, [False,False,False,True,False,False,True,False,True,False])\n",
|
|
"check_expression(x, at_least_three, [True,True,True,True,True,True,True,True,True,True])"
|
|
],
|
|
"metadata": {
|
|
"id": "ESnui2V7YBQC"
|
|
},
|
|
"execution_count": null,
|
|
"outputs": []
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"source": [
|
|
"Optional: write functions to test if there are:\n",
|
|
"\n",
|
|
"* Fewer than $K$ elements\n",
|
|
"* Exactly $N$ elements\n",
|
|
"\n"
|
|
],
|
|
"metadata": {
|
|
"id": "PwgpncA5g0-C"
|
|
}
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"source": [
|
|
"def fewer_than_k(x, K):\n",
|
|
" # Create nxk table of literals r_{i,j}\n",
|
|
" N = len(x) ;\n",
|
|
" r = [[ z3.Bool(\"r_{%d,%d}\"%((i,j))) for j in range(0,K) ] for i in range(0,N) ]\n",
|
|
"\n",
|
|
" #1. Top left element $r_{0,0}$ is the first data element\n",
|
|
"\n",
|
|
" clauses = (r[0][0] == x[0])\n",
|
|
"\n",
|
|
" #2. Remaining elements $r_{0,1:}$ must be false\n",
|
|
"\n",
|
|
" clauses = And(clauses, And([ Not(r[0][j]) for j in range(1,K) ]))\n",
|
|
"\n",
|
|
" #3. Remaining elements $r_{i,0}$ in first column are true where x_i is true\n",
|
|
" clauses = And(clauses, And([Implies(x[i],r[i][0]) for i in range(1,N)]))\n",
|
|
"\n",
|
|
" #4. For rows 1:n-1, if the element above is true, this must be true\n",
|
|
" for i in range(1,N):\n",
|
|
" for j in range(0,K):\n",
|
|
" clauses = And(clauses, Implies(r[i-1][j], r[i][j]))\n",
|
|
"\n",
|
|
" #5. If x is true for this row and the element above and to the left is true then set this element to true.\n",
|
|
" #6. If x is false for this row and the element above is false then set to false\n",
|
|
" #7. if x is false for this row and the element above and to the left is false then set to false:\n",
|
|
" for i in range(1,N):\n",
|
|
" for j in range(1,K):\n",
|
|
" clauses = And(clauses, Implies(And(x[i], r[i-1][j-1]), r[i][j]))\n",
|
|
" clauses = And(clauses, Implies(And(Not(x[i]), Not(r[i-1][j])), Not(r[i][j])))\n",
|
|
" clauses = And(clauses, Implies(And(Not(x[i]), Not(r[i-1][j-1])), Not(r[i][j])))\n",
|
|
"\n",
|
|
" #8. The bottom-right element of r must be false\n",
|
|
" clauses = And(clauses, Not(r[N-1][K-1]))\n",
|
|
"\n",
|
|
" return clauses"
|
|
],
|
|
"metadata": {
|
|
"id": "RS31wg5Ig0f-"
|
|
},
|
|
"execution_count": null,
|
|
"outputs": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"source": [
|
|
"#This function defined for convenience so that check_expression works\n",
|
|
"def fewer_than_three(x):\n",
|
|
" return fewer_than_k(x,3)\n",
|
|
"\n",
|
|
"check_expression(x, fewer_than_three, [False,False,False,False,False,False,False,False,False,False])\n",
|
|
"check_expression(x, fewer_than_three, [True,False,False,False,False,False,False,False,False,False])\n",
|
|
"check_expression(x, fewer_than_three, [False,False,False,True,False,False,True,False,True,False])\n",
|
|
"check_expression(x, fewer_than_three, [True,True,True,True,True,True,True,True,True,True])"
|
|
],
|
|
"metadata": {
|
|
"id": "Sy67NXs7hqDS"
|
|
},
|
|
"execution_count": null,
|
|
"outputs": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"source": [
|
|
"def exactly_k(x, K):\n",
|
|
" # Create n x (k+1) table of literals r_{i,j}\n",
|
|
" N = len(x) ;\n",
|
|
" r = [[ z3.Bool(\"r_{%d,%d}\"%((i,j))) for j in range(0,K+1) ] for i in range(0,N) ]\n",
|
|
"\n",
|
|
" #1. Top left element $r_{0,0}$ is the first data element\n",
|
|
"\n",
|
|
" clauses = (r[0][0] == x[0])\n",
|
|
"\n",
|
|
" #2. Remaining elements $r_{0,1:}$ must be false\n",
|
|
"\n",
|
|
" clauses = And(clauses, And([ Not(r[0][j]) for j in range(1,K+1) ]))\n",
|
|
"\n",
|
|
" #3. Remaining elements $r_{i,0}$ in first column are true where x_i is true\n",
|
|
" clauses = And(clauses, And([Implies(x[i],r[i][0]) for i in range(1,N)]))\n",
|
|
"\n",
|
|
" #4. For rows 1:n-1, if the element above is true, this must be true\n",
|
|
" for i in range(1,N):\n",
|
|
" for j in range(0,K+1):\n",
|
|
" clauses = And(clauses, Implies(r[i-1][j], r[i][j]))\n",
|
|
"\n",
|
|
" #5. If x is true for this row and the element above and to the left is true then set this element to true.\n",
|
|
" #6. If x is false for this row and the element above is false then set to false\n",
|
|
" #7. if x is false for this row and the element above and to the left is false then set to false:\n",
|
|
" for i in range(1,N):\n",
|
|
" for j in range(1,K+1):\n",
|
|
" clauses = And(clauses, Implies(And(x[i], r[i-1][j-1]), r[i][j]))\n",
|
|
" clauses = And(clauses, Implies(And(Not(x[i]), Not(r[i-1][j])), Not(r[i][j])))\n",
|
|
" clauses = And(clauses, Implies(And(Not(x[i]), Not(r[i-1][j-1])), Not(r[i][j])))\n",
|
|
"\n",
|
|
" #8. The bottom-right element of r must be\n",
|
|
" clauses = And(clauses, r[N-1][K-1])\n",
|
|
" clauses = And(clauses, Not(r[N-1][K]))\n",
|
|
"\n",
|
|
" return clauses"
|
|
],
|
|
"metadata": {
|
|
"id": "Fzaa1NoaicKT"
|
|
},
|
|
"execution_count": null,
|
|
"outputs": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"source": [
|
|
"#This function defined for convenience so that check_expression works\n",
|
|
"def exactly_three(x):\n",
|
|
" return exactly_k(x,3)\n",
|
|
"\n",
|
|
"check_expression(x, exactly_three, [False,False,False,False,False,False,False,False,False,False])\n",
|
|
"check_expression(x, exactly_three, [True,False,False,False,False,False,False,False,False,False])\n",
|
|
"check_expression(x, exactly_three, [False,False,False,True,False,False,True,False,True,False])\n",
|
|
"check_expression(x, exactly_three, [True,True,True,True,True,True,True,True,True,True])"
|
|
],
|
|
"metadata": {
|
|
"id": "L_xwfybUkKhw"
|
|
},
|
|
"execution_count": null,
|
|
"outputs": []
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"source": [
|
|
"Now that we've finished, I'll let you into a secret. Z3 actually contains routines for (AtLeast, FewerThanOrEqualToo, and Exactly)"
|
|
],
|
|
"metadata": {
|
|
"id": "H3lipx8akmHp"
|
|
}
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"source": [
|
|
"def at_least_k_z3(x,K):\n",
|
|
" return PbGe([(i,1) for i in x],K)\n",
|
|
"\n",
|
|
"def at_least_three_z3(x):\n",
|
|
" return at_least_k_z3(x,3)\n",
|
|
"\n",
|
|
"check_expression(x, at_least_three_z3, [False,False,False,False,False,False,False,False,False,False])\n",
|
|
"check_expression(x, at_least_three_z3, [True,False,False,False,False,False,False,False,False,False])\n",
|
|
"check_expression(x, at_least_three_z3, [False,False,False,True,False,False,True,False,True,False])\n",
|
|
"check_expression(x, at_least_three_z3, [True,True,True,True,True,True,True,True,True,True])"
|
|
],
|
|
"metadata": {
|
|
"id": "Yho3WtG0luM6"
|
|
},
|
|
"execution_count": null,
|
|
"outputs": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"source": [
|
|
"def fewer_than_k_z3(x,K):\n",
|
|
" return PbLe([(i,1) for i in x],K-1)\n",
|
|
"\n",
|
|
"def fewer_than_three_z3(x):\n",
|
|
" return fewer_than_k_z3(x,3)\n",
|
|
"\n",
|
|
"check_expression(x, fewer_than_three_z3, [False,False,False,False,False,False,False,False,False,False])\n",
|
|
"check_expression(x, fewer_than_three_z3, [True,False,False,False,False,False,False,False,False,False])\n",
|
|
"check_expression(x, fewer_than_three_z3, [False,False,False,True,False,False,True,False,True,False])\n",
|
|
"check_expression(x, fewer_than_three_z3, [True,True,True,True,True,True,True,True,True,True])"
|
|
],
|
|
"metadata": {
|
|
"id": "ZjAMpiNFmJPc"
|
|
},
|
|
"execution_count": null,
|
|
"outputs": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"source": [
|
|
"def exactly_k_z3(x,K):\n",
|
|
" return PbEq([(i,1) for i in x],K)\n",
|
|
"\n",
|
|
"def exactly_three_z3(x):\n",
|
|
" return exactly_k_z3(x,3)\n",
|
|
"\n",
|
|
"check_expression(x, exactly_three_z3, [False,False,False,False,False,False,False,False,False,False])\n",
|
|
"check_expression(x, exactly_three_z3, [True,False,False,False,False,False,False,False,False,False])\n",
|
|
"check_expression(x, exactly_three_z3, [False,False,False,True,False,False,True,False,True,False])\n",
|
|
"check_expression(x, exactly_three_z3, [True,True,True,True,True,True,True,True,True,True])"
|
|
],
|
|
"metadata": {
|
|
"id": "EgG6jGAskUze"
|
|
},
|
|
"execution_count": null,
|
|
"outputs": []
|
|
},
|
|
{
|
|
"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",
|
|
"\n",
|
|
"We can test this by multiplying any adjacency matrix of size $N\\times N$ by itself $N-1$ times (or more). If the resulting matrix contains all non-zero elements then the graph was fully connected. If there are any zeros, then the graph is not fully connected. Let's try that for these two matrices.\n"
|
|
],
|
|
"metadata": {
|
|
"id": "CZQygtit0D9Q"
|
|
}
|
|
},
|
|
{
|
|
"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",
|
|
"\n",
|
|
"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",
|
|
"\n",
|
|
"\n",
|
|
"print(\"Matrix A1 is fully connected. Product does not contain any zeros :\\n\\n\",A1@A1@A1@A1@A1@A1@A1)\n",
|
|
"print(\"\\nMatrix A2 is not fully connected. Product contains zeros :\\n\\n\",A2@A2@A2@A2@A2@A2@A2)"
|
|
],
|
|
"metadata": {
|
|
"colab": {
|
|
"base_uri": "https://localhost:8080/"
|
|
},
|
|
"id": "ywLO1nan2_6K",
|
|
"outputId": "4704aab6-a155-4bd3-857d-d4a6c3b38947"
|
|
},
|
|
"execution_count": null,
|
|
"outputs": [
|
|
{
|
|
"output_type": "stream",
|
|
"name": "stdout",
|
|
"text": [
|
|
"Matrix A1 is fully connected. Product does not contain any zeros :\n",
|
|
"\n",
|
|
" [[127 196 189 133 70 27 7 1]\n",
|
|
" [196 316 329 259 160 77 28 7]\n",
|
|
" [189 329 386 356 266 161 77 27]\n",
|
|
" [133 259 356 393 357 266 160 70]\n",
|
|
" [ 70 160 266 357 393 356 259 133]\n",
|
|
" [ 27 77 161 266 356 386 329 189]\n",
|
|
" [ 7 28 77 160 259 329 316 196]\n",
|
|
" [ 1 7 27 70 133 189 196 127]]\n",
|
|
"\n",
|
|
"Matrix A2 is not fully connected. Product contains zeros :\n",
|
|
"\n",
|
|
" [[ 652 609 651 800 441 191 0 0]\n",
|
|
" [ 609 575 609 728 382 154 0 0]\n",
|
|
" [ 651 609 652 800 441 191 0 0]\n",
|
|
" [ 800 728 800 1016 609 287 0 0]\n",
|
|
" [ 441 382 441 609 421 227 0 0]\n",
|
|
" [ 191 154 191 287 227 134 0 0]\n",
|
|
" [ 0 0 0 0 0 0 64 64]\n",
|
|
" [ 0 0 0 0 0 0 64 64]]\n"
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"source": [
|
|
"In fact we could do this a bit more efficiently, by first calculating $B = A^2$ and then computing $C = B^2 = A^4$ and finally $D=C^2 = A^8$. In this way, we only need $\\log[N]$ multiplications to check the graph is connected."
|
|
],
|
|
"metadata": {
|
|
"id": "SRQTzwSn4zFD"
|
|
}
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"source": [
|
|
"B1 = A1@A1\n",
|
|
"C1 = B1@B1\n",
|
|
"D1 = C1@C1\n",
|
|
"print(\"Matrix A1 is fully connected. Product does not contain any zeros :\\n\\n\",D1)\n",
|
|
"\n",
|
|
"B2 = A2@A2\n",
|
|
"C2 = B2@B2\n",
|
|
"D2 = C2@C2\n",
|
|
"print(\"\\nMatrix A2 is not fully connected. Product contains zeros :\\n\\n\",D2)"
|
|
],
|
|
"metadata": {
|
|
"colab": {
|
|
"base_uri": "https://localhost:8080/"
|
|
},
|
|
"id": "xVbt1Fud61tG",
|
|
"outputId": "15b4e5ce-47ef-474c-9abc-455388616a75"
|
|
},
|
|
"execution_count": null,
|
|
"outputs": [
|
|
{
|
|
"output_type": "stream",
|
|
"name": "stdout",
|
|
"text": [
|
|
"Matrix A1 is fully connected. Product does not contain any zeros :\n",
|
|
"\n",
|
|
" [[ 323 512 518 392 230 104 35 8]\n",
|
|
" [ 512 841 904 748 496 265 112 35]\n",
|
|
" [ 518 904 1071 1008 783 504 265 104]\n",
|
|
" [ 392 748 1008 1106 1016 783 496 230]\n",
|
|
" [ 230 496 783 1016 1106 1008 748 392]\n",
|
|
" [ 104 265 504 783 1008 1071 904 518]\n",
|
|
" [ 35 112 265 496 748 904 841 512]\n",
|
|
" [ 8 35 104 230 392 518 512 323]]\n",
|
|
"\n",
|
|
"Matrix A2 is not fully connected. Product contains zeros :\n",
|
|
"\n",
|
|
" [[2061 1912 2060 2544 1432 632 0 0]\n",
|
|
" [1912 1793 1912 2328 1264 536 0 0]\n",
|
|
" [2060 1912 2061 2544 1432 632 0 0]\n",
|
|
" [2544 2328 2544 3225 1912 896 0 0]\n",
|
|
" [1432 1264 1432 1912 1257 648 0 0]\n",
|
|
" [ 632 536 632 896 648 361 0 0]\n",
|
|
" [ 0 0 0 0 0 0 128 128]\n",
|
|
" [ 0 0 0 0 0 0 128 128]]\n"
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"source": [
|
|
"Obviously, we are working in the world of Boolean variables, so we cannot do full matrix multiplication, but we there is a binary equivalent of matrix multiplication which use AND and OR operations instead of multiplications and additions, respectively. To make this happen, we just define the matrices as boolean and multiply matrices together using the dot product operator between the matrix transpose and itself $\\textrm{dot}[A^T, A]$"
|
|
],
|
|
"metadata": {
|
|
"id": "2brsB9m54aGo"
|
|
}
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"source": [
|
|
"A1Bool = A1.astype(bool)\n",
|
|
"B1 = np.dot(A1Bool.T, A1Bool)\n",
|
|
"C1 = np.dot(B1.T, B1)\n",
|
|
"D1 = np.dot(C1.T, C1)\n",
|
|
"\n",
|
|
"print(\"Matrix A1 is fully connected. Product does not contain any zeros :\\n\\n\",D1)\n",
|
|
"\n",
|
|
"A2Bool = A2.astype(bool)\n",
|
|
"B2 = np.dot(A2Bool.T, A2Bool)\n",
|
|
"C2 = np.dot(B2.T, B2)\n",
|
|
"D2 = np.dot(C2.T, C2)\n",
|
|
"print(\"\\nMatrix A2 is not fully connected. Product contains false values :\\n\\n\",D2)"
|
|
],
|
|
"metadata": {
|
|
"colab": {
|
|
"base_uri": "https://localhost:8080/"
|
|
},
|
|
"id": "o_jvXGDV4Wer",
|
|
"outputId": "da2b933d-27df-40d9-88cb-de2a4a28b032"
|
|
},
|
|
"execution_count": null,
|
|
"outputs": [
|
|
{
|
|
"output_type": "stream",
|
|
"name": "stdout",
|
|
"text": [
|
|
"\n",
|
|
"Matrix A1 is fully connected. Product does not contain any zeros :\n",
|
|
"\n",
|
|
" [[ True True True True True True True True]\n",
|
|
" [ True True True True True True True True]\n",
|
|
" [ True True True True True True True True]\n",
|
|
" [ True True True True True True True True]\n",
|
|
" [ True True True True True True True True]\n",
|
|
" [ True True True True True True True True]\n",
|
|
" [ True True True True True True True True]\n",
|
|
" [ True True True True True True True True]]\n",
|
|
"Matrix A2 is not fully connected. Product contains false values :\n",
|
|
"\n",
|
|
" [[ True True True True True True False False]\n",
|
|
" [ True True True True True True False False]\n",
|
|
" [ True True True True True True False False]\n",
|
|
" [ True True True True True True False False]\n",
|
|
" [ True True True True True True False False]\n",
|
|
" [ True True True True True True False False]\n",
|
|
" [False False False False False False True True]\n",
|
|
" [False False False False False False True True]]\n"
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"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",
|
|
" for i in range(n_components):\n",
|
|
" for j in range(n_components):\n",
|
|
" s.add(connected[i][j][0]==adjacency[i][j])\n",
|
|
"\n",
|
|
" # Constraint 2\n",
|
|
" # Value at position [i,j] in layer n is value at position [i,j] of the binary matrix product of layer n-1 with itself\n",
|
|
" for n in range(1,n_layers):\n",
|
|
" for i in range(n_components):\n",
|
|
" for j in range(n_components):\n",
|
|
" matrix_entry_ij = False\n",
|
|
" for k in range(n_components):\n",
|
|
" matrix_entry_ij = Or(matrix_entry_ij, And(connected[i][k][n-1],connected[k][j][n-1]))\n",
|
|
" s.add(connected[i][j][n]==matrix_entry_ij)\n",
|
|
"\n",
|
|
" # Constraint 3 -- any row of column of the matrix should be full of ones at the end (everything is connected)\n",
|
|
" for i in range(n_components):\n",
|
|
" s.add(connected[i][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": [
|
|
"test_is_fully_connected(A1)"
|
|
],
|
|
"metadata": {
|
|
"colab": {
|
|
"base_uri": "https://localhost:8080/"
|
|
},
|
|
"id": "rk83toMaAkQX",
|
|
"outputId": "75fe712d-1565-4509-9a2e-06e2bea19971"
|
|
},
|
|
"execution_count": null,
|
|
"outputs": [
|
|
{
|
|
"output_type": "stream",
|
|
"name": "stdout",
|
|
"text": [
|
|
"sat\n",
|
|
"Layer: 0\n",
|
|
"[[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",
|
|
"Layer: 1\n",
|
|
"[[1 1 1 0 0 0 0 0]\n",
|
|
" [1 1 1 1 0 0 0 0]\n",
|
|
" [1 1 1 1 1 0 0 0]\n",
|
|
" [0 1 1 1 1 1 0 0]\n",
|
|
" [0 0 1 1 1 1 1 0]\n",
|
|
" [0 0 0 1 1 1 1 1]\n",
|
|
" [0 0 0 0 1 1 1 1]\n",
|
|
" [0 0 0 0 0 1 1 1]]\n",
|
|
"Layer: 2\n",
|
|
"[[1 1 1 1 1 0 0 0]\n",
|
|
" [1 1 1 1 1 1 0 0]\n",
|
|
" [1 1 1 1 1 1 1 0]\n",
|
|
" [1 1 1 1 1 1 1 1]\n",
|
|
" [1 1 1 1 1 1 1 1]\n",
|
|
" [0 1 1 1 1 1 1 1]\n",
|
|
" [0 0 1 1 1 1 1 1]\n",
|
|
" [0 0 0 1 1 1 1 1]]\n",
|
|
"Layer: 3\n",
|
|
"[[1 1 1 1 1 1 1 1]\n",
|
|
" [1 1 1 1 1 1 1 1]\n",
|
|
" [1 1 1 1 1 1 1 1]\n",
|
|
" [1 1 1 1 1 1 1 1]\n",
|
|
" [1 1 1 1 1 1 1 1]\n",
|
|
" [1 1 1 1 1 1 1 1]\n",
|
|
" [1 1 1 1 1 1 1 1]\n",
|
|
" [1 1 1 1 1 1 1 1]]\n"
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"source": [
|
|
"test_is_fully_connected(A2)"
|
|
],
|
|
"metadata": {
|
|
"colab": {
|
|
"base_uri": "https://localhost:8080/"
|
|
},
|
|
"id": "DRzo_XrCAlrz",
|
|
"outputId": "1afa9bfb-8ce0-4c9b-bdd6-20e3aed5e128"
|
|
},
|
|
"execution_count": null,
|
|
"outputs": [
|
|
{
|
|
"output_type": "stream",
|
|
"name": "stdout",
|
|
"text": [
|
|
"unsat\n"
|
|
]
|
|
}
|
|
]
|
|
}
|
|
]
|
|
} |