minimax,_alpha_beta_and_walksat.ipynb

{
  "nbformat": 4,
  "nbformat_minor": 0,
  "metadata": {
    "colab": {
      "provenance": []
    },
    "kernelspec": {
      "name": "python3",
      "display_name": "Python 3"
    },
    "language_info": {
      "name": "python"
    }
  },
  "cells": [
    {
      "cell_type": "code",
      "execution_count": 61,
      "metadata": {
        "id": "GrUHOJpTBLfZ"
      },
      "outputs": [],
      "source": [
        "class Game:\n",
        "    \"\"\"A game is similar to a problem, but it has a utility for each\n",
        "    state and a terminal test instead of a path cost and a goal\n",
        "    test. To create a game, subclass this class and implement actions,\n",
        "    result, utility, and terminal_test. You may override display and\n",
        "    successors or you can inherit their default methods. You will also\n",
        "    need to set the .initial attribute to the initial state; this can\n",
        "    be done in the constructor.\"\"\"\n",
        "\n",
        "    def actions(self, state):\n",
        "        \"\"\"Return a list of the allowable moves at this point.\"\"\"\n",
        "        raise NotImplementedError\n",
        "\n",
        "    def result(self, state, move):\n",
        "        \"\"\"Return the state that results from making a move from a state.\"\"\"\n",
        "        raise NotImplementedError\n",
        "\n",
        "    def utility(self, state, player):\n",
        "        \"\"\"Return the value of this final state to player.\"\"\"\n",
        "        raise NotImplementedError\n",
        "\n",
        "    def terminal_test(self, state):\n",
        "        \"\"\"Return True if this is a final state for the game.\"\"\"\n",
        "        return not self.actions(state)\n",
        "\n",
        "    def to_move(self, state):\n",
        "        \"\"\"Return the player whose move it is in this state.\"\"\"\n",
        "        return state.to_move\n",
        "\n",
        "    def display(self, state):\n",
        "        \"\"\"Print or otherwise display the state.\"\"\"\n",
        "        print(state)\n",
        "\n",
        "    def __repr__(self):\n",
        "        return '<{}>'.format(self.__class__.__name__)\n",
        "\n",
        "    def play_game(self, *players):\n",
        "        \"\"\"Play an n-person, move-alternating game.\"\"\"\n",
        "        state = self.initial\n",
        "        while True:\n",
        "            for player in players:\n",
        "                move = player(self, state)\n",
        "                state = self.result(state, move)\n",
        "                if self.terminal_test(state):\n",
        "                    self.display(state)\n",
        "                    return self.utility(state, self.to_move(self.initial))\n",
        "\n",
        "\n",
        "\n",
        "\n",
        "\n"
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "game = Fig52Game()"
      ],
      "metadata": {
        "id": "zQ7rYqe5BRTU"
      },
      "execution_count": 120,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "game.terminal_test('C')\n"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "ykly5kgyBjyH",
        "outputId": "ef378e75-f047-4a46-96ad-25e5d605728b"
      },
      "execution_count": 124,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "False"
            ]
          },
          "metadata": {},
          "execution_count": 124
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "import copy\n",
        "import itertools\n",
        "import random\n",
        "from collections import namedtuple\n",
        "import numpy as np\n",
        "\n",
        "\n",
        "\n",
        "def minmax_decision(state, game):\n",
        "    \"\"\"Given a state in a game, calculate the best move by searching\n",
        "    forward all the way to the terminal states. [Figure 5.3]\"\"\"\n",
        "\n",
        "    player = game.to_move(state)\n",
        "\n",
        "    def max_value(state):\n",
        "        if game.terminal_test(state):\n",
        "            return game.utility(state, player)\n",
        "        v = -np.inf\n",
        "        for a in game.actions(state):\n",
        "            v = max(v, min_value(game.result(state, a)))\n",
        "        return v\n",
        "\n",
        "    def min_value(state):\n",
        "        if game.terminal_test(state):\n",
        "            return game.utility(state, player)\n",
        "        v = np.inf\n",
        "        for a in game.actions(state):\n",
        "            v = min(v, max_value(game.result(state, a)))\n",
        "        return v\n",
        "\n",
        "    # Body of minmax_decision:\n",
        "    return max(game.actions(state), key=lambda a: min_value(game.result(state, a)))\n",
        "\n",
        "\n",
        "\n"
      ],
      "metadata": {
        "id": "vm6h-pPRBlLj"
      },
      "execution_count": 64,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "minmax_decision('A', game)"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/",
          "height": 35
        },
        "id": "rhXg6ErqBv_8",
        "outputId": "fa0b15e7-b515-460d-9f3c-b7ec24822964"
      },
      "execution_count": 65,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "'a1'"
            ],
            "application/vnd.google.colaboratory.intrinsic+json": {
              "type": "string"
            }
          },
          "metadata": {},
          "execution_count": 65
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "minmax_decision('C', game)"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/",
          "height": 35
        },
        "id": "bUHQHQJgBzw0",
        "outputId": "eee6857f-7040-494e-8a33-ce5fbf9bc4aa"
      },
      "execution_count": 66,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "'c1'"
            ],
            "application/vnd.google.colaboratory.intrinsic+json": {
              "type": "string"
            }
          },
          "metadata": {},
          "execution_count": 66
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "class Fig52Game(Game):\n",
        "    \"\"\"The game represented in [Figure 5.2]. Serves as a simple test case.\"\"\"\n",
        "\n",
        "    succs = dict(A=dict(a1='B', a2='C', a3='D'),\n",
        "                 B=dict(b1='B1', b2='B2', b3='B3'),\n",
        "                 C=dict(c1='C1', c2='C2', c3='C3'),\n",
        "                 D=dict(d1='D1', d2='D2', d3='D3'))\n",
        "    utils = dict(B1=3, B2=12, B3=8, C1=2, C2=4, C3=6, D1=14, D2=5, D3=2)\n",
        "    initial = 'A'\n",
        "\n",
        "    def actions(self, state):\n",
        "        return list(self.succs.get(state, {}).keys())\n",
        "\n",
        "    def result(self, state, move):\n",
        "        return self.succs[state][move]\n",
        "\n",
        "    def utility(self, state, player):\n",
        "        if player == 'MAX':\n",
        "            return self.utils[state]\n",
        "        else:\n",
        "            return -self.utils[state]\n",
        "\n",
        "    def terminal_test(self, state):\n",
        "        return state not in ('A', 'B', 'C', 'D')\n",
        "\n",
        "    def to_move(self, state):\n",
        "        return 'MIN' if state in 'BCD' else 'MAX'\n",
        "\n",
        "\n",
        "class Fig52Extended(Game):\n",
        "    \"\"\"Similar to Fig52Game but bigger. Useful for visualisation\"\"\"\n",
        "\n",
        "    succs = dict(A=dict(a1='B', a2='C', a3='D'),\n",
        "                 B=dict(b1='B1', b2='B2', b3='B3'),\n",
        "                 C=dict(c1='C1', c2='C2', c3='C3'),\n",
        "                 D=dict(d1='D1', d2='D2', d3='D3'),\n",
        "                 E=dict(e1='E1', e2='E2', e3='E3'),\n",
        "                 F=dict(f1='F1', f2='F2', f3='F3'))\n",
        "    utils = dict(B1=3, B2=12, B3=8, C1=2, C2=4, C3=6, D1=14, D2=5, D3=2, E1=7, E2=8, E3=9, F1=4, F2=3, F3=11)\n",
        "\n",
        "    def actions(self, state):\n",
        "        return sorted(list(self.succs.get(state, {}).keys()))\n",
        "\n",
        "    def result(self, state, move):\n",
        "        return self.succs[state][move]\n",
        "\n",
        "    def utility(self, state, player):\n",
        "        if player == 'MAX':\n",
        "            return self.utils[state]\n",
        "        else:\n",
        "            return -self.utils[state]\n",
        "\n",
        "    def terminal_test(self, state):\n",
        "        return state not in ('A', 'B', 'C', 'D', 'E', 'F')\n",
        "\n",
        "    def to_move(self, state):\n",
        "        return 'MIN' if state in 'BCDF' else 'MAX'"
      ],
      "metadata": {
        "id": "ySy2SWYJC4Gs"
      },
      "execution_count": 129,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "game_extended = Fig52Extended()"
      ],
      "metadata": {
        "id": "zxy67OsdDHgt"
      },
      "execution_count": 130,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "minmax_decision('F', game_extended)"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/",
          "height": 35
        },
        "id": "u3taIatvDKzA",
        "outputId": "87474cad-3e2c-4d9d-d829-ac3d77141068"
      },
      "execution_count": 183,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "'f2'"
            ],
            "application/vnd.google.colaboratory.intrinsic+json": {
              "type": "string"
            }
          },
          "metadata": {},
          "execution_count": 183
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "minmax_decision('C', game)"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/",
          "height": 35
        },
        "id": "LmmiEQvWDMzp",
        "outputId": "bc273896-082d-4ef5-b8c7-be7e821c4d96"
      },
      "execution_count": 181,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "'c1'"
            ],
            "application/vnd.google.colaboratory.intrinsic+json": {
              "type": "string"
            }
          },
          "metadata": {},
          "execution_count": 181
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "A=dict(a1='B', a2='C', a3='D')"
      ],
      "metadata": {
        "id": "Nk9Sei6fEMzH"
      },
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "dict(A=dict(a1='B', a2='C', a3='D'))"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "8AwHv4oLF4uQ",
        "outputId": "38176eb7-70ff-43b2-a100-26339f6a7b84"
      },
      "execution_count": null,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "{'A': {'a1': 'B', 'a2': 'C', 'a3': 'D'}}"
            ]
          },
          "metadata": {},
          "execution_count": 42
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "{i: dict(l=i * 3 + 1, m=i * 3 + 2, r=i * 3 + 3) for i in range(13)}"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "W7ha0lRUF5RX",
        "outputId": "7394043f-ad9c-4d6f-d64f-37e39b7c7fd3"
      },
      "execution_count": null,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "{0: {'l': 1, 'm': 2, 'r': 3},\n",
              " 1: {'l': 4, 'm': 5, 'r': 6},\n",
              " 2: {'l': 7, 'm': 8, 'r': 9},\n",
              " 3: {'l': 10, 'm': 11, 'r': 12},\n",
              " 4: {'l': 13, 'm': 14, 'r': 15},\n",
              " 5: {'l': 16, 'm': 17, 'r': 18},\n",
              " 6: {'l': 19, 'm': 20, 'r': 21},\n",
              " 7: {'l': 22, 'm': 23, 'r': 24},\n",
              " 8: {'l': 25, 'm': 26, 'r': 27},\n",
              " 9: {'l': 28, 'm': 29, 'r': 30},\n",
              " 10: {'l': 31, 'm': 32, 'r': 33},\n",
              " 11: {'l': 34, 'm': 35, 'r': 36},\n",
              " 12: {'l': 37, 'm': 38, 'r': 39}}"
            ]
          },
          "metadata": {},
          "execution_count": 43
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "i4V8ggb8eQ7z",
        "outputId": "71a2a926-3f91-4a81-950a-a2275b0a6f40"
      },
      "execution_count": 68,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "{'l': 1, 'm': 2, 'r': 3}"
            ]
          },
          "metadata": {},
          "execution_count": 68
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "def alpha_beta_search(state, game):\n",
        "    \"\"\"Search game to determine best action; use alpha-beta pruning.\n",
        "    As in [Figure 5.7], this version searches all the way to the leaves.\"\"\"\n",
        "\n",
        "    player = game.to_move(state)\n",
        "\n",
        "    # Functions used by alpha_beta\n",
        "    def max_value(state, alpha, beta):\n",
        "        if game.terminal_test(state):\n",
        "            return game.utility(state, player)\n",
        "        v = -np.inf\n",
        "        for a in game.actions(state):\n",
        "            v = max(v, min_value(game.result(state, a), alpha, beta))\n",
        "            if v >= beta:\n",
        "                return v\n",
        "            alpha = max(alpha, v)\n",
        "        return v\n",
        "\n",
        "    def min_value(state, alpha, beta):\n",
        "        if game.terminal_test(state):\n",
        "            return game.utility(state, player)\n",
        "        v = np.inf\n",
        "        for a in game.actions(state):\n",
        "            v = min(v, max_value(game.result(state, a), alpha, beta))\n",
        "            if v <= alpha:\n",
        "                return v\n",
        "            beta = min(beta, v)\n",
        "        return v\n",
        "\n",
        "    # Body of alpha_beta_search:\n",
        "    best_score = -np.inf\n",
        "    beta = np.inf\n",
        "    best_action = None\n",
        "    for a in game.actions(state):\n",
        "        v = min_value(game.result(state, a), best_score, beta)\n",
        "        if v > best_score:\n",
        "            best_score = v\n",
        "            best_action = a\n",
        "    return best_action"
      ],
      "metadata": {
        "id": "jZJj1qvNRFAn"
      },
      "execution_count": 133,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "alpha_beta_search('B', game_extended)"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/",
          "height": 35
        },
        "id": "EM8g5RjdnURf",
        "outputId": "7de26002-b963-4c35-feb6-71c839a9a90b"
      },
      "execution_count": 185,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "'b1'"
            ],
            "application/vnd.google.colaboratory.intrinsic+json": {
              "type": "string"
            }
          },
          "metadata": {},
          "execution_count": 185
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "def WalkSAT(clauses, p=0.5, max_flips=10000):\n",
        "    \"\"\"Checks for satisfiability of all clauses by randomly flipping values of variables\n",
        "    \"\"\"\n",
        "    # Set of all symbols in all clauses\n",
        "    symbols = {sym for clause in clauses for sym in prop_symbols(clause)}\n",
        "    # model is a random assignment of true/false to the symbols in clauses\n",
        "    model = {s: random.choice([True, False]) for s in symbols}\n",
        "    for i in range(max_flips):\n",
        "        satisfied, unsatisfied = [], []\n",
        "        for clause in clauses:\n",
        "            (satisfied if pl_true(clause, model) else unsatisfied).append(clause)\n",
        "        if not unsatisfied:  # if model satisfies all the clauses\n",
        "            return model\n",
        "        clause = random.choice(unsatisfied)\n",
        "        if probability(p):\n",
        "            sym = random.choice(list(prop_symbols(clause)))\n",
        "        else:\n",
        "            # Flip the symbol in clause that maximizes number of sat. clauses\n",
        "            def sat_count(sym):\n",
        "                # Return the the number of clauses satisfied after flipping the symbol.\n",
        "                model[sym] = not model[sym]\n",
        "                count = len([clause for clause in clauses if pl_true(clause, model)])\n",
        "                model[sym] = not model[sym]\n",
        "                return count\n",
        "            sym = argmax(prop_symbols(clause), key=sat_count)\n",
        "        model[sym] = not model[sym]\n",
        "    # If no solution is found within the flip limit, we return failure\n",
        "    return None"
      ],
      "metadata": {
        "id": "JeiFbpVlpwFe"
      },
      "execution_count": 136,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "def WalkSAT_CNF(sentence, p=0.5, max_flips=10000):\n",
        "    return WalkSAT(conjuncts(to_cnf(sentence)), 0, max_flips)"
      ],
      "metadata": {
        "id": "8WEH9Vpg4Cm8"
      },
      "execution_count": 137,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [],
      "metadata": {
        "id": "_OJ8ElnQ4JWY"
      },
      "execution_count": 137,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "!git clone https://github.com/aimacode/aima-python.git"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "1jJhaHkK5UJ9",
        "outputId": "6f7b1ed6-43fe-4663-c540-b28499179028"
      },
      "execution_count": 138,
      "outputs": [
        {
          "output_type": "stream",
          "name": "stdout",
          "text": [
            "Cloning into 'aima-python'...\n",
            "remote: Enumerating objects: 5095, done.\u001b[K\n",
            "remote: Counting objects: 100% (3/3), done.\u001b[K\n",
            "remote: Compressing objects: 100% (3/3), done.\u001b[K\n",
            "remote: Total 5095 (delta 0), reused 1 (delta 0), pack-reused 5092\u001b[K\n",
            "Receiving objects: 100% (5095/5095), 17.71 MiB | 21.51 MiB/s, done.\n",
            "Resolving deltas: 100% (3416/3416), done.\n"
          ]
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "cd aima-python/"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "ZRAW68TP5jAz",
        "outputId": "243d9b12-01f1-43bd-bfce-dc49c884be54"
      },
      "execution_count": 139,
      "outputs": [
        {
          "output_type": "stream",
          "name": "stdout",
          "text": [
            "/content/aima-python/aima-python/aima-python\n"
          ]
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "from utils import *"
      ],
      "metadata": {
        "id": "K6jynOcU5o19"
      },
      "execution_count": 140,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "!pip install ipythonblocks"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "K1dpKhpq7N3S",
        "outputId": "283cbc3c-6328-4583-cf6e-8c95b99d6f5d"
      },
      "execution_count": 141,
      "outputs": [
        {
          "output_type": "stream",
          "name": "stdout",
          "text": [
            "Looking in indexes: https://pypi.org/simple, https://us-python.pkg.dev/colab-wheels/public/simple/\n",
            "Requirement already satisfied: ipythonblocks in /usr/local/lib/python3.7/dist-packages (1.9.0)\n",
            "Requirement already satisfied: ipython>=4.0 in /usr/local/lib/python3.7/dist-packages (from ipythonblocks) (7.9.0)\n",
            "Requirement already satisfied: notebook>=4.0 in /usr/local/lib/python3.7/dist-packages (from ipythonblocks) (5.7.16)\n",
            "Requirement already satisfied: requests>=1.0 in /usr/local/lib/python3.7/dist-packages (from ipythonblocks) (2.23.0)\n",
            "Requirement already satisfied: pexpect in /usr/local/lib/python3.7/dist-packages (from ipython>=4.0->ipythonblocks) (4.8.0)\n",
            "Requirement already satisfied: jedi>=0.10 in /usr/local/lib/python3.7/dist-packages (from ipython>=4.0->ipythonblocks) (0.18.2)\n",
            "Requirement already satisfied: pygments in /usr/local/lib/python3.7/dist-packages (from ipython>=4.0->ipythonblocks) (2.6.1)\n",
            "Requirement already satisfied: traitlets>=4.2 in /usr/local/lib/python3.7/dist-packages (from ipython>=4.0->ipythonblocks) (5.1.1)\n",
            "Requirement already satisfied: prompt-toolkit<2.1.0,>=2.0.0 in /usr/local/lib/python3.7/dist-packages (from ipython>=4.0->ipythonblocks) (2.0.10)\n",
            "Requirement already satisfied: decorator in /usr/local/lib/python3.7/dist-packages (from ipython>=4.0->ipythonblocks) (4.4.2)\n",
            "Requirement already satisfied: pickleshare in /usr/local/lib/python3.7/dist-packages (from ipython>=4.0->ipythonblocks) (0.7.5)\n",
            "Requirement already satisfied: backcall in /usr/local/lib/python3.7/dist-packages (from ipython>=4.0->ipythonblocks) (0.2.0)\n",
            "Requirement already satisfied: setuptools>=18.5 in /usr/local/lib/python3.7/dist-packages (from ipython>=4.0->ipythonblocks) (57.4.0)\n",
            "Requirement already satisfied: parso<0.9.0,>=0.8.0 in /usr/local/lib/python3.7/dist-packages (from jedi>=0.10->ipython>=4.0->ipythonblocks) (0.8.3)\n",
            "Requirement already satisfied: Send2Trash in /usr/local/lib/python3.7/dist-packages (from notebook>=4.0->ipythonblocks) (1.8.0)\n",
            "Requirement already satisfied: pyzmq>=17 in /usr/local/lib/python3.7/dist-packages (from notebook>=4.0->ipythonblocks) (23.2.1)\n",
            "Requirement already satisfied: ipython-genutils in /usr/local/lib/python3.7/dist-packages (from notebook>=4.0->ipythonblocks) (0.2.0)\n",
            "Requirement already satisfied: tornado<7,>=4.1 in /usr/local/lib/python3.7/dist-packages (from notebook>=4.0->ipythonblocks) (6.0.4)\n",
            "Requirement already satisfied: nbconvert<6.0 in /usr/local/lib/python3.7/dist-packages (from notebook>=4.0->ipythonblocks) (5.6.1)\n",
            "Requirement already satisfied: prometheus-client in /usr/local/lib/python3.7/dist-packages (from notebook>=4.0->ipythonblocks) (0.15.0)\n",
            "Requirement already satisfied: nbformat in /usr/local/lib/python3.7/dist-packages (from notebook>=4.0->ipythonblocks) (5.7.0)\n",
            "Requirement already satisfied: terminado>=0.8.1 in /usr/local/lib/python3.7/dist-packages (from notebook>=4.0->ipythonblocks) (0.13.3)\n",
            "Requirement already satisfied: jinja2<=3.0.0 in /usr/local/lib/python3.7/dist-packages (from notebook>=4.0->ipythonblocks) (2.11.3)\n",
            "Requirement already satisfied: jupyter-client<7.0.0,>=5.2.0 in /usr/local/lib/python3.7/dist-packages (from notebook>=4.0->ipythonblocks) (6.1.12)\n",
            "Requirement already satisfied: jupyter-core>=4.4.0 in /usr/local/lib/python3.7/dist-packages (from notebook>=4.0->ipythonblocks) (4.11.2)\n",
            "Requirement already satisfied: ipykernel in /usr/local/lib/python3.7/dist-packages (from notebook>=4.0->ipythonblocks) (5.3.4)\n",
            "Requirement already satisfied: MarkupSafe>=0.23 in /usr/local/lib/python3.7/dist-packages (from jinja2<=3.0.0->notebook>=4.0->ipythonblocks) (2.0.1)\n",
            "Requirement already satisfied: python-dateutil>=2.1 in /usr/local/lib/python3.7/dist-packages (from jupyter-client<7.0.0,>=5.2.0->notebook>=4.0->ipythonblocks) (2.8.2)\n",
            "Requirement already satisfied: mistune<2,>=0.8.1 in /usr/local/lib/python3.7/dist-packages (from nbconvert<6.0->notebook>=4.0->ipythonblocks) (0.8.4)\n",
            "Requirement already satisfied: defusedxml in /usr/local/lib/python3.7/dist-packages (from nbconvert<6.0->notebook>=4.0->ipythonblocks) (0.7.1)\n",
            "Requirement already satisfied: entrypoints>=0.2.2 in /usr/local/lib/python3.7/dist-packages (from nbconvert<6.0->notebook>=4.0->ipythonblocks) (0.4)\n",
            "Requirement already satisfied: bleach in /usr/local/lib/python3.7/dist-packages (from nbconvert<6.0->notebook>=4.0->ipythonblocks) (5.0.1)\n",
            "Requirement already satisfied: pandocfilters>=1.4.1 in /usr/local/lib/python3.7/dist-packages (from nbconvert<6.0->notebook>=4.0->ipythonblocks) (1.5.0)\n",
            "Requirement already satisfied: testpath in /usr/local/lib/python3.7/dist-packages (from nbconvert<6.0->notebook>=4.0->ipythonblocks) (0.6.0)\n",
            "Requirement already satisfied: jsonschema>=2.6 in /usr/local/lib/python3.7/dist-packages (from nbformat->notebook>=4.0->ipythonblocks) (4.3.3)\n",
            "Requirement already satisfied: fastjsonschema in /usr/local/lib/python3.7/dist-packages (from nbformat->notebook>=4.0->ipythonblocks) (2.16.2)\n",
            "Requirement already satisfied: importlib-metadata>=3.6 in /usr/local/lib/python3.7/dist-packages (from nbformat->notebook>=4.0->ipythonblocks) (4.13.0)\n",
            "Requirement already satisfied: zipp>=0.5 in /usr/local/lib/python3.7/dist-packages (from importlib-metadata>=3.6->nbformat->notebook>=4.0->ipythonblocks) (3.10.0)\n",
            "Requirement already satisfied: typing-extensions>=3.6.4 in /usr/local/lib/python3.7/dist-packages (from importlib-metadata>=3.6->nbformat->notebook>=4.0->ipythonblocks) (4.1.1)\n",
            "Requirement already satisfied: attrs>=17.4.0 in /usr/local/lib/python3.7/dist-packages (from jsonschema>=2.6->nbformat->notebook>=4.0->ipythonblocks) (22.1.0)\n",
            "Requirement already satisfied: importlib-resources>=1.4.0 in /usr/local/lib/python3.7/dist-packages (from jsonschema>=2.6->nbformat->notebook>=4.0->ipythonblocks) (5.10.0)\n",
            "Requirement already satisfied: pyrsistent!=0.17.0,!=0.17.1,!=0.17.2,>=0.14.0 in /usr/local/lib/python3.7/dist-packages (from jsonschema>=2.6->nbformat->notebook>=4.0->ipythonblocks) (0.19.2)\n",
            "Requirement already satisfied: six>=1.9.0 in /usr/local/lib/python3.7/dist-packages (from prompt-toolkit<2.1.0,>=2.0.0->ipython>=4.0->ipythonblocks) (1.15.0)\n",
            "Requirement already satisfied: wcwidth in /usr/local/lib/python3.7/dist-packages (from prompt-toolkit<2.1.0,>=2.0.0->ipython>=4.0->ipythonblocks) (0.2.5)\n",
            "Requirement already satisfied: urllib3!=1.25.0,!=1.25.1,<1.26,>=1.21.1 in /usr/local/lib/python3.7/dist-packages (from requests>=1.0->ipythonblocks) (1.24.3)\n",
            "Requirement already satisfied: certifi>=2017.4.17 in /usr/local/lib/python3.7/dist-packages (from requests>=1.0->ipythonblocks) (2022.9.24)\n",
            "Requirement already satisfied: chardet<4,>=3.0.2 in /usr/local/lib/python3.7/dist-packages (from requests>=1.0->ipythonblocks) (3.0.4)\n",
            "Requirement already satisfied: idna<3,>=2.5 in /usr/local/lib/python3.7/dist-packages (from requests>=1.0->ipythonblocks) (2.10)\n",
            "Requirement already satisfied: ptyprocess in /usr/local/lib/python3.7/dist-packages (from terminado>=0.8.1->notebook>=4.0->ipythonblocks) (0.7.0)\n",
            "Requirement already satisfied: webencodings in /usr/local/lib/python3.7/dist-packages (from bleach->nbconvert<6.0->notebook>=4.0->ipythonblocks) (0.5.1)\n"
          ]
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "import heapq\n",
        "import itertools\n",
        "import random\n",
        "from collections import defaultdict, Counter\n",
        "from logic import to_cnf, prop_symbols\n",
        "from utils import remove_all, unique, first, probability, isnumber, issequence, Expr, expr, subexpressions, extend"
      ],
      "metadata": {
        "id": "XWW7Xztq5vXe"
      },
      "execution_count": 142,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "def WalkSAT(clauses, p=0.5, max_flips=10000):\n",
        "    \"\"\"Checks for satisfiability of all clauses by randomly flipping values of variables\n",
        "    >>> WalkSAT([A & ~A], 0.5, 100) is None\n",
        "    True\n",
        "    \"\"\"\n",
        "    # Set of all symbols in all clauses\n",
        "    symbols = {sym for clause in clauses for sym in prop_symbols(clause)}\n",
        "    # model is a random assignment of true/false to the symbols in clauses\n",
        "    model = {s: random.choice([True, False]) for s in symbols}\n",
        "    for i in range(max_flips):\n",
        "        satisfied, unsatisfied = [], []\n",
        "        for clause in clauses:\n",
        "            (satisfied if pl_true(clause, model) else unsatisfied).append(clause)\n",
        "        if not unsatisfied:  # if model satisfies all the clauses\n",
        "            return model\n",
        "        clause = random.choice(unsatisfied)\n",
        "        if probability(p):\n",
        "            sym = random.choice(list(prop_symbols(clause)))\n",
        "        else:\n",
        "            # Flip the symbol in clause that maximizes number of sat. clauses\n",
        "            def sat_count(sym):\n",
        "                # Return the the number of clauses satisfied after flipping the symbol.\n",
        "                model[sym] = not model[sym]\n",
        "                count = len([clause for clause in clauses if pl_true(clause, model)])\n",
        "                model[sym] = not model[sym]\n",
        "                return count\n",
        "\n",
        "            sym = max(prop_symbols(clause), key=sat_count)\n",
        "        model[sym] = not model[sym]\n",
        "    # If no solution is found within the flip limit, we return failure\n",
        "    return None"
      ],
      "metadata": {
        "id": "YQ8EMOzP54_V"
      },
      "execution_count": 143,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "X1, X2, X3, X4, X5, X6 = expr('X1, X2, X3, X4, X5, X6')"
      ],
      "metadata": {
        "id": "wFVZz8GH6obr"
      },
      "execution_count": 162,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "A"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "qG3qLxIu6tEv",
        "outputId": "e7ddab83-4441-4129-d5e3-5b412516da3e"
      },
      "execution_count": 148,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "X1"
            ]
          },
          "metadata": {},
          "execution_count": 148
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "from logic import pl_true, dissociate\n",
        "from numpy import argmax\n",
        "from logic import *\n",
        "\n",
        "WalkSAT([A, B, ~C, D], 0.5, 100)\n"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "Yjekmhhs6uN7",
        "outputId": "085a5442-f0a7-4855-aa0d-e6999e586dac"
      },
      "execution_count": null,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "{B: True, A: True, C: False, D: True}"
            ]
          },
          "metadata": {},
          "execution_count": 55
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "def WalkSAT_CNF(sentence, p=0.5, max_flips=10000):\n",
        "    return WalkSAT(conjuncts(to_cnf(sentence)), 0, max_flips)"
      ],
      "metadata": {
        "id": "p-WhHkCo6xI2"
      },
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "sentence_1 = A |'<=>'| B\n",
        "sentence_2 = (A & B) | (C & ~A) | (B & ~D)\n",
        "sentence_3 = (A | (B & C)) |'<=>'| ((A | B) & (A | C))"
      ],
      "metadata": {
        "id": "ECrKnlDv8Oat"
      },
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "sentence_1\n"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "I0kOEK0R8UPV",
        "outputId": "2bcbd036-2656-48a6-9dc5-4d54b9c673ec"
      },
      "execution_count": null,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "(A <=> B)"
            ]
          },
          "metadata": {},
          "execution_count": 58
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "WalkSAT_CNF(sentence_1)\n",
        "WalkSAT_CNF(sentence_2)\n",
        "WalkSAT_CNF(sentence_3)\n"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "BUct0Rn-8WOh",
        "outputId": "9d49f70a-f038-4137-f366-f7c3e8c51fee"
      },
      "execution_count": null,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "{B: False, A: False, C: False}"
            ]
          },
          "metadata": {},
          "execution_count": 59
        }
      ]
    },
    {
      "cell_type": "markdown",
      "source": [
        "\n",
        "\n",
        "```\n",
        "Here are the 3-CNF inputs used\n",
        "\n",
        "1) (x1 v x2 v x3) ^ (~x1 v ~x2) ^ (~x1 v ~x3) ^ (~x2 v x3) ^ (x1 v ~x3)\n",
        "\n",
        "2) (~x1 v x2) ^ (~x2 v ~x3 v x4) ^ (~x3 v ~x4 v x5) ^ (x1 v ~x4 v x5) ^ ~(x1 v x2 v x3)\n",
        "\n",
        "3) (x1 ^ ~x2 ^ ~x3) v (~x1 ^ x2 ^ x3) v (x1 ^ ~x2 ^ x3) v (x1 ^ x2 ^ ~x3)\n",
        "\n",
        "4) (~x1 v x2 v x3) ^ (~x1 v ~x2 v x3) ^ (~x1 v ~x2 v ~x3) ^ (x2 v ~x3) ^ (x3 v x4)\n",
        "\n",
        "5) (~x1 v x2) ^ (~x1 v ~x2 v x3) ^ (~x2 v ~x3 v x4) ^ (~x3 v ~x4 v x5) ^ (~x4 v ~x5 v x6)\n",
        "\n",
        "6) (x1 ^ ~x2 ^ x3) v (~x1 ^ x2 ^ ~x3) v (x1 ^ x2 ^ x3) v (~x1 ^ ~x2 ^ ~x3) v (x2 v x3)\n",
        "\n",
        "# 7) (~x1 v ~x2 v x3) ^ (~x1 v x2 v ~x3) ^ (x1 v ~x2 v ~x3) ^ (~x3 v x4) ^ (x1 v x2 v x3)\n",
        "\n",
        "8) (~x1 v ~x2) ^ (~x1 v ~x2 v x3) ^ (~x1 v ~x2 v ~x3) ^ (~x2 v ~x3 v ~x4) ^ (x4 v ~x5)\n",
        "\n",
        "9) (x1 ^ x2 ^ ~x3) v (~x1 ^ x2 ^ x3) v (~x1 ^ ~x2 ^ x3) v (~x1 ^ ~x2 ^ ~x3) v (x2 v ~x3)\n",
        "\n",
        "10) (~x1 v ~x2 v ~x3) ^ (x1 v ~x2 v x3) ^ (~x1 v x2 v x3) ^ (~x2 v ~x3 v x4) ^ (x1 v ~x2 v ~x3)\n",
        "```\n",
        "\n"
      ],
      "metadata": {
        "id": "2T9OCyL6n7Ls"
      }
    },
    {
      "cell_type": "code",
      "source": [
        "sent1 = ((X1 | X2 | X3) & (~X1 | ~X2) ^ (~X1 | ~X3) & (~X2 | X3) & (X1 | ~X3))"
      ],
      "metadata": {
        "id": "mQrLAGxjoVJC"
      },
      "execution_count": 149,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "WalkSAT_CNF(sent1)"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "Ed98N_5rqJsz",
        "outputId": "babb6358-be6b-4389-8c0d-d48bb5272a91"
      },
      "execution_count": 152,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "{X3: True, X1: False, X2: False}"
            ]
          },
          "metadata": {},
          "execution_count": 152
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "sent2 = ((~X1 | X2) & (~X2 | ~X3 | X4) & (~X3 | ~X4 | X5) & (X1 | ~X4 | X5) & ~(X1 | X2 | X3))"
      ],
      "metadata": {
        "id": "Wpq9wlnIqKsN"
      },
      "execution_count": 153,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "sent2"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "uAHfLK2Pq9s_",
        "outputId": "c0562b4d-9fb5-42f8-9324-4cdc7a62361b"
      },
      "execution_count": 154,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "(((((~X1 | X2) & ((~X2 | ~X3) | X4)) & ((~X3 | ~X4) | X5)) & ((X1 | ~X4) | X5)) & ~((X1 | X2) | X3))"
            ]
          },
          "metadata": {},
          "execution_count": 154
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "WalkSAT_CNF(sent2)"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "4N9teVJIq_Tk",
        "outputId": "e81634d5-013b-434e-d718-402578e53cff"
      },
      "execution_count": 155,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "{X3: False, X4: True, X2: False, X1: False, X5: True}"
            ]
          },
          "metadata": {},
          "execution_count": 155
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "# 3) (x1 ^ ~x2 ^ ~x3) v (~x1 ^ x2 ^ x3) v (x1 ^ ~x2 ^ x3) v (x1 ^ x2 ^ ~x3)\n",
        "sent3 = ((X1 & ~X2 & ~X3) | (~X1 & X2 & X3) | (X1 & ~X2 & X3) | (X1 & X2 & ~X3))"
      ],
      "metadata": {
        "id": "cZ-HF7_nrBbk"
      },
      "execution_count": 156,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "WalkSAT_CNF(sent3)"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "f_h6Otrerjbp",
        "outputId": "1beaaba9-9672-47ef-bdb6-f04d898a7e6d"
      },
      "execution_count": 157,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "{X3: False, X1: True, X2: False}"
            ]
          },
          "metadata": {},
          "execution_count": 157
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "# (~x1 v x2 v x3) ^ (~x1 v ~x2 v x3) ^ (~x1 v ~x2 v ~x3) ^ (x2 v ~x3) ^ (x3 v x4)\n",
        "\n",
        "sent4 = ((~X1 | X2 | X3) & (~X1 | ~X2 | X3) & (~X1 | ~X2 | ~X3) & (X2 | ~X3) & (X3 | X4))"
      ],
      "metadata": {
        "id": "ZjhX898-rlqi"
      },
      "execution_count": 159,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "sent4"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "K2xbSBHXr_UL",
        "outputId": "34bf9f1b-103a-4b42-e0d9-2117ecfdd963"
      },
      "execution_count": 160,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "((((((~X1 | X2) | X3) & ((~X1 | ~X2) | X3)) & ((~X1 | ~X2) | ~X3)) & (X2 | ~X3)) & (X3 | X4))"
            ]
          },
          "metadata": {},
          "execution_count": 160
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "WalkSAT_CNF(sent4)"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "yIzZRJJysF9W",
        "outputId": "fbff6b62-1ebf-43ad-b286-3a61463ee6b1"
      },
      "execution_count": 161,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "{X4: True, X3: False, X1: False, X2: False}"
            ]
          },
          "metadata": {},
          "execution_count": 161
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "# (~x1 v x2) ^ (~x1 v ~x2 v x3) ^ (~x2 v ~x3 v x4) ^ (~x3 v ~x4 v x5) ^ (~x4 v ~x5 v x6)\n",
        "\n",
        "sent5 = ((~X1 | X2) & (~X1 | ~X2 | X3) & (~X2 | ~X3 |X4) & (~X3 | ~X4 | X5) & (~X4 | ~X5 | X6))"
      ],
      "metadata": {
        "id": "YeyUMuQqsIs8"
      },
      "execution_count": 163,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "sent5"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "AKJxGKq7snEF",
        "outputId": "f7f4cca0-4a22-4b2a-e924-c801b1412830"
      },
      "execution_count": 164,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "(((((~X1 | X2) & ((~X1 | ~X2) | X3)) & ((~X2 | ~X3) | X4)) & ((~X3 | ~X4) | X5)) & ((~X4 | ~X5) | X6))"
            ]
          },
          "metadata": {},
          "execution_count": 164
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "WalkSAT_CNF(sent5)"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "ydn7ssdxso6N",
        "outputId": "451e1516-fc16-45a1-932c-86b90710b3b4"
      },
      "execution_count": 166,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "{X3: False, X6: True, X4: True, X2: True, X1: False, X5: True}"
            ]
          },
          "metadata": {},
          "execution_count": 166
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "# (x1 ^ ~x2 ^ x3) v (~x1 ^ x2 ^ ~x3) v (x1 ^ x2 ^ x3) v (~x1 ^ ~x2 ^ ~x3) v (x2 v x3)\n",
        "\n",
        "sent6 = ((X1 & ~X2 & X3) | (~X1 & X2 & ~X3) | (X1 & X2 & X3) | (~X1 & ~X2 & ~X3) | (X2 | X3))"
      ],
      "metadata": {
        "id": "Q3NHG03lsqoK"
      },
      "execution_count": 167,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "WalkSAT_CNF(sent6)"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "YoDErBbstENY",
        "outputId": "ba60ed49-c69b-48f1-a4c7-23d8a941ca91"
      },
      "execution_count": 168,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "{X3: False, X1: True, X2: True}"
            ]
          },
          "metadata": {},
          "execution_count": 168
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "# (~x1 v ~x2 v x3) ^ (~x1 v x2 v ~x3) ^ (x1 v ~x2 v ~x3) ^ (~x3 v x4) ^ (x1 v x2 v x3)\n",
        "sent7 = ((~X1 | ~X2 | X3) & (~X1 | X2 | ~X3) & (X1 | ~X2 | ~X3) & (~X3 | X4) & (X1 | X2 |X3))"
      ],
      "metadata": {
        "id": "uJMAcIxItGrH"
      },
      "execution_count": 169,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "WalkSAT_CNF(sent7)"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "JLtYjibytavL",
        "outputId": "c04e66aa-2b8c-4547-e298-eb3c734cdb83"
      },
      "execution_count": 170,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "{X4: False, X3: False, X1: True, X2: False}"
            ]
          },
          "metadata": {},
          "execution_count": 170
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "# (~x1 v ~x2) ^ (~x1 v ~x2 v x3) ^ (~x1 v ~x2 v ~x3) ^ (~x2 v ~x3 v ~x4) ^ (x4 v ~x5)\n",
        "\n",
        "sent8 = ((~X1 | ~X2) & (~X1 | ~X2 | X3) & (~X1 | ~X2 | ~X3) & (~X2 | ~X3 | ~X4) & (X4 | ~X5))"
      ],
      "metadata": {
        "id": "ovF9WYj3tdkf"
      },
      "execution_count": 171,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "WalkSAT_CNF(sent8)"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "WZ6lLZPhtzkh",
        "outputId": "41f1cef2-1b81-4945-bfc2-01ec2a5bb0ab"
      },
      "execution_count": 172,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "{X3: False, X4: True, X2: True, X1: False, X5: True}"
            ]
          },
          "metadata": {},
          "execution_count": 172
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "# (x1 ^ x2 ^ ~x3) v (~x1 ^ x2 ^ x3) v (~x1 ^ ~x2 ^ x3) v (~x1 ^ ~x2 ^ ~x3) v (x2 v ~x3)\n",
        "sent9 = ((X1 & X2 & ~X3) | (~X1 & X2 & X3) | (~X1 & ~X2 & X3) | (~X1 & ~X2 & ~X3) | (X2 | ~X3))"
      ],
      "metadata": {
        "id": "1ZUQ6Di7t1vU"
      },
      "execution_count": 173,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "WalkSAT_CNF(sent9)"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "hYi2z5PmuOTt",
        "outputId": "3e6b1ab0-49c2-42a0-a8a3-9ba73920a6fb"
      },
      "execution_count": 174,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "{X3: True, X1: True, X2: True}"
            ]
          },
          "metadata": {},
          "execution_count": 174
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "# (~x1 v ~x2 v ~x3) ^ (x1 v ~x2 v x3) ^ (~x1 v x2 v x3) ^ (~x2 v ~x3 v x4) ^ (x1 v ~x2 v ~x3)\n",
        "\n",
        "sent10 = ((~X1 | ~X2 | ~X3) & (X1 | ~X2 | X3) & (~X1 | X2 | X3) & (~X2 | ~X3 | X4) & (X1 | ~X2 | ~X3))"
      ],
      "metadata": {
        "id": "rToRXGetuQWm"
      },
      "execution_count": 175,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "WalkSAT_CNF(sent10)"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "cZIDjP1vukvf",
        "outputId": "f1275b1f-27d2-4945-9d3d-18c528fd077b"
      },
      "execution_count": 176,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "{X4: False, X3: False, X1: True, X2: True}"
            ]
          },
          "metadata": {},
          "execution_count": 176
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "%%timeit\n",
        "\n",
        "WalkSAT_CNF(sent1)\n",
        "WalkSAT_CNF(sent2)\n",
        "WalkSAT_CNF(sent3)\n",
        "WalkSAT_CNF(sent4)\n",
        "WalkSAT_CNF(sent5)\n",
        "WalkSAT_CNF(sent6)\n",
        "WalkSAT_CNF(sent7)\n",
        "WalkSAT_CNF(sent8)\n",
        "WalkSAT_CNF(sent9)\n",
        "WalkSAT_CNF(sent10)"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "8JJyYMjquopQ",
        "outputId": "30dcca04-4f0d-4895-c88d-84a57011063c"
      },
      "execution_count": 179,
      "outputs": [
        {
          "output_type": "stream",
          "name": "stdout",
          "text": [
            "16.2 ms ± 167 µs per loop (mean ± std. dev. of 7 runs, 100 loops each)\n"
          ]
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [],
      "metadata": {
        "id": "bZebGek4vDAk"
      },
      "execution_count": null,
      "outputs": []
    }
  ]
}