diff --git a/Trees/SAT_Tseitin.ipynb b/Trees/SAT_Tseitin.ipynb new file mode 100644 index 0000000..fc279b8 --- /dev/null +++ b/Trees/SAT_Tseitin.ipynb @@ -0,0 +1,251 @@ +{ + "nbformat": 4, + "nbformat_minor": 0, + "metadata": { + "colab": { + "provenance": [], + "authorship_tag": "ABX9TyO30jtLgfo4lSQLEOV3NJw3", + "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": [ + "\"Open" + ] + }, + { + "cell_type": "markdown", + "source": [ + "" + ], + "metadata": { + "id": "9Qgup23vwdll" + } + }, + { + "cell_type": "markdown", + "source": [ + "# The Tseitin transformation\n", + "\n", + "The purpose of this Python notebook is to check that the Tseitin transformation example in the text is correct. Once we have the formula in conjunctive normal form, we can use the Python SAT library Z3 to solve 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_Tseitin_Answers.ipynb).\n", + "\n", + "Contact me at iclimbtreesmail@gmail.com if you find any mistakes or have any suggestions." + ], + "metadata": { + "id": "uORlKyPv02ge" + } + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": { + "id": "bbF6SE_F0tU8" + }, + "outputs": [], + "source": [ + "# Math library\n", + "import numpy as np" + ] + }, + { + "cell_type": "markdown", + "source": [ + "# Boolean operators\n", + "\n", + "First, let's write some functions for the five Boolean operators discussed in the unit. " + ], + "metadata": { + "id": "8z_AvPoU6zck" + } + }, + { + "cell_type": "code", + "source": [ + "def or_op(x_1, x_2):\n", + " return x_1 or x_2 ;\n", + "\n", + "def and_op(x_1, x_2):\n", + " return x_1 and x_2\n", + "\n", + "def imp_op(x_1, x_2):\n", + " return not x_1 or x_2\n", + "\n", + "def equiv_op(x_1, x_2):\n", + " return x_1==x_2\n", + "\n", + "def not_op(x_1):\n", + " return not x_1" + ], + "metadata": { + "id": "ogfjSL857Dlo" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "markdown", + "source": [ + "# Example Boolean Logic Formula\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": "e3a1Ps1D8kUH" + } + }, + { + "cell_type": "code", + "source": [ + "def phi(x_1, x_2, x_3, x_4):\n", + " phi_val = imp_op(equiv_op(or_op(x_1, x_2), x_3), not_op(x_4))\n", + " return phi_val" + ], + "metadata": { + "id": "yBPbxHTL8xOl" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "markdown", + "source": [ + "# Exhaustive SAT\n", + "\n", + "Now let's implement an exhaustive SAT solver. For each possible combination of $x_1$, $x_2$, and $x_3$, we evaluate the Boolean logic formula $\\phi$. If it evaluates to **true** for any of these combinations then the function is **SAT**. Otherwise, it is **UNSAT**." + ], + "metadata": { + "id": "OeRG0RB-9HP4" + } + }, + { + "cell_type": "code", + "source": [ + "def exhaustive_3(phi):\n", + " is_sat = False\n", + " for t in range (np.power(2,4)):\n", + " x_1 = (t % 2) >= 1\n", + " x_2 = (t % 4) >= 2\n", + " x_3 = (t % 8) >= 4\n", + " x_4 = (t % 16) >= 8\n", + " this_phi = phi(x_1, x_2, x_3,x_4)\n", + " print(\"phi(\",x_1,\",\",x_2,\",\",x_3,\",\",x_4,\")=\",this_phi)\n", + "\n", + " is_sat = is_sat or this_phi\n", + "\n", + " if is_sat:\n", + " print(\"Phi is SAT\")\n", + " else:\n", + " print(\"Phi is UNSAT\")" + ], + "metadata": { + "id": "QBj3Ap3t9CVO" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "code", + "source": [ + "exhaustive_3(phi)" + ], + "metadata": { + "id": "FJGoau6C_fWP" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "markdown", + "source": [ + "This is the same formula expressed in conjunctive normal form (see main text). The variables $y_1, y_2, y_3, y_4$ are extra terms that were needed to do this conversion. Their final values do not matter.\n", + "\n", + "$$\\begin{align}\\phi_2&:= y_{4} \\land (y_4\\lor y_2) \\land (y_4 \\lor \\lnot y_3) \\land (\\lnot y_4 \\lor \\lnot y_2 \\lor y_3)\\nonumber \\\\\n", + "&\\hspace{0.4cm}\\land (y_3 \\lor x_4) \\land (\\lnot y_3 \\lor \\lnot x_4)\\nonumber\\\\\n", + "& \\hspace{0.4cm}\\land (\\lnot y_2 \\lor \\lnot y_1 \\lor x_3)\\land (\\lnot y_2 \\lor y_1 \\lor \\lnot x_3) \\land (y_2 \\lor \\lnot y_1 \\lor \\lnot x_3) \\land (y_2\\lor y_1\\lor x_3)\\nonumber \\\\&\n", + "\\hspace{0.4cm}\\land (y_1\\lor \\lnot x_1) \\land (y_1 \\lor \\lnot x_2) \\land (\\lnot y_1 \\lor x_1 \\lor x_2). \\end{align}$$" + ], + "metadata": { + "id": "MSTx8YXlmycP" + } + }, + { + "cell_type": "code", + "source": [ + "def phi_2(x_1, x_2, x_3, x_4, y_1, y_2, y_3, y_4):\n", + " return y_4 and (y_4 or y_2) and (y_4 or not y_3) and (not y_4 or not y_2 or y_3) \\\n", + " and (y_3 or x_4) and (not y_3 or not x_4) and (not y_2 or not y_1 or x_3) and (not y_2 or y_1 or not x_3) \\\n", + " and (y_2 or not y_1 or not x_3) and (y_2 or y_1 or x_3) and (y_1 or not x_1) and (y_1 or not x_2) and (not y_1 or x_1 or x_2)" + ], + "metadata": { + "id": "z7wZRlrjnpK9" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "code", + "source": [ + "def exhaustive_8(phi):\n", + " is_sat = False\n", + "\n", + " # TODO Complete this routine to test whether phi is SAT\n", + " # You now need to iterate over 8 variables (x1,x2,x3,x4,y1,y2,y3,y4)\n", + " # However, the values of y1,y2,y3,y4 don't matter.\n", + " # A given configuration of x_1, x_2, x_3, x_4 is satisfiable if the formula\n", + " # returns true for ANY of the 16 possible values of y_1, y_2, y_3, y_4\n", + " # Print out the results in the same format as above\n", + "\n", + " if is_sat:\n", + " print(\"Phi is SAT\")\n", + " else:\n", + " print(\"Phi is UNSAT\")" + ], + "metadata": { + "id": "YZNCyXCGmiiG" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "code", + "source": [ + "exhaustive_8(phi_2)" + ], + "metadata": { + "id": "qCm_ZdIgCv_P" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "markdown", + "source": [ + "You should see that the truth tables are the same for both the original and Tseitin transformed formulae. The two formulations are equivalent. Notice thought that we pay a cost for this simplification in that we have to add four more variables $y_1, y_2, y_3, y_4$ and so potentially have to iterate over 16 times the number of combinations." + ], + "metadata": { + "id": "iyIYwgwvhUXO" + } + } + ] +} \ No newline at end of file