From 2c6e1cb9f89119aecc875c29cf8f2bac04e501bd Mon Sep 17 00:00:00 2001 From: udlbook <110402648+udlbook@users.noreply.github.com> Date: Tue, 4 Mar 2025 16:32:31 -0500 Subject: [PATCH] Created using Colab --- Trees/SAT_Exhaustive_Answers.ipynb | 250 +++++++++++++++++++++++++++++ 1 file changed, 250 insertions(+) create mode 100644 Trees/SAT_Exhaustive_Answers.ipynb diff --git a/Trees/SAT_Exhaustive_Answers.ipynb b/Trees/SAT_Exhaustive_Answers.ipynb new file mode 100644 index 0000000..a71f255 --- /dev/null +++ b/Trees/SAT_Exhaustive_Answers.ipynb @@ -0,0 +1,250 @@ +{ + "nbformat": 4, + "nbformat_minor": 0, + "metadata": { + "colab": { + "provenance": [], + "authorship_tag": "ABX9TyM5J6fIsz12gt3/KyELcoXi", + "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": [ + "# Boolean logic formulae and exhaustive SAT algorithms\n", + "\n", + "The purpose of this Python notebook experiment with an exhuastive algorithm for SAT solving.\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": "uORlKyPv02ge" + } + }, + { + "cell_type": "code", + "execution_count": 1, + "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": 6, + "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 text.\n", + "\n", + "$$\\phi:= \\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": "e3a1Ps1D8kUH" + } + }, + { + "cell_type": "code", + "source": [ + "def phi(x_1, x_2, x_3):\n", + " phi_val = and_op(imp_op(x_1, and_op(not_op(x_2), x_3)),equiv_op(x_2, or_op(not_op(x_3), x_1)))\n", + " print(\"phi(\",x_1,\",\",x_2,\",\",x_3,\")=\",phi_val)\n", + " return phi_val" + ], + "metadata": { + "id": "yBPbxHTL8xOl" + }, + "execution_count": 7, + "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", + " for t in range (np.power(2,3)):\n", + " x_1 = (t % 2) >= 1\n", + " x_2 = (t % 4) >= 2\n", + " x_3 = (t % 8) >= 4\n", + " phi_val = phi(x_1, x_2, x_3)\n", + " if phi_val:\n", + " print(\"SAT\")\n", + " return\n", + " print(\"UNSAT\")" + ], + "metadata": { + "id": "QBj3Ap3t9CVO" + }, + "execution_count": 14, + "outputs": [] + }, + { + "cell_type": "code", + "source": [ + "exhaustive_3(phi)" + ], + "metadata": { + "colab": { + "base_uri": "https://localhost:8080/" + }, + "id": "FJGoau6C_fWP", + "outputId": "a841116e-8e8a-400f-a560-b52c670e6b0a" + }, + "execution_count": 15, + "outputs": [ + { + "output_type": "stream", + "name": "stdout", + "text": [ + "phi( False , False , False )= False\n", + "phi( True , False , False )= False\n", + "phi( False , True , False )= True\n", + "SAT\n" + ] + } + ] + }, + { + "cell_type": "markdown", + "source": [ + "How about if we add another constraint (by logically ANDing another term)?\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": "nnHxv9IHB185" + } + }, + { + "cell_type": "code", + "source": [ + "def phi_1(x_1, x_2, x_3):\n", + " phi_val = and_op(and_op(imp_op(x_1, and_op(not_op(x_2), x_3)),equiv_op(x_2, or_op(not_op(x_3), x_1))),not_op(imp_op(not_op(x_3), x_2)))\n", + " print(\"phi(\",x_1,\",\",x_2,\",\",x_3,\")=\",phi_val)\n", + " return phi_val\n" + ], + "metadata": { + "id": "T13sNtofBuLs" + }, + "execution_count": 24, + "outputs": [] + }, + { + "cell_type": "code", + "source": [ + "exhaustive_3(phi_1)" + ], + "metadata": { + "colab": { + "base_uri": "https://localhost:8080/" + }, + "id": "qCm_ZdIgCv_P", + "outputId": "f1cbb656-9f4d-4b68-b347-876ada5fb926" + }, + "execution_count": 25, + "outputs": [ + { + "output_type": "stream", + "name": "stdout", + "text": [ + "phi( False , False , False )= False\n", + "phi( True , False , False )= False\n", + "phi( False , True , False )= False\n", + "phi( True , True , False )= False\n", + "phi( False , False , True )= False\n", + "phi( True , False , True )= False\n", + "phi( False , True , True )= False\n", + "phi( True , True , True )= False\n", + "UNSAT\n" + ] + } + ] + }, + { + "cell_type": "markdown", + "source": [ + "You should fined that this is **UNSAT**. We have added too many constraints and the three terms that are **AND**ed together are never simultaneously true." + ], + "metadata": { + "id": "nlsUlJQfDB14" + } + } + ] +} \ No newline at end of file