AI - Lab 06 - DPLL Algorithm.ipynb

{
  "nbformat": 4,
  "nbformat_minor": 0,
  "metadata": {
    "kernelspec": {
      "display_name": "Python 3",
      "language": "python",
      "name": "python3"
    },
    "language_info": {
      "codemirror_mode": {
        "name": "ipython",
        "version": 3
      },
      "file_extension": ".py",
      "mimetype": "text/x-python",
      "name": "python",
      "nbconvert_exporter": "python",
      "pygments_lexer": "ipython3",
      "version": "3.8.5"
    },
    "colab": {
      "name": "AI - Lab 06 - DPLL Algorithm.ipynb",
      "provenance": [],
      "include_colab_link": true
    }
  },
  "cells": [
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "view-in-github",
        "colab_type": "text"
      },
      "source": [
        "<a href=\"https://colab.research.google.com/github/svishakan/Artificial-Intelligence/blob/master/AI%20-%20Lab%2006%20-%20DPLL%20Algorithm.ipynb\" target=\"_parent\"><img src=\"https://colab.research.google.com/assets/colab-badge.svg\" alt=\"Open In Colab\"/></a>"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "gW_PTH1E8vPZ"
      },
      "source": [
        "# Artificial Intelligence — Lab — Exercise 06"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "wXG0GF-S8vPa"
      },
      "source": [
        "#### 6 October 2020"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "i2R8JDj88vPa"
      },
      "source": [
        "## Davis–Putnam–Logemann–Loveland (DPLL) algorithm"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "Ecg9ZYbs8vPb"
      },
      "source": [
        "Implement David-Putnam algorithm for checking the satisfiability of a sentence represented in propositional logic.\n",
        "<hr>"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "V4KS9KzZ8vPb"
      },
      "source": [
        "The Davis–Putnam–Logemann–Loveland (DPLL) algorithm is a complete, \n",
        "backtracking-based search algorithm for deciding the satisfiability of propositional logic formulae \n",
        "in conjunctive normal form, i.e. for solving the CNF-SAT problem.\n",
        "<hr>"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "uersSUsN8vPc"
      },
      "source": [
        "Theory is adapted from Artificial Intelligence: A Modern Approach by Peter Norvig & Stuart J. Russell"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "_KF9qAV18vPc"
      },
      "source": [
        "<hr>\n",
        "This algorithm is very similar to Backtracking-Search. It recursively enumerates possible models in a depth-first fashion with the following improvements over algorithms like Truth Table Entailment.\n",
        "\n",
        "1. Early termination:\n",
        "In certain cases, the algorithm can detect the truth value of a statement using just a partially completed model. For example, $(P\\lor Q)\\land(P\\lor R)$ is true if P is true, regardless of other variables. This reduces the search space significantly.\n",
        "<br><br>\n",
        "2. Pure symbol heuristic:\n",
        "A symbol that has the same sign (positive or negative) in all clauses is called a pure symbol. It isn't difficult to see that any satisfiable model will have the pure symbols assigned such that its parent clause becomes true. For example, $(P\\lor\\neg Q)\\land(\\neg Q\\lor\\neg R)\\land(R\\lor P)$ has P and Q as pure symbols and for the sentence to be true, P has to be true and Q has to be false. The pure symbol heuristic thus simplifies the problem a bit.\n",
        "<br><br>\n",
        "3. Unit clause heuristic:\n",
        "In the context of DPLL, clauses with just one literal and clauses with all but one false literals are called unit clauses. If a clause is a unit clause, it can only be satisfied by assigning the necessary value to make the last literal true. We have no other choice.\n",
        "<br><br>\n",
        "Assigning one unit clause can create another unit clause. For example, when P is false, $(P\\lor Q)$ becomes a unit clause, causing true to be assigned to Q. A series of forced assignments derived from previous unit clauses is called unit propagation. In this way, this heuristic simplifies the problem further.\n",
        "<hr>\n"
      ]
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "QmMSFa7h8vPd"
      },
      "source": [
        "class DPLL:\n",
        "    true_literals = set()\n",
        "    false_literals = set()\n",
        "    pure_literals = set()\n",
        "    cnf = []\n",
        "    literals = []\n",
        "    unit_props, num_pure, branches = 0, 0, 0\n",
        "    \n",
        "    def __init__(self, formula):\n",
        "        \"\"\"To initialize the DPLL Solver with the required CNF Form & Literals. \"\"\"\n",
        "        \n",
        "        self.cnf = formula.split(\", \")\n",
        "        self.literals = self.find_literals(self.cnf)\n",
        "        self.pure_literals = set()\n",
        "\n",
        "        print(\"Initial Formula:\\t\\t\\t\", self)\n",
        "        \n",
        "        \n",
        "    def __str__(self):\n",
        "        \"\"\"To convert the Pythonic-list used for CNF notation into a readable formula in CNF. \"\"\"\n",
        "        \n",
        "        cnf_str = \"\"\n",
        "        \n",
        "        for clause in self.cnf:  #represent each claue in CNF\n",
        "            if len(clause) > 0:\n",
        "                cnf_str += '(' + clause.replace(' ', ' ∨ ') + ') ∧ '\n",
        "    \n",
        "        if cnf_str == \"\":       #formula is empty\n",
        "            cnf_str = \"()\"\n",
        "            \n",
        "        if cnf_str[-2] == \"∧\":  #removing the final '∧' added which is un-wanted.\n",
        "            cnf_str = cnf_str[:-2:] \n",
        "    \n",
        "        return cnf_str\n",
        "\n",
        "    \n",
        "    def find_literals(self, formula):\n",
        "        \"\"\"Finds the literals existing in a given formula. \"\"\"\n",
        "\n",
        "        literals = [literal for literal in list(set(''.join(formula))) if literal.isalpha()]\n",
        "\n",
        "        return literals\n",
        "    \n",
        "    def remove_pure_literals(self):\n",
        "        \"\"\"Finds the pure literals in the given formula. \"\"\"\n",
        "\n",
        "        cnf = list(set(self.cnf))\n",
        "        unit_clauses = [clause for clause in cnf if len(clause) < 3]\n",
        "        unit_clauses = list(set(unit_clauses))\n",
        "        current_literals = self.find_literals(cnf)  #Find literals in the current formula\n",
        "\n",
        "        for literal in current_literals:  #Check for literals like X\n",
        "            is_pure_literal = False\n",
        "\n",
        "            for i in range(len(cnf)):\n",
        "                if '¬' + literal not in cnf[i]: \n",
        "                    is_pure_literal = True\n",
        "                else:  #If ¬X exists in other clauses\n",
        "                    is_pure_literal = False\n",
        "                    break\n",
        "            \n",
        "            if is_pure_literal:  #If X is a pure literal\n",
        "                self.num_pure += 1\n",
        "                self.pure_literals.add(literal)\n",
        "                self.true_literals.add(literal)  #Add X to True literals\n",
        "                i = 0\n",
        "\n",
        "                while True:  #Remove clauses containing X\n",
        "                    if i >= len(cnf):\n",
        "                        break\n",
        "\n",
        "                    if literal in cnf[i]:\n",
        "                        cnf.remove(cnf[i])\n",
        "                    \n",
        "                        i -= 1\n",
        "                    i += 1\n",
        "\n",
        "        for literal in current_literals:  #Check for literals like ¬X \n",
        "            literal = '¬' + literal  #Search for literals of the type ¬X\n",
        "            is_pure_literal = False\n",
        "\n",
        "            for i in range(len(cnf)):\n",
        "                if literal in cnf[i]: \n",
        "                    is_pure_literal = True\n",
        "                else:  #If X exists in other clauses\n",
        "                    is_pure_literal = False\n",
        "                    break\n",
        "            \n",
        "            if is_pure_literal:  #If ¬X is a pure literal\n",
        "                self.num_pure += 1\n",
        "                self.pure_literals.add(literal)\n",
        "                self.false_literals.add(literal[-1])  #Add X to False literals\n",
        "                i = 0\n",
        "\n",
        "                while True:  #Remove clauses containing ¬X\n",
        "                    if i >= len(cnf):\n",
        "                        break\n",
        "\n",
        "                    if literal in cnf[i]:\n",
        "                        cnf.remove(cnf[i])\n",
        "                    \n",
        "                        i -= 1\n",
        "                    i += 1\n",
        "        \n",
        "        self.cnf = cnf\n",
        "\n",
        "        print(\"Pure Literals:\\t\\t\\t\\t\", list(self.pure_literals))\n",
        "        print(\"CNF after removing Pure Literals:\\t\", self)\n",
        "\n",
        "        return cnf\n",
        "\n",
        "    \n",
        "    def unit_clause_propagation(self):\n",
        "        \"\"\"Peform the unit-clause propagation on the given formula. \"\"\"\n",
        "        \n",
        "        new_true_literals  =  []\n",
        "        new_false_literals =  []\n",
        "        \n",
        "        print(\"\\nCurrent Formula:\\t\\t\\t\", self)\n",
        "        \n",
        "        cnf = list(set(self.cnf))\n",
        "        unit_clauses = [clause for clause in cnf if len(clause) < 3]   #clause of len < 3 is a unit clause\n",
        "        unit_clauses = list(set(unit_clauses))\n",
        "        \n",
        "        if unit_clauses:  #Assign truth values to unit clauses for satisfying the given formula\n",
        "            for unit in unit_clauses:\n",
        "                self.unit_props += 1\n",
        "                \n",
        "                if '¬' in unit:  #False unit clause\n",
        "                    self.false_literals.add(unit[-1])\n",
        "                    new_false_literals.append(unit[-1])\n",
        "                    i = 0\n",
        "                    \n",
        "                    while True:\n",
        "                        if unit in cnf[i]:  #Remove the unit clause from the formula\n",
        "                            cnf.remove(cnf[i])\n",
        "                            i -= 1\n",
        "                        \n",
        "                        elif unit[-1] in cnf[i]:  #If a ¬(unit clause) exists in the formula\n",
        "                            cnf[i] = cnf[i].replace(unit[-1], '').strip()\n",
        "                    \n",
        "                        i += 1\n",
        "                    \n",
        "                        if i >= len(cnf):\n",
        "                            break\n",
        "        \n",
        "                else:  #True unit clause\n",
        "                    self.true_literals.add(unit)\n",
        "                    new_true_literals.append(unit)\n",
        "                    i = 0\n",
        "                \n",
        "                    while True:\n",
        "                        if '¬' + unit in cnf[i]:  #If a ¬(unit clause) exists in the formula\n",
        "                            cnf[i] = cnf[i].replace('¬' + unit, '').strip()\n",
        "                        \n",
        "                            if '  ' in cnf[i]:  #Empty clause\n",
        "                                cnf[i] = cnf[i].replace('  ', ' ')\n",
        "                        \n",
        "                        elif unit in cnf[i]:  #Remove the unit clause from the formula\n",
        "                            cnf.remove(cnf[i])\n",
        "                            i -= 1\n",
        "                            \n",
        "                        i += 1\n",
        "                        \n",
        "                        if i >= len(cnf):\n",
        "                            break\n",
        "        \n",
        "        self.cnf = cnf\n",
        "\n",
        "        print(\"Current Unit Clauses:\\t\\t\\t\", unit_clauses)\n",
        "        print(\"CNF after doing Unit Propagation:\\t\", self)\n",
        "\n",
        "        return cnf, new_true_literals, new_false_literals\n",
        "    \n",
        "    \n",
        "    def DPLL_Algorithm(self):\n",
        "        \"\"\"Perform the David-Putnam-Logemann-Loveland algorithm on the given formula. \"\"\"\n",
        "        \n",
        "        self.true_literals = set(self.true_literals)\n",
        "        self.false_literals = set(self.false_literals)\n",
        "        \n",
        "        self.branches += 1  #Since this is a new branch\n",
        "\n",
        "        self.cnf, new_true_literals, new_false_literals = self.unit_clause_propagation()  #Do unit-clause propagation\n",
        "\n",
        "        if sum(len(clause) == 0 for clause in self.cnf):  #If there are empty parantheses, indicating contradiction\n",
        "            \n",
        "            for literal in new_true_literals:   #clear every newly set true literal\n",
        "                self.true_literals.remove(literal)\n",
        "            \n",
        "            for literal in new_false_literals:  #clear every newly set false literal\n",
        "                self.false_literals.remove(literal)\n",
        "                \n",
        "            print(\"\\nNull clause found. Backtracking...\")\n",
        "            \n",
        "            return False  #Backtrack, since we cannot simplify anymore, and it is unsatisfiable in the current branch\n",
        "\n",
        "\n",
        "        self.cnf = self.remove_pure_literals()  #Removing pure literal containing clauses from the formula\n",
        "\n",
        "        cnf = self.cnf\n",
        "\n",
        "        if len(self.cnf) == 0:  #No more clauses to satisfy\n",
        "            return True\n",
        "\n",
        "        \n",
        "        self.literals = self.find_literals(self.cnf)\n",
        "        #form the literals again from the updated formula\n",
        "        \n",
        "        first_literal = self.literals[0]  #choose the first literal to set as True/False to find satisfying assignments\n",
        "        \n",
        "        self.cnf = cnf + [first_literal]  #Try with first literal set to True\n",
        "        print(\"\\nTrying with {0} as True...\".format(first_literal))\n",
        "        \n",
        "        if self.DPLL_Algorithm():  #recursively work on the new formula\n",
        "            return True\n",
        "        \n",
        "        self.cnf = cnf + ['¬' + first_literal]  #Try with first literal set to False (i.e ¬(first literal) is True)\n",
        "        print(\"\\nTrying with ¬{0} as True...\".format(first_literal))\n",
        "        \n",
        "        if self.DPLL_Algorithm():  #recursively work on the new formula\n",
        "            return True\n",
        "\n",
        "        \n",
        "        else:  #no satisfying assignments were found to the literals of the formula\n",
        "            self.cnf = cnf\n",
        "            \n",
        "            for literal in new_true_literals:   #remove all the assignments\n",
        "                self.true_literals.remove(literal)\n",
        "            \n",
        "            for literal in new_false_literals:  #remove all the assignments\n",
        "                self.false_literals.remove(literal)\n",
        "            \n",
        "            return False  #the formula is unsatisfiable.\n",
        "        \n",
        "    \n",
        "    def print_result(self, satisfiability):\n",
        "        \"\"\"Print the result of the DPLL Algorithm on the formula along with its literals' assignments and statistics. \"\"\"\n",
        "        \n",
        "        if satisfiability == True:\n",
        "            print(\"\\nThe given CNF statement is satisfiable.\")\n",
        "            print(\"\\nSolution: \")\n",
        "            \n",
        "            for literal in self.true_literals:\n",
        "                print(\"\\t\"+literal, \"= True\")\n",
        "                \n",
        "            for literal in self.false_literals:\n",
        "                print(\"\\t\"+literal, \"= False\")\n",
        "            \n",
        "        else:\n",
        "            print(\"\\nThe given CNF statement was unsatisfiable.\")\n",
        "            \n",
        "        print(\"\\nNo. of branches:\\t\\t\", self.branches)\n",
        "        print(\"\\nNo. of unit propagations:\\t\", self.unit_props)\n",
        "        print(\"\\nNo. of pure literals removed:\\t\", self.num_pure)\n"
      ],
      "execution_count": 11,
      "outputs": []
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "dzn8CYTN8vPf"
      },
      "source": [
        "<hr>\n",
        "Running DPLL Algorithm for $(X \\lor Y \\lor Z)\\land(X \\lor\\neg Y \\lor Z)\\land(\\neg X \\lor Y \\lor\\neg Z)\\land(\\neg Z)$\n",
        "<hr>"
      ]
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "vR2P0M_q8vPg",
        "outputId": "9ebd9a6a-213a-4ae6-df0f-b7706221464e",
        "colab": {
          "base_uri": "https://localhost:8080/",
          "height": 336
        }
      },
      "source": [
        "dpll_solver = DPLL(\"X Y Z, X ¬Y Z, ¬X Y ¬Z, ¬Z\")\n",
        "satisfiability = dpll_solver.DPLL_Algorithm()\n",
        "dpll_solver.print_result(satisfiability)"
      ],
      "execution_count": 16,
      "outputs": [
        {
          "output_type": "stream",
          "text": [
            "Initial Formula:\t\t\t (X ∨ Y ∨ Z) ∧ (X ∨ ¬Y ∨ Z) ∧ (¬X ∨ Y ∨ ¬Z) ∧ (¬Z) \n",
            "\n",
            "Current Formula:\t\t\t (X ∨ Y ∨ Z) ∧ (X ∨ ¬Y ∨ Z) ∧ (¬X ∨ Y ∨ ¬Z) ∧ (¬Z) \n",
            "Current Unit Clauses:\t\t\t ['¬Z']\n",
            "CNF after doing Unit Propagation:\t (X ∨ ¬Y) ∧ (X ∨ Y) \n",
            "Pure Literals:\t\t\t\t ['X']\n",
            "CNF after removing Pure Literals:\t ()\n",
            "\n",
            "The given CNF statement is satisfiable.\n",
            "\n",
            "Solution: \n",
            "\tX = True\n",
            "\tZ = False\n",
            "\n",
            "No. of branches:\t\t 1\n",
            "\n",
            "No. of unit propagations:\t 1\n",
            "\n",
            "No. of pure literals removed:\t 1\n"
          ],
          "name": "stdout"
        }
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "5ehaWPBN8vPj"
      },
      "source": [
        "<hr>\n",
        "Running DPLL Algorithm for $(\\neg P \\lor Q)\\land(\\neg Q \\lor\\neg R)\\land(\\neg S \\lor P)\\land(P \\lor Q \\lor\\neg R)$\n",
        "<hr>"
      ]
    },
    {
      "cell_type": "code",
      "metadata": {
        "scrolled": true,
        "id": "hfl-IRas8vPj",
        "outputId": "8c7e3545-7edf-4a27-be54-fbf94ac577ea",
        "colab": {
          "base_uri": "https://localhost:8080/",
          "height": 1000
        }
      },
      "source": [
        "dpll_solver = DPLL(\"¬P Q, ¬Q ¬R, R ¬S, ¬S P, P Q ¬R\")\n",
        "satisfiability = dpll_solver.DPLL_Algorithm()\n",
        "dpll_solver.print_result(satisfiability)"
      ],
      "execution_count": 13,
      "outputs": [
        {
          "output_type": "stream",
          "text": [
            "Initial Formula:\t\t\t (¬P ∨ Q) ∧ (¬Q ∨ ¬R) ∧ (R ∨ ¬S) ∧ (¬S ∨ P) ∧ (P ∨ Q ∨ ¬R) \n",
            "\n",
            "Current Formula:\t\t\t (¬P ∨ Q) ∧ (¬Q ∨ ¬R) ∧ (R ∨ ¬S) ∧ (¬S ∨ P) ∧ (P ∨ Q ∨ ¬R) \n",
            "Current Unit Clauses:\t\t\t []\n",
            "CNF after doing Unit Propagation:\t (¬Q ∨ ¬R) ∧ (R ∨ ¬S) ∧ (¬S ∨ P) ∧ (¬P ∨ Q) ∧ (P ∨ Q ∨ ¬R) \n",
            "Pure Literals:\t\t\t\t []\n",
            "CNF after removing Pure Literals:\t (¬Q ∨ ¬R) ∧ (R ∨ ¬S) ∧ (¬P ∨ Q) ∧ (¬S ∨ P) ∧ (P ∨ Q ∨ ¬R) \n",
            "\n",
            "Trying with S as True...\n",
            "\n",
            "Current Formula:\t\t\t (¬Q ∨ ¬R) ∧ (R ∨ ¬S) ∧ (¬P ∨ Q) ∧ (¬S ∨ P) ∧ (P ∨ Q ∨ ¬R) ∧ (S) \n",
            "Current Unit Clauses:\t\t\t ['S']\n",
            "CNF after doing Unit Propagation:\t (¬Q ∨ ¬R) ∧ (R) ∧ (P) ∧ (¬P ∨ Q) ∧ (P ∨ Q ∨ ¬R) \n",
            "Pure Literals:\t\t\t\t []\n",
            "CNF after removing Pure Literals:\t (¬Q ∨ ¬R) ∧ (P) ∧ (¬P ∨ Q) ∧ (R) ∧ (P ∨ Q ∨ ¬R) \n",
            "\n",
            "Trying with P as True...\n",
            "\n",
            "Current Formula:\t\t\t (¬Q ∨ ¬R) ∧ (P) ∧ (¬P ∨ Q) ∧ (R) ∧ (P ∨ Q ∨ ¬R) ∧ (P) \n",
            "Current Unit Clauses:\t\t\t ['R', 'P']\n",
            "CNF after doing Unit Propagation:\t (¬Q) ∧ (Q) \n",
            "Pure Literals:\t\t\t\t []\n",
            "CNF after removing Pure Literals:\t (Q) ∧ (¬Q) \n",
            "\n",
            "Trying with Q as True...\n",
            "\n",
            "Current Formula:\t\t\t (Q) ∧ (¬Q) ∧ (Q) \n",
            "Current Unit Clauses:\t\t\t ['Q', '¬Q']\n",
            "CNF after doing Unit Propagation:\t ()\n",
            "\n",
            "Null clause found. Backtracking...\n",
            "\n",
            "Trying with ¬Q as True...\n",
            "\n",
            "Current Formula:\t\t\t (Q) ∧ (¬Q) ∧ (¬Q) \n",
            "Current Unit Clauses:\t\t\t ['Q', '¬Q']\n",
            "CNF after doing Unit Propagation:\t ()\n",
            "\n",
            "Null clause found. Backtracking...\n",
            "\n",
            "Trying with ¬P as True...\n",
            "\n",
            "Current Formula:\t\t\t (¬Q ∨ ¬R) ∧ (P) ∧ (¬P ∨ Q) ∧ (R) ∧ (P ∨ Q ∨ ¬R) ∧ (¬P) \n",
            "Current Unit Clauses:\t\t\t ['R', 'P', '¬P']\n",
            "CNF after doing Unit Propagation:\t (¬Q) ∧ (Q) \n",
            "\n",
            "Null clause found. Backtracking...\n",
            "\n",
            "Trying with ¬S as True...\n",
            "\n",
            "Current Formula:\t\t\t (¬Q ∨ ¬R) ∧ (R ∨ ¬S) ∧ (¬P ∨ Q) ∧ (¬S ∨ P) ∧ (P ∨ Q ∨ ¬R) ∧ (¬S) \n",
            "Current Unit Clauses:\t\t\t ['¬S']\n",
            "CNF after doing Unit Propagation:\t (¬Q ∨ ¬R) ∧ (¬P ∨ Q) ∧ (P ∨ Q ∨ ¬R) \n",
            "Pure Literals:\t\t\t\t []\n",
            "CNF after removing Pure Literals:\t (¬Q ∨ ¬R) ∧ (P ∨ Q ∨ ¬R) ∧ (¬P ∨ Q) \n",
            "\n",
            "Trying with P as True...\n",
            "\n",
            "Current Formula:\t\t\t (¬Q ∨ ¬R) ∧ (P ∨ Q ∨ ¬R) ∧ (¬P ∨ Q) ∧ (P) \n",
            "Current Unit Clauses:\t\t\t ['P']\n",
            "CNF after doing Unit Propagation:\t (¬Q ∨ ¬R) ∧ (Q) \n",
            "Pure Literals:\t\t\t\t []\n",
            "CNF after removing Pure Literals:\t (¬Q ∨ ¬R) ∧ (Q) \n",
            "\n",
            "Trying with R as True...\n",
            "\n",
            "Current Formula:\t\t\t (¬Q ∨ ¬R) ∧ (Q) ∧ (R) \n",
            "Current Unit Clauses:\t\t\t ['R', 'Q']\n",
            "CNF after doing Unit Propagation:\t ()\n",
            "\n",
            "Null clause found. Backtracking...\n",
            "\n",
            "Trying with ¬R as True...\n",
            "\n",
            "Current Formula:\t\t\t (¬Q ∨ ¬R) ∧ (Q) ∧ (¬R) \n",
            "Current Unit Clauses:\t\t\t ['¬R', 'Q']\n",
            "CNF after doing Unit Propagation:\t ()\n",
            "Pure Literals:\t\t\t\t []\n",
            "CNF after removing Pure Literals:\t ()\n",
            "\n",
            "The given CNF statement is satisfiable.\n",
            "\n",
            "Solution: \n",
            "\tP = True\n",
            "\tQ = True\n",
            "\tS = False\n",
            "\tR = False\n",
            "\n",
            "No. of branches:\t\t 10\n",
            "\n",
            "No. of unit propagations:\t 16\n",
            "\n",
            "No. of pure literals removed:\t 0\n"
          ],
          "name": "stdout"
        }
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "yDzb9uoS8vPl"
      },
      "source": [
        "<hr>\n",
        "Custom formula : Separate clauses in formula by commas \", \" and literals inside a clause with spaces. Use \"¬\" for negation of a literal.\n",
        "<hr>"
      ]
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "nnBoz4bg8vPm",
        "outputId": "8f81b86c-ee38-4d89-8dc4-b65c76c1bba0",
        "colab": {
          "base_uri": "https://localhost:8080/",
          "height": 286
        }
      },
      "source": [
        "dpll_solver = DPLL(input(\"Enter a formula in CNF: \"))\n",
        "satisfiability = dpll_solver.DPLL_Algorithm()\n",
        "dpll_solver.print_result(satisfiability)"
      ],
      "execution_count": 14,
      "outputs": [
        {
          "output_type": "stream",
          "text": [
            "Enter a formula in CNF: P, ¬P\n",
            "Initial Formula:\t\t\t (P) ∧ (¬P) \n",
            "\n",
            "Current Formula:\t\t\t (P) ∧ (¬P) \n",
            "Current Unit Clauses:\t\t\t ['P', '¬P']\n",
            "CNF after doing Unit Propagation:\t ()\n",
            "\n",
            "Null clause found. Backtracking...\n",
            "\n",
            "The given CNF statement was unsatisfiable.\n",
            "\n",
            "No. of branches:\t\t 1\n",
            "\n",
            "No. of unit propagations:\t 2\n",
            "\n",
            "No. of pure literals removed:\t 0\n"
          ],
          "name": "stdout"
        }
      ]
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "obibUeIaYhml",
        "outputId": "fbcac55e-9096-498e-c5d1-ff447a17e401",
        "colab": {
          "base_uri": "https://localhost:8080/",
          "height": 470
        }
      },
      "source": [
        "dpll_solver = DPLL(\"X Y, Y ¬X, ¬X ¬Y\")\n",
        "satisfiability = dpll_solver.DPLL_Algorithm()\n",
        "dpll_solver.print_result(satisfiability)"
      ],
      "execution_count": 15,
      "outputs": [
        {
          "output_type": "stream",
          "text": [
            "Initial Formula:\t\t\t (X ∨ Y) ∧ (Y ∨ ¬X) ∧ (¬X ∨ ¬Y) \n",
            "\n",
            "Current Formula:\t\t\t (X ∨ Y) ∧ (Y ∨ ¬X) ∧ (¬X ∨ ¬Y) \n",
            "Current Unit Clauses:\t\t\t []\n",
            "CNF after doing Unit Propagation:\t (Y ∨ ¬X) ∧ (¬X ∨ ¬Y) ∧ (X ∨ Y) \n",
            "Pure Literals:\t\t\t\t []\n",
            "CNF after removing Pure Literals:\t (Y ∨ ¬X) ∧ (¬X ∨ ¬Y) ∧ (X ∨ Y) \n",
            "\n",
            "Trying with Y as True...\n",
            "\n",
            "Current Formula:\t\t\t (Y ∨ ¬X) ∧ (¬X ∨ ¬Y) ∧ (X ∨ Y) ∧ (Y) \n",
            "Current Unit Clauses:\t\t\t ['Y']\n",
            "CNF after doing Unit Propagation:\t (¬X) \n",
            "Pure Literals:\t\t\t\t ['¬X']\n",
            "CNF after removing Pure Literals:\t ()\n",
            "\n",
            "The given CNF statement is satisfiable.\n",
            "\n",
            "Solution: \n",
            "\tY = True\n",
            "\tX = False\n",
            "\n",
            "No. of branches:\t\t 2\n",
            "\n",
            "No. of unit propagations:\t 1\n",
            "\n",
            "No. of pure literals removed:\t 1\n"
          ],
          "name": "stdout"
        }
      ]
    }
  ]
}