264 lines
20 KiB
Plaintext
264 lines
20 KiB
Plaintext
{
|
|
"nbformat": 4,
|
|
"nbformat_minor": 0,
|
|
"metadata": {
|
|
"colab": {
|
|
"provenance": [],
|
|
"authorship_tag": "ABX9TyOQ/cPvllkwhCPc062L9r/d",
|
|
"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_Z3.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": [
|
|
"# The Z3 library\n",
|
|
"\n",
|
|
"The purpose of this Python notebook is to use the Z3 library to solve simple SAT problems. \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://colab.research.google.com/github/udlbook/udlbook/blob/main/Trees/SAT_Z3_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"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"source": [
|
|
"# Example 1\n",
|
|
"\n",
|
|
"Now let's define and implement a Boolean logic formula. We'll use the one from the Tseitin transormation example in the text.\n",
|
|
"\n",
|
|
"$$\\phi:= ((x_{1} \\lor x_{2}) \\Leftrightarrow x_{3}) \\Rightarrow (\\lnot x_{4}).$$"
|
|
],
|
|
"metadata": {
|
|
"id": "aVj9RmuB3ZWJ"
|
|
}
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"source": [
|
|
"First we define the variables:"
|
|
],
|
|
"metadata": {
|
|
"id": "Amv5G3VR3zIJ"
|
|
}
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"source": [
|
|
"x1 = Bool('x1')\n",
|
|
"x2 = Bool('x2')\n",
|
|
"x3 = Bool('x3')\n",
|
|
"x4 = Bool('x4')"
|
|
],
|
|
"metadata": {
|
|
"id": "f0esE71E94fm"
|
|
},
|
|
"execution_count": null,
|
|
"outputs": []
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"source": [
|
|
"Then we define the Boolean logic formula"
|
|
],
|
|
"metadata": {
|
|
"id": "0IIRG5ZWIZV6"
|
|
}
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"source": [
|
|
"phi = Implies(Or(x1, x2)==x3, Not(x4))"
|
|
],
|
|
"metadata": {
|
|
"id": "C0HGBOjI99Ex"
|
|
},
|
|
"execution_count": null,
|
|
"outputs": []
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"source": [
|
|
"Next, we add the logic formula to the solver. If we have multiple constraints, connected by AND functions, we could add them one at a time."
|
|
],
|
|
"metadata": {
|
|
"id": "2Y_1zYOZIoZI"
|
|
}
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"source": [
|
|
"s = Solver()\n",
|
|
"s.add(phi)"
|
|
],
|
|
"metadata": {
|
|
"id": "zQksy42u-qom"
|
|
},
|
|
"execution_count": null,
|
|
"outputs": []
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"source": [
|
|
"Now let's see if this logic formula is satisfiable"
|
|
],
|
|
"metadata": {
|
|
"id": "2lIQSZO8IzOu"
|
|
}
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"source": [
|
|
"print(s.check())"
|
|
],
|
|
"metadata": {
|
|
"id": "fraGSSzV_wTO"
|
|
},
|
|
"execution_count": null,
|
|
"outputs": []
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"source": [
|
|
"We see that it is. Now lets get it to return a set of variables that satisfies the formula"
|
|
],
|
|
"metadata": {
|
|
"id": "BPR2s_otI-ca"
|
|
}
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"source": [
|
|
"print(s.model())"
|
|
],
|
|
"metadata": {
|
|
"id": "kT3GlhUwI8IN"
|
|
},
|
|
"execution_count": null,
|
|
"outputs": []
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"source": [
|
|
"Note that it does not print a value for $x_1$ because the formula is true regardless of the value of $x_1$"
|
|
],
|
|
"metadata": {
|
|
"id": "YL-seZBWJOtG"
|
|
}
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"source": [
|
|
"# Example 2\n",
|
|
"\n",
|
|
"Let's use Z3 if this formula is SAT or UNSAT:\n",
|
|
"\n",
|
|
"$$\\phi_2:= \\bigl(x_{1}\\Rightarrow (\\lnot x_{2}\\land x_{3})\\bigr) \\land \\bigl(x_{2} \\Leftrightarrow (\\lnot x_{3} \\lor x_{1})\\bigr).$$"
|
|
],
|
|
"metadata": {
|
|
"id": "pVAFYHwFJbRw"
|
|
}
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"source": [
|
|
"# TODO Use Z3 to test if this is SAT or UNSAT\n",
|
|
"# 1. Define the formula\n",
|
|
"# 2. Create a new\n",
|
|
"# 3. Add the formula to the solver\n",
|
|
"# 4. Check if SAT or UNSAT\n",
|
|
"# 5. If SAT, then print out a sat of variables that satisfies the formula\n"
|
|
],
|
|
"metadata": {
|
|
"id": "zqdfz1MxJNk1"
|
|
},
|
|
"execution_count": null,
|
|
"outputs": []
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"source": [
|
|
"# Example 3\n",
|
|
"\n",
|
|
"Let's add another clause to the formula and use Z3 if this formula is SAT or UNSAT:\n",
|
|
"\n",
|
|
"$$\\phi_1:= \\bigl(x_{1}\\Rightarrow (\\lnot x_{2}\\land x_{3})\\bigr) \\land \\bigl(x_{2} \\Leftrightarrow (\\lnot x_{3} \\lor x_{1})\\bigr)\\land\\lnot \\bigl(\\lnot x_3 \\Rightarrow x_2\\bigr).$$"
|
|
],
|
|
"metadata": {
|
|
"id": "QAfr332sLyHH"
|
|
}
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"source": [
|
|
"# TODO Use Z3 to test if this is SAT or UNSAT\n",
|
|
"# 1. Define the formula\n",
|
|
"# 2. Create a new\n",
|
|
"# 3. Add the formula to the solver\n",
|
|
"# 4. Check if SAT or UNSAT\n",
|
|
"# 5. If SAT, then print out a sat of variables that satisfies the formula\n"
|
|
],
|
|
"metadata": {
|
|
"id": "fPMvltcyMBGQ"
|
|
},
|
|
"execution_count": null,
|
|
"outputs": []
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"source": [
|
|
"You should fined that this is UNSAT. We have added too many constraints and the three terms that are ANDed together are never simultaneously true."
|
|
],
|
|
"metadata": {
|
|
"id": "ZFW5Z_oWM9TE"
|
|
}
|
|
}
|
|
]
|
|
} |