From 49da623d8622b9f105bda964b7f8eeba681b2117 Mon Sep 17 00:00:00 2001 From: udlbook <110402648+udlbook@users.noreply.github.com> Date: Mon, 7 Jul 2025 11:18:57 -0400 Subject: [PATCH] Created using Colab --- notebooks/SAT_Exhaustive.ipynb | 248 +++++++++++++++++++++++++++++++++ 1 file changed, 248 insertions(+) create mode 100644 notebooks/SAT_Exhaustive.ipynb diff --git a/notebooks/SAT_Exhaustive.ipynb b/notebooks/SAT_Exhaustive.ipynb new file mode 100644 index 0000000..8693810 --- /dev/null +++ b/notebooks/SAT_Exhaustive.ipynb @@ -0,0 +1,248 @@ +{ + "nbformat": 4, + "nbformat_minor": 0, + "metadata": { + "colab": { + "provenance": [], + "authorship_tag": "ABX9TyOqPerBAXic4uxFN4LNgvJ/", + "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", + "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/iclimbtrees/blob/main/notebooks/SAT_Exhaustive_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", + " # TODO: write this function\n", + " return False ;\n", + "\n", + "def and_op(x_1, x_2):\n", + " # TODO: write this function\n", + " return False\n", + "\n", + "def imp_op(x_1, x_2):\n", + " # TODO: write this function\n", + " return False\n", + "\n", + "def equiv_op(x_1, x_2):\n", + " # TODO: write this function\n", + " return False\n", + "\n", + "def not_op(x_1):\n", + " # TODO: write this function\n", + " return False" + ], + "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 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", + " # TODO: write this function\n", + " # Replace the line below\n", + " phi_val = False\n", + " print(\"phi(\",x_1,\",\",x_2,\",\",x_3,\")=\",phi_val)\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", + " # TODO: write this function\n", + " # You can use three loops or do this in a cleverer way if you know how\n", + " # Replace this line\n", + "\n", + " print(\"UNSAT\")" + ], + "metadata": { + "id": "QBj3Ap3t9CVO" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "code", + "source": [ + "exhaustive_3(phi)" + ], + "metadata": { + "colab": { + "base_uri": "https://localhost:8080/" + }, + "id": "FJGoau6C_fWP", + "outputId": "589979b2-857c-4ff9-f358-d93a008184a1" + }, + "execution_count": null, + "outputs": [ + { + "output_type": "stream", + "name": "stdout", + "text": [ + "UNSAT\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", + " # TODO: write this function\n", + " # Replace this line\n", + " phi_val = False\n", + " print(\"phi(\",x_1,\",\",x_2,\",\",x_3,\")=\",phi_val)\n", + " return phi_val\n" + ], + "metadata": { + "id": "T13sNtofBuLs" + }, + "execution_count": null, + "outputs": [] + }, + { + "cell_type": "code", + "source": [ + "exhaustive_3(phi_1)" + ], + "metadata": { + "colab": { + "base_uri": "https://localhost:8080/" + }, + "id": "qCm_ZdIgCv_P", + "outputId": "642ca068-8c3a-4071-9d3c-e62de00c7f37" + }, + "execution_count": null, + "outputs": [ + { + "output_type": "stream", + "name": "stdout", + "text": [ + "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