minimax,_alpha_beta_and_walksat (2).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": 25,
      "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": [
        "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": 26,
      "outputs": []
    },
    {
      "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'),\n",
        "                 B=dict(b1='D', b2='E'),\n",
        "                 C=dict(c1='F', c2='G'),\n",
        "                 D=dict(d1='H', d2='I'),\n",
        "                 E=dict(e1='J', e2='K'),\n",
        "                 F=dict(f1='L', f2='M'),\n",
        "                 G=dict(g1='N', g2='O'),\n",
        "                 H=dict(h1='h1', h2='h2'),\n",
        "                 I=dict(i1='i1', i2='i2'),\n",
        "                 J=dict(j1='j1', j2='j2'),\n",
        "                 K=dict(k1='k1', k2='k2'),\n",
        "                 L=dict(l1='l1', l2='l2'),\n",
        "                 M=dict(m1='m1', m2='m2'),\n",
        "                 N=dict(n1='n1', n2='n2'),\n",
        "                 O=dict(o1='o1', o2='o2'))\n",
        "    utils = dict(h1=84, h2=-29, i1=-37, i2=-25, j1=1, j2=-43, k1=-75, k2=49, l1=-21, l2=-51, m1=58, m2=-46, n1=-3, n2=-13, o1=26, o2=79)\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', 'G', 'H', 'I', 'J', 'K', 'L', 'M', 'N', 'O')\n",
        "\n",
        "    def to_move(self, state):\n",
        "        return 'MIN' if state in 'BCHILMNO' else 'MAX'"
      ],
      "metadata": {
        "id": "ySy2SWYJC4Gs"
      },
      "execution_count": 79,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "game_extended = Fig52Extended()"
      ],
      "metadata": {
        "id": "zxy67OsdDHgt"
      },
      "execution_count": 82,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "minmax_decision('K', game_extended)"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/",
          "height": 35
        },
        "id": "u3taIatvDKzA",
        "outputId": "f8548b22-b496-4d08-8726-55b944f34b98"
      },
      "execution_count": 89,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "'k2'"
            ],
            "application/vnd.google.colaboratory.intrinsic+json": {
              "type": "string"
            }
          },
          "metadata": {},
          "execution_count": 89
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "game = Fig52Game()"
      ],
      "metadata": {
        "id": "9LpJ6m4mopvb"
      },
      "execution_count": 84,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "minmax_decision('D', game)"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/",
          "height": 35
        },
        "id": "LmmiEQvWDMzp",
        "outputId": "785d4542-61f6-41b6-cd58-c7df68f5ad2f"
      },
      "execution_count": 86,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "'d3'"
            ],
            "application/vnd.google.colaboratory.intrinsic+json": {
              "type": "string"
            }
          },
          "metadata": {},
          "execution_count": 86
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "A=dict(a1='B', a2='C', a3='D')"
      ],
      "metadata": {
        "id": "Nk9Sei6fEMzH"
      },
      "execution_count": 32,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "dict(A=dict(a1='B', a2='C', a3='D'))"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "8AwHv4oLF4uQ",
        "outputId": "dc70e44f-1249-4012-d045-1c672a4abb89"
      },
      "execution_count": 33,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "{'A': {'a1': 'B', 'a2': 'C', 'a3': 'D'}}"
            ]
          },
          "metadata": {},
          "execution_count": 33
        }
      ]
    },
    {
      "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": "63da1db9-51b9-4c5a-94cd-26c656175719"
      },
      "execution_count": 34,
      "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": 34
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [],
      "metadata": {
        "id": "i4V8ggb8eQ7z"
      },
      "execution_count": 34,
      "outputs": []
    },
    {
      "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": 35,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "alpha_beta_search('B', game_extended)"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/",
          "height": 35
        },
        "id": "EM8g5RjdnURf",
        "outputId": "30adce9d-451b-402d-c491-74c971412273"
      },
      "execution_count": 90,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "'b2'"
            ],
            "application/vnd.google.colaboratory.intrinsic+json": {
              "type": "string"
            }
          },
          "metadata": {},
          "execution_count": 90
        }
      ]
    },
    {
      "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": 91,
      "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": 92,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [],
      "metadata": {
        "id": "_OJ8ElnQ4JWY"
      },
      "execution_count": 38,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "!git clone https://github.com/aimacode/aima-python.git"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "1jJhaHkK5UJ9",
        "outputId": "2df8480a-2901-4b61-c3db-2ebd909f5d09"
      },
      "execution_count": 93,
      "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 | 26.39 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": "7db1ae9f-63ec-4562-bfa2-2d8f60dde448"
      },
      "execution_count": 94,
      "outputs": [
        {
          "output_type": "stream",
          "name": "stdout",
          "text": [
            "/content/aima-python/aima-python\n"
          ]
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "from utils import *"
      ],
      "metadata": {
        "id": "K6jynOcU5o19"
      },
      "execution_count": 95,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "!pip install ipythonblocks"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "K1dpKhpq7N3S",
        "outputId": "aca571c9-f586-46b6-9227-dce909e23a75"
      },
      "execution_count": 96,
      "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: requests>=1.0 in /usr/local/lib/python3.7/dist-packages (from ipythonblocks) (2.23.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: pygments in /usr/local/lib/python3.7/dist-packages (from ipython>=4.0->ipythonblocks) (2.6.1)\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: jedi>=0.10 in /usr/local/lib/python3.7/dist-packages (from ipython>=4.0->ipythonblocks) (0.18.2)\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: setuptools>=18.5 in /usr/local/lib/python3.7/dist-packages (from ipython>=4.0->ipythonblocks) (57.4.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: 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: pickleshare in /usr/local/lib/python3.7/dist-packages (from ipython>=4.0->ipythonblocks) (0.7.5)\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: 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: nbformat in /usr/local/lib/python3.7/dist-packages (from notebook>=4.0->ipythonblocks) (5.7.0)\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: prometheus-client in /usr/local/lib/python3.7/dist-packages (from notebook>=4.0->ipythonblocks) (0.15.0)\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: nbconvert<6.0 in /usr/local/lib/python3.7/dist-packages (from notebook>=4.0->ipythonblocks) (5.6.1)\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: 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: 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: Send2Trash in /usr/local/lib/python3.7/dist-packages (from notebook>=4.0->ipythonblocks) (1.8.0)\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: tornado<7,>=4.1 in /usr/local/lib/python3.7/dist-packages (from notebook>=4.0->ipythonblocks) (6.0.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: defusedxml in /usr/local/lib/python3.7/dist-packages (from nbconvert<6.0->notebook>=4.0->ipythonblocks) (0.7.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: 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: 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: testpath in /usr/local/lib/python3.7/dist-packages (from nbconvert<6.0->notebook>=4.0->ipythonblocks) (0.6.0)\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: 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: 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: 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: 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: 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: 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: 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: 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: 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: 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: 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": 97,
      "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": 98,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "X1, X2, X3, X4, X5, X6 = expr('X1, X2, X3, X4, X5, X6')"
      ],
      "metadata": {
        "id": "wFVZz8GH6obr"
      },
      "execution_count": 99,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "A"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "qG3qLxIu6tEv",
        "outputId": "b1275f4d-3043-4c1e-ae91-3d78b18bcd36"
      },
      "execution_count": 46,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "{'a1': 'B', 'a2': 'C', 'a3': 'D'}"
            ]
          },
          "metadata": {},
          "execution_count": 46
        }
      ]
    },
    {
      "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": "385c19e5-8b42-4f3c-e5e9-6e93989884b9"
      },
      "execution_count": 100,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "{C: False, B: True, A: True, D: True}"
            ]
          },
          "metadata": {},
          "execution_count": 100
        }
      ]
    },
    {
      "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": 101,
      "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": 102,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "sentence_1\n"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "I0kOEK0R8UPV",
        "outputId": "3edb12a7-0d33-4a9f-fd64-d736e7cea34f"
      },
      "execution_count": 103,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "(A <=> B)"
            ]
          },
          "metadata": {},
          "execution_count": 103
        }
      ]
    },
    {
      "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": "b71161e0-0512-4828-d460-d5c9f7ee6c65"
      },
      "execution_count": 104,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "{C: True, B: True, A: False}"
            ]
          },
          "metadata": {},
          "execution_count": 104
        }
      ]
    },
    {
      "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": 52,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "WalkSAT_CNF(sent1)"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "Ed98N_5rqJsz",
        "outputId": "f03b24a9-19a5-40b9-b453-d3f60a5e43a2"
      },
      "execution_count": 105,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "{X2: True, X1: False, X3: True}"
            ]
          },
          "metadata": {},
          "execution_count": 105
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "sent2 = ((~X1 | X2) & (~X2 | ~X3 | X4) & (~X3 | ~X4 | X5) & (X1 | ~X4 | X5) & ~(X1 | X2 | X3))"
      ],
      "metadata": {
        "id": "Wpq9wlnIqKsN"
      },
      "execution_count": 54,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "sent2"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "uAHfLK2Pq9s_",
        "outputId": "a25b07ad-c6c2-413b-818e-7862e0008bf3"
      },
      "execution_count": 55,
      "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": 55
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "WalkSAT_CNF(sent2)"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "4N9teVJIq_Tk",
        "outputId": "46cf2ac1-a540-4a93-bb19-42a6f73546c4"
      },
      "execution_count": 56,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "{X4: False, X1: False, X5: True, X2: False, X3: False}"
            ]
          },
          "metadata": {},
          "execution_count": 56
        }
      ]
    },
    {
      "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": 57,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "WalkSAT_CNF(sent3)"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "f_h6Otrerjbp",
        "outputId": "40f203a4-84d8-4489-8cad-650574791bfb"
      },
      "execution_count": 58,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "{X2: True, X3: True, X1: False}"
            ]
          },
          "metadata": {},
          "execution_count": 58
        }
      ]
    },
    {
      "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": 59,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "sent4"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "K2xbSBHXr_UL",
        "outputId": "8424ae2e-6f5b-4aba-e805-aed652fddc59"
      },
      "execution_count": 60,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "((((((~X1 | X2) | X3) & ((~X1 | ~X2) | X3)) & ((~X1 | ~X2) | ~X3)) & (X2 | ~X3)) & (X3 | X4))"
            ]
          },
          "metadata": {},
          "execution_count": 60
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "WalkSAT_CNF(sent4)"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "yIzZRJJysF9W",
        "outputId": "43d43b5e-3127-42eb-f6c8-c8e576ab22dc"
      },
      "execution_count": 61,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "{X2: True, X4: False, X1: False, X3: True}"
            ]
          },
          "metadata": {},
          "execution_count": 61
        }
      ]
    },
    {
      "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": 62,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "sent5"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "AKJxGKq7snEF",
        "outputId": "114150e2-8159-40c4-b17c-ef86dffb8d87"
      },
      "execution_count": 63,
      "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": 63
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "WalkSAT_CNF(sent5)"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "ydn7ssdxso6N",
        "outputId": "10adc160-45b4-4aaf-b2f0-8e01e82cf581"
      },
      "execution_count": 64,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "{X4: False, X1: False, X6: False, X5: False, X2: False, X3: True}"
            ]
          },
          "metadata": {},
          "execution_count": 64
        }
      ]
    },
    {
      "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": 65,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "WalkSAT_CNF(sent6)"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "YoDErBbstENY",
        "outputId": "d69da07b-8485-4a94-9a39-69c7cf26269b"
      },
      "execution_count": 66,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "{X2: False, X1: False, X3: True}"
            ]
          },
          "metadata": {},
          "execution_count": 66
        }
      ]
    },
    {
      "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": 67,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "WalkSAT_CNF(sent7)"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "JLtYjibytavL",
        "outputId": "2813bccc-3637-45bd-e1fe-0ccb6a794efe"
      },
      "execution_count": 68,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "{X2: False, X4: True, X1: True, X3: False}"
            ]
          },
          "metadata": {},
          "execution_count": 68
        }
      ]
    },
    {
      "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": 69,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "WalkSAT_CNF(sent8)"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "WZ6lLZPhtzkh",
        "outputId": "a8130256-f86c-4425-e755-7a60029c55b2"
      },
      "execution_count": 70,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "{X4: False, X1: False, X5: False, X2: True, X3: True}"
            ]
          },
          "metadata": {},
          "execution_count": 70
        }
      ]
    },
    {
      "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": 71,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "WalkSAT_CNF(sent9)"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "hYi2z5PmuOTt",
        "outputId": "3ac636d0-d33e-4582-967c-e05eae482c6e"
      },
      "execution_count": 72,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "{X2: False, X1: True, X3: False}"
            ]
          },
          "metadata": {},
          "execution_count": 72
        }
      ]
    },
    {
      "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": 73,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "WalkSAT_CNF(sent10)"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "cZIDjP1vukvf",
        "outputId": "53b8bb3a-1ea0-402f-911c-c5d59f5abda0"
      },
      "execution_count": 74,
      "outputs": [
        {
          "output_type": "execute_result",
          "data": {
            "text/plain": [
              "{X2: False, X4: True, X1: False, X3: False}"
            ]
          },
          "metadata": {},
          "execution_count": 74
        }
      ]
    },
    {
      "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": "bc64b9dc-c8ff-47e9-a623-975226ebd3ef"
      },
      "execution_count": 106,
      "outputs": [
        {
          "output_type": "stream",
          "name": "stdout",
          "text": [
            "16.3 ms ± 233 µs per loop (mean ± std. dev. of 7 runs, 100 loops each)\n"
          ]
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [],
      "metadata": {
        "id": "bZebGek4vDAk"
      },
      "execution_count": 75,
      "outputs": []
    }
  ]
}