489 lines
30 KiB
Plaintext
489 lines
30 KiB
Plaintext
{
|
|
"nbformat": 4,
|
|
"nbformat_minor": 0,
|
|
"metadata": {
|
|
"colab": {
|
|
"provenance": [],
|
|
"authorship_tag": "ABX9TyPHpSfq+tkEJ6pqN8jebPBC",
|
|
"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.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",
|
|
"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_Construction_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": [
|
|
"# 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",
|
|
" # TODO Complete this routine\n",
|
|
" # Replace this line:\n",
|
|
" return True"
|
|
],
|
|
"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",
|
|
" # TODO Complete this routine\n",
|
|
" # Replace this line:\n",
|
|
" return True\n",
|
|
"\n",
|
|
"def no_more_than_one(x):\n",
|
|
" # TODO Complete this routine\n",
|
|
" # Replace this line:\n",
|
|
" return True\n",
|
|
"\n",
|
|
"def exactly_one(x):\n",
|
|
" # TODO Complete this routine\n",
|
|
" # Replace this line:\n",
|
|
" return True"
|
|
],
|
|
"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_{0}$$\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",
|
|
" # TODO Complete this routine\n",
|
|
" # Replace this line:\n",
|
|
" return True ;"
|
|
],
|
|
"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",
|
|
" # TODO Complete this routine\n",
|
|
" # Replace this line:\n",
|
|
" return True"
|
|
],
|
|
"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",
|
|
" # TODO Complete this routine\n",
|
|
" # Replace this line:\n",
|
|
" return True"
|
|
],
|
|
"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, here's a useful tip. Z3 actually contains routines for (AtLeast, FewerThanOrEqualToo, and Exactly). Probably faster than enything you can implement yourself!"
|
|
],
|
|
"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": []
|
|
}
|
|
]
|
|
} |