From 9de32ff327779d74a96057ea7305a1f7b80ed01b Mon Sep 17 00:00:00 2001 From: udlbook <110402648+udlbook@users.noreply.github.com> Date: Mon, 15 Dec 2025 15:15:33 -0500 Subject: [PATCH] Delete notebooks/SAT2/EfficientBinarySearch.ipynb --- notebooks/SAT2/EfficientBinarySearch.ipynb | 263 --------------------- 1 file changed, 263 deletions(-) delete mode 100644 notebooks/SAT2/EfficientBinarySearch.ipynb diff --git a/notebooks/SAT2/EfficientBinarySearch.ipynb b/notebooks/SAT2/EfficientBinarySearch.ipynb deleted file mode 100644 index d325996..0000000 --- a/notebooks/SAT2/EfficientBinarySearch.ipynb +++ /dev/null @@ -1,263 +0,0 @@ -{ - "nbformat": 4, - "nbformat_minor": 0, - "metadata": { - "colab": { - "provenance": [], - "authorship_tag": "ABX9TyNHypl2CalLIdc7TxiXks7a", - "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": "jSS2pwvk9D1m" - } - }, - { - "cell_type": "markdown", - "source": [ - "# Efficient binary search\n", - "\n", - "The purpose of this Python notebook is to use conditioning to solve SAT problems by searching through the tree of possible solutions.\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/SAT2/EfficientBinarySearch_Answers.ipynb).\n", - "\n", - "\n", - "Contact me at iclimbtreesmail@gmail.com if you find any mistakes or have any suggestions." - ], - "metadata": { - "id": "h61RTzt_9KE1" - } - }, - { - "cell_type": "markdown", - "source": [ - "To implement efficient binary search, we condition on a variable and its complement and simplify the resulting formula in each case. If the either of the resulting formulas are SAT, then we terminate. If clauses remain in either case, then we condition on the next variable (by calling the same routine recursively). If all branches are UNSAT, then the original expression is UNSAT." - ], - "metadata": { - "id": "oNpA6A9J5bEX" - } - }, - { - "cell_type": "markdown", - "source": [ - "First, let's write a routine that takes a set of clauses and conditions on a literal. It returns a simplified set of clauses or False if it finds a contradiction." - ], - "metadata": { - "id": "1mXmlroE8XUk" - } - }, - { - "cell_type": "code", - "source": [ - "\"\"\" Args:\n", - " clauses: A list of sets, where each set represents a clause\n", - " (e.g., [{1, 2, 3}, {-1, 3, 4}]).\n", - " literal: One literal (e.g., -2)\n", - " \"\"\"\n", - "def condition_on_literal(clauses, literal):\n", - " simplified_clauses = []\n", - " for clause in clauses:\n", - " # 1. If the clause is just the complement of the literal then we have a contradiction\n", - " # and we return False\n", - " # TODO -- Implement this test.\n", - " # Replace this line:\n", - " return False ;\n", - "\n", - " # 2. If the literal is in the clause,\n", - " # the clause is satisfied, so we just move to next clauses\n", - " # TODO -- Implement this test and continue to the next clause if it is present\n", - " # Replace this line:\n", - " return False ;\n", - "\n", - " # 3. If the complement of the literal is in the clause,\n", - " # that literal is falsified, so it is removed from the clause.\n", - " # A copy is made to avoid modifying the original set during iteration.\n", - " new_clause = set(clause)\n", - " # TODO -- modify new_clause if the ngative literal is present\n", - " # Replace this line:\n", - " return False ;\n", - "\n", - " # Append the new (modified or unmodified clause)\n", - " simplified_clauses.append(new_clause)\n", - " return simplified_clauses\n" - ], - "metadata": { - "id": "U8yn8BNJ8KW9" - }, - "execution_count": 73, - "outputs": [] - }, - { - "cell_type": "markdown", - "source": [ - "Then we implement the recursive tree search." - ], - "metadata": { - "id": "saCzeEaVgeoL" - } - }, - { - "cell_type": "code", - "source": [ - "def efficient_tree_search(clauses):\n", - " \"\"\"\n", - " Checks for satisfiability of a SAT formula using\n", - " recursive conditioning\n", - "\n", - " Args:\n", - " clauses: A list of sets, where each set represents a clause\n", - " (e.g., [{1, 2, 3}, {-1, 3, 4}]).\n", - "\n", - " Returns:\n", - " True if the formula is satisfiable, False otherwise.\n", - " \"\"\"\n", - " print(f\"\\nAttempting to solve with clauses: {clauses}\")\n", - "\n", - "\n", - " # Step 1: Check base cases\n", - " if clauses is False:\n", - " print(\" -> Contradiction found. UNSAT.\")\n", - " return False\n", - "\n", - " # Clauses empty, or only one clause with single literal in it\n", - " if not clauses or (len(clauses)==1 and len(clauses[0])==1):\n", - " print(\" -> All clauses satisfied. SAT.\")\n", - " return True\n", - "\n", - " # Step 2: If clauses remain, pick a variable to branch on\n", - " # We'll choose the one with the lowest index, to make this easier\n", - " variable_to_condition = min(abs(literal) for current_clause in clauses for literal in current_clause)\n", - " print(f\"Conditioning on variable: {variable_to_condition}\")\n", - "\n", - " # Step 3: Recursive calls\n", - " print(f\" -> Trying {variable_to_condition} = False\")\n", - " # Create a new list of clauses for the recursive call.\n", - " new_clauses_false = condition_on_literal(clauses, -variable_to_condition)\n", - " print(f\" -> New clauses: {new_clauses_false}\")\n", - " if efficient_tree_search(new_clauses_false):\n", - " return True\n", - "\n", - " # If the above branch returned False, try assigning the variable to\n", - " print(f\" -> Trying {variable_to_condition} = True\")\n", - " # Create a new list of clauses for the recursive call, ensuring it's a list of sets.\n", - " new_clauses_true = condition_on_literal(clauses, variable_to_condition)\n", - " if efficient_tree_search(new_clauses_true):\n", - " return True\n", - "\n", - "\n", - " # If neither assignment leads to a satisfiable solution, the current path is unsatisfiable\n", - " print(f\" -> Both branches for variable {variable_to_condition} led to UNSAT. Backtracking.\")\n", - " print(\"======================================================================================\")\n", - " return False" - ], - "metadata": { - "id": "vAbKbqvuiXVa" - }, - "execution_count": 74, - "outputs": [] - }, - { - "cell_type": "markdown", - "source": [ - "Let's try with the example that created the figure in the unit, which has clauses:\n", - "\n", - "\\begin{align}\n", - "& 1:(x_{1},x_{2}) \\\\\n", - "& 2:(x_{1}, \\overline{x}_{2},\\overline{x}_{3}, x_{4}) \\\\\n", - "& 3:(x_{1},\\overline{x}_{3}, \\overline{x}_{4}) \\\\\n", - "& 4:(\\overline{x}_{1},x_{2}, \\overline{x}_{3}) \\\\\n", - "& 6:(\\overline{x}_{1},x_{2}, \\overline{x}_{4}) \\\\\n", - "& 5:(\\overline{x}_{1},x_{3}, x_{4}) \\\\\n", - "& 7:(\\overline{x}_{2},x_{3}) \\\\\n", - "\\end{align}" - ], - "metadata": { - "id": "PtBS3aU2_yjb" - } - }, - { - "cell_type": "code", - "source": [ - "formula = [{1,2}, {1, -2, -3, 4}, {1, -3, -4}, {-1, 2, -3}, {-1, 2, -4}, {-1, 3, 4}, {-2, 3}]\n", - "current_assignments = set()\n", - "efficient_tree_search(formula)" - ], - "metadata": { - "colab": { - "base_uri": "https://localhost:8080/" - }, - "id": "WBGmpgZli6of", - "outputId": "88dc73ab-0508-4388-8fe3-114676d807c4" - }, - "execution_count": 75, - "outputs": [ - { - "output_type": "stream", - "name": "stdout", - "text": [ - "\n", - "Attempting to solve with clauses: [{1, 2}, {1, 4, -3, -2}, {1, -4, -3}, {2, -3, -1}, {2, -4, -1}, {3, 4, -1}, {3, -2}]\n", - "Conditioning on variable: 1\n", - " -> Trying 1 = False\n", - " -> New clauses: False\n", - "\n", - "Attempting to solve with clauses: False\n", - " -> Contradiction found. UNSAT.\n", - " -> Trying 1 = True\n", - "\n", - "Attempting to solve with clauses: False\n", - " -> Contradiction found. UNSAT.\n", - " -> Both branches for variable 1 led to UNSAT. Backtracking.\n", - "======================================================================================\n" - ] - }, - { - "output_type": "execute_result", - "data": { - "text/plain": [ - "False" - ] - }, - "metadata": {}, - "execution_count": 75 - } - ] - }, - { - "cell_type": "code", - "source": [], - "metadata": { - "id": "Bhd3vERCJsbh" - }, - "execution_count": null, - "outputs": [] - } - ] -} \ No newline at end of file