A2: The DPLL Algorithm.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "markdown",
     "checksum": "69f9950e2c060ad5c3cc41d2c78fa636",
     "grade": false,
     "grade_id": "cell-36d7173cbd11c12a",
     "locked": true,
     "schema_version": 3,
     "solution": false,
     "task": false
    }
   },
   "source": [
    "<h1>CS152 Assignment 2: The DPLL Algorithm</h1>"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "In this assignment, you are required to implement the DPLL algorithm in python as described in Figure 7.17 in Russell & Norvig, and demonstrate it on a given KB.\n",
    "\n",
    "## Assignment Overview\n",
    "This assignment consists of several parts that should be completed in python code. You may use a\n",
    "python notebook with markdown cells for documentation, or a python script with substantial commenting to explain your code.\n",
    "\n",
    "1. Implement a python class Literal, which will be used to represent a logical literal. This class\n",
    "should contain a name attribute, which is a string containing the name of the literal. In addition, since clauses in DPLL may include negated literals, the class should also have a sign\n",
    "attribute, which is True if the literal is positive and False if the literal is negative. The class\n",
    "should also overload the `__neg__(self,other)` method to allow negative literals to be defined in clauses. As an example, the class should allow us to define literals like:\n",
    "\n",
    "    ```\n",
    "    - A = Literal(A)\n",
    "    - B = Literal(B)\n",
    "    - C = Literal(C)\n",
    "    - D = Literal(D)\n",
    "    ```\n",
    "\n",
    "   which will then allow us to define a KB in CNF comprising clauses by a list of sets. For example, if we wish to represent the knowledge base given by the CNF\n",
    "    \n",
    "    $$(A ∨ B) ∧ (A ∨ ¬C) ∧ (¬A ∨ B ∨ D),$$\n",
    "\n",
    "   we would write the python code\n",
    "   \n",
    "   ```\n",
    "   KB = [{A,B},{A,-C},{-A,B,D}]\n",
    "   ```\n",
    "   \n",
    "   Each set indicates a disjunction of the literals contained within it, with the negative sign indicating a negated literal.\n",
    "   \n",
    "   \n",
    "2. Implement a simplified version of the DPLL algorithm as in Figure 7.17, excluding the pure symbol and unit clause heuristics. This essentially reduces to choosing an arbitrary unassigned literal and trying to assign both true and false values to it and performing recursive evaluation of DPLL. You should have a function that is callable using the signature\n",
    "    \n",
    "    ```\n",
    "   (satisfiable, model) = DPLLSatisfiable(KB)\n",
    "   ```\n",
    "   \n",
    "   where KB is the knowledge base as above. This contains an additional output to the specification in Russell & Norvig. The outputs are satisfiable - a boolean value indicating whether or not the KB is satisfiable, and model - a python dictionary that has a Literal as the key and the value being one of the strings ‘true’, ‘false’ or ‘free’, depending on whether the literal must be true or false or can be freely chosen to ensure satisfiability. Remember that this function only has to return one model that works (even though there may be several). An example output for the KB above would be\n",
    "   \n",
    "   ```\n",
    "   model = {A: true, B: true, C: false, D: free}\n",
    "   ```\n",
    "   \n",
    "   Note that in this case, the literal A could also be free, but depending on the DPLL trace, A may be assigned in a model. The free variables will in practice be those symbols left over after DPLL has run to completion.\n",
    "   \n",
    "3. Test your code on the KB given in Exercise 7.20 of Russell & Norvig. Convert the KB into CNF and then run DPLL to determine a model for the KB and print it out.\n",
    "\n",
    "### Extensions\n",
    "1. Instead of choosing a symbol to assign arbitrarily, choose the one that is yet to be assigned\n",
    "and occurs in the most number of clauses at each point in the algorithm (known as the degree\n",
    "heuristic)\n",
    "\n",
    "2. Implement the pure symbol and unit clause heuristics, which are the primary innovations of\n",
    "DPLL over a simple recursive depth-first enumeration over true-false values. Extra kudos\n",
    "will be given for choosing the pure symbol that occurs the most over all clauses each time\n",
    "rather than choosing one arbitrarily.\n",
    "\n",
    "### Hints\n",
    "1. You can assume that a literal can occur at most once in every clause, either non-negated or\n",
    "negated. Two literals of the same sign in the one clause would cancel out and reduce to a\n",
    "single literal $(A ∨ A = A)$, and two literals of opposing signs will make the clause trivially\n",
    "true i.e. $(A ∨ ¬A = true)$.\n",
    "\n",
    "2. A clause is true as soon as any of its literals are true, and a clause with any literals false can\n",
    "be replaced by a clause with those literals removed. The only way to falsify a clause is if all\n",
    "literals (taking signs into account) are false.\n",
    "\n",
    "3. You may wish to put literals into a set regardless of their sign and not treat two literals with\n",
    "the same name, but different signs, as distinct. In this case, you can overload the equality\n",
    "operator `__eq__(self,other)` in order to specify that two literals are equal regardless of their\n",
    "sign (i.e. based only on their names). An alternative would be to use two sets for each clause,\n",
    "one storing the positive literals and one storing the negative ones.\n",
    "\n",
    "4. You may find it useful to define literals ‘true’ and ‘false’, and use these to indicate whether\n",
    "a clause is true in a given model or has been falsified. Additionally, at the execution point where all of the clauses are true, you could save the model using a global variable, that you\n",
    "can read once the DPLL recursion has terminated."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "---"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "markdown",
     "checksum": "7947006e03ad4d3e0b5469c4ddf997f0",
     "grade": false,
     "grade_id": "cell-8ec27aa9925ffc86",
     "locked": true,
     "schema_version": 3,
     "solution": false,
     "task": false
    }
   },
   "source": [
    "<h1>Question 1</h1>\n",
    "\n",
    "Define your <code>Literal</code> class below.  Ensure that you define a <code>name</code> and <code>sign</code> attribute as required in the assignment description.  In addition, include any other attributes and member functions as needed. You will need to overload <code>__neg__()</code> to correctly handle negated literals.  You may need to overload <code>__eq__()</code> and <code>__hash__()</code> also."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {
    "deletable": false,
    "nbgrader": {
     "cell_type": "code",
     "checksum": "6f3dcb95b91cd3b0f526b89f339b3fe9",
     "grade": false,
     "grade_id": "cell-575ae3fbbe1ccbf6",
     "locked": false,
     "schema_version": 3,
     "solution": true,
     "task": false
    }
   },
   "outputs": [],
   "source": [
    "# Import any packages you need here\n",
    "from functools import reduce\n",
    "from copy import deepcopy\n",
    "from collections import Counter\n",
    "\n",
    "class Literal:\n",
    "    \n",
    "    def __init__(self,name):\n",
    "        \n",
    "        \"\"\"\n",
    "        Literal class to represent positive and negative literals.\n",
    "    \n",
    "        Inputs/Attributes:\n",
    "            - name: Name of the literal\n",
    "            - sign: Sign to indicate if literal is positive or negative.\n",
    "                    Set to True for positive literals and False for negative literals\n",
    "    \n",
    "        \"\"\"\n",
    "        \n",
    "        #If the Literal has a negation symbol, assign False to sign, else assign True\n",
    "        if name[0] in ('-', '!','￢', '~'): \n",
    "            self.name= name[1:]\n",
    "            self.sign= False\n",
    "        else:\n",
    "            self.name = name\n",
    "            self.sign = True\n",
    "        \n",
    "    def __neg__(self):\n",
    "        \n",
    "        #Overload negation to alter the sign of a Literal\n",
    "        \n",
    "        if self.sign:\n",
    "            return Literal('{}{}'.format('-',self.name))\n",
    "        else:\n",
    "            return Literal(self.name)\n",
    "        \n",
    "    def __eq__(self, other):\n",
    "        \n",
    "        #Overloading to ensure that two literals with opposite sign are equal (i.e. same name)\n",
    "        \n",
    "        return self.name == other.name\n",
    "    \n",
    "    \n",
    "    def __lt__(self, other):\n",
    "        \n",
    "        #Overload to allow alphabetical sorting based on names.\n",
    "        return self.name < other.name\n",
    "    \n",
    "\n",
    "    def __hash__(self):\n",
    "        return hash(self.name)\n",
    "    \n",
    "    def __str__(self):\n",
    "        return self.name if self.sign else '￢{}'.format(self.name)\n",
    "\n",
    "    def __repr__(self):\n",
    "        return self.name    \n",
    "    \n",
    "    def standardize(self):\n",
    "        return Literal(self.name)\n",
    "        "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "markdown",
     "checksum": "7e6af6a3602f2712265baf6d3ce930f4",
     "grade": false,
     "grade_id": "cell-5df02e9e3f9998b4",
     "locked": true,
     "schema_version": 3,
     "solution": false,
     "task": false
    }
   },
   "source": [
    "<h1>Question 2</h1>\n",
    "Implement DPLL by filling in the stubs below.  Note that the various heuristics are not required to be implemented for basic functionality, but a template has been provided for you to do so if you attempt the extension questions"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {
    "deletable": false,
    "nbgrader": {
     "cell_type": "code",
     "checksum": "4ddf2e140725e3b8a6048c92bac9580c",
     "grade": false,
     "grade_id": "cell-2846b43cfaf88026",
     "locked": false,
     "schema_version": 3,
     "solution": true,
     "task": false
    }
   },
   "outputs": [],
   "source": [
    "# Define degree, pure symbol and unit clause heuristics here (optional).\n",
    "# Add in your functions under the templates below\n",
    "\n",
    "def true_clause(clause,model):\n",
    "    \n",
    "    \"\"\"\n",
    "    Checks if the inputted clause is True based on the literal value assignment\n",
    "    in the inputted model. Once one of the literals is found to be True, the clause\n",
    "    is determined to be True as well. This follows from the  fact that a clause is a \n",
    "    disjunction of literals.\n",
    "    \n",
    "    Inputs:\n",
    "        - clause (set): A set of Literal objects\n",
    "        - model (dict): A dictionary specifying the Literal assignment (True or False)\n",
    "                        in the given model. The keys are Literal objects and the \n",
    "                        value of each key is either True or False.\n",
    "        \n",
    "    Output:\n",
    "        - bool: Returns True if the clause is True in the given model. Returns False otherwise.\n",
    "        - None: Returns None if the truth status of the clause cannot be determined from the model\n",
    "    \n",
    "    \"\"\"\n",
    "    \n",
    "    #Placeholder to track symbols with unknown truth values (unassigned symbols)\n",
    "    unknown= False\n",
    "    \n",
    "    #Check each Literal in the clause\n",
    "    for literal in clause:\n",
    "        \n",
    "        \n",
    "        #If the literal has not been assigned, set unknown to True to indicate that the\n",
    "        #truth value cannot be determined\n",
    "        if literal not in model:\n",
    "            if unknown is False:\n",
    "                unknown= True\n",
    "        \n",
    "        #If the literal is assigned in the model, and evaluates to True after assignment\n",
    "        elif literal in model and literal.sign == model[literal]:\n",
    "            \n",
    "            #Return True, indicating that the clause is True in the model\n",
    "            return True\n",
    "    \n",
    "    #If the truth value of a clause cannot be determined, return None\n",
    "    if unknown:\n",
    "        return None\n",
    "    #If all the symbols in the clause evaluate to False after assignment, return False\n",
    "    else:\n",
    "        return False\n",
    "\n",
    "def update(model, key, value):\n",
    "    \n",
    "    \"\"\"\n",
    "    Copy and update model by setting key to value. Return the copy with new update.\n",
    "    \n",
    "    Inputs:\n",
    "        - model (dict): Dictionary containing Literal assignments. The keys of the dictionary \n",
    "                        represent the Literals and the values of each represents their assignment \n",
    "                        in the model(either True or False)\n",
    "        - key (Literal): The Literal to be added to the model\n",
    "        - value (bool): True or False assignment to key in the given model\n",
    "        \n",
    "    Output:\n",
    "        - updated_model (dict): Model with added Literal and its assignment\n",
    "    \n",
    "    \n",
    "    \"\"\"\n",
    "    \n",
    "    updated_model = model.copy()\n",
    "    updated_model[key] = value\n",
    "\n",
    "    return updated_model\n",
    "\n",
    "def degree_heuristic(symbols,KB,model):\n",
    "    \n",
    "    \n",
    "    \"\"\"\n",
    "    Order symbols in terms of their frequency of occurrence in the KB and return the symbol that \n",
    "    occurs most frequently (and is currently unassigned) as well as the other symbols in the KB. \n",
    "    Symbols with same frequency of occurence are ordered alphabetically.\n",
    "    \n",
    "    Inputs:\n",
    "        - symbols: A set containing all propositional symbols the KB\n",
    "        - KB: Knowledge base in the form of a list of sets of Literal objects, where each set\n",
    "              represents a clause in CNF form. \n",
    "        - model(dict): The configuration of the world (assignment of literals). The keys of the \n",
    "                       dictionary represent the Literals and the values of each represents their assignment \n",
    "                       in the model (either True or False).\n",
    "                       \n",
    "    Outputs:\n",
    "        - symbol: An unassigned symbol with the highest frequency in the KB\n",
    "        - rest: A list containing all other symbols in the KB (after exclusion of symbol described above)\n",
    "    \n",
    "    \"\"\"\n",
    "    \n",
    "    \n",
    "    #Flatten knowledge base to get every single symbol in the KB\n",
    "    flat_KB = [symbol for clause in KB for symbol in clause]\n",
    "    \n",
    "    #Count the occurrence of each of the symbol (Note: a postive and negative literal of the same symbol\n",
    "    #are considered the same symbol). Here the output is a dictionary like structure with the symbol \n",
    "    #as the key and its frequency of occurrence as the corresponding value.\n",
    "    symb_freq= Counter(flat_KB)\n",
    "    \n",
    "    #Sort symbols first based on decreasing frequency of occurrence then alphabetically\n",
    "    freq_ord_symb = sorted(symb_freq, key=lambda x: (-symb_freq[x], -x))\n",
    "    \n",
    "    #Iterate through all the symbols after they have been ordered \n",
    "    for symbol in freq_ord_symb:\n",
    "        \n",
    "        #Return the most frequently occuring symbol that is currently not assigned in the model\n",
    "        if symbol not in model:\n",
    "            \n",
    "            #Get the rest of the symbols after excluding the most frequently occuring symbol\n",
    "            freq_ord_symb.remove(symbol)\n",
    "            \n",
    "            #Return the standardized symbol (get rid of negation if present) and the rest\n",
    "            #of the symbols\n",
    "            return symbol.standardize(), freq_ord_symb\n",
    "        \n",
    "def find_pure_symbol(symbols,KB,model,with_degree_heuristic= False):\n",
    "    \n",
    "    \"\"\"\n",
    "    \n",
    "    Checks for pure symbols (symbols that appear only as a positive literal or only\n",
    "    as a negative literal) in the KB clauses that are not already assigned in the model.\n",
    "    In the event that there are multiple pure symbols, a pure symbol is returned if it comes before\n",
    "    others alphabetically.\n",
    "    \n",
    "    Inputs:\n",
    "        - symbols: A set containing all propositional symbols the KB\n",
    "        - KB: Knowledge base in the form of a list of sets of Literal objects, where each set\n",
    "              represents a clause in CNF form. \n",
    "        - model(dict): The configuration of the world (assignment of literals). The keys of the \n",
    "                       dictionary represent the Literals and the values of each represents their assignment \n",
    "                       in the model (either True or False).\n",
    "    \n",
    "    Output:\n",
    "        - symbol, sign: Return a pure symbol and the sign the assignment that makes it True in \n",
    "                        all clauses. In the case of multiple pure symbols, ff with_degree_heuristic\n",
    "                        is True the most frequently occuring pure symbol in the KB\n",
    "                        is selected for assignment, else a symbol is selected alphabetically.\n",
    "                        \n",
    "        - None: Returns None if no pure symbol is found\n",
    "    \"\"\"\n",
    "    \n",
    "    #Replace all negative symbols with positive ones. This is needed to ensure the evaluation\n",
    "    #of symbols to determine pure symbols on lines 160-164 is fair\n",
    "    symbols = [symbol.standardize() if not symbol.sign else symbol for symbol in symbols] \n",
    "\n",
    "    \n",
    "    #List to store the pure symbols found \n",
    "    pure_symbols= []\n",
    "    \n",
    "    #Flatten knowledge base to get every single symbol in the KB\n",
    "    flat_KB = [symbol for clause in KB for symbol in clause]\n",
    "    \n",
    "    #For each symbol\n",
    "    for symbol in symbols:\n",
    "        \n",
    "        #If the symbol is unassigned in the model\n",
    "        if symbol not in model:\n",
    "            \n",
    "            #Create placeholders to track the valency of the symbol in all clauses\n",
    "            pos_literal, neg_literal= False, False\n",
    "            \n",
    "            #For each symbol/literal in the knowledge base\n",
    "            for literal in flat_KB:\n",
    "                \n",
    "                #Check the valency of each instance of the symbol under question \n",
    "                #and update placeholders accordingly\n",
    "                if symbol == literal:\n",
    "                    if (symbol.sign and literal.sign == True) and not pos_literal:\n",
    "                        pos_literal= True\n",
    "                    elif (-symbol.sign and literal.sign == False) and not neg_literal:\n",
    "                        neg_literal = True\n",
    "            \n",
    "            #If the symbol is a pure symbol, add it to the list alongside the value that will make it\n",
    "            #True in all clauses it is contained in\n",
    "            if pos_literal != neg_literal:\n",
    "                pure_symbols.append((symbol,pos_literal))\n",
    "    \n",
    "    #If there is at least one pure symbol\n",
    "    if pure_symbols:\n",
    "        \n",
    "        #EXTENSION OF PURE SYMBOL HEURISTIC AS REQUIRED FOR HEURISTIC 3\n",
    "        if with_degree_heuristic:\n",
    "            \n",
    "            #If there is just one pure symbol,return it and the assignment that makes it True in all clauses\n",
    "            if len(pure_symbols)>1:\n",
    "                \n",
    "                #Count the occurrence of each of the symbol (here a positive and negative literal \n",
    "                #of the same symbol are considered the same symbol). Note: The output is a \n",
    "                #dictionary like structure with the symbol  as the key and its frequency of \n",
    "                #occurrence as the corresponding value.\n",
    "                symb_freq= Counter(flat_KB)\n",
    "\n",
    "\n",
    "                #Sort symbols first based on decreasing frequency of occurrence then alphabetically\n",
    "                freq_ord_symb = sorted(symb_freq, key=lambda x: (-symb_freq[x], -x))\n",
    "\n",
    "\n",
    "                #Iterate through all the symbols after they have been ordered \n",
    "                for symbol in freq_ord_symb:\n",
    "\n",
    "                    #Return the most frequently occuring pure symbol that is \n",
    "                    #currently not assigned in the model\n",
    "                    if (symbol,symbol.sign) in pure_symbols:\n",
    "\n",
    "                        return symbol, symbol.sign\n",
    "                    \n",
    "            #If there is just one pure symbol,return it and the assignment that makes it True in all clauses\n",
    "            else:\n",
    "                return pure_symbols[0]\n",
    "                \n",
    "        \n",
    "        #STANDARD IMPLEMENTATION OF PURE SYMBOL HEURISTIC\n",
    "        else:\n",
    "        \n",
    "            #If there are multiple pure symbols\n",
    "            if len(pure_symbols) > 1:\n",
    "                \n",
    "\n",
    "                #Return the symbol that comes first alphabetically and the assignment that makes it \n",
    "                #True in all clauses\n",
    "                return sorted(pure_symbols,reverse=True)[0]\n",
    "\n",
    "            #If there is just one pure symbol,return it and the assignment that makes it True in all clauses\n",
    "            else:\n",
    "                return pure_symbols[0]\n",
    "     \n",
    "    #If no pure symbol is found, return None\n",
    "    else:\n",
    "        return None, None\n",
    "                      \n",
    "\n",
    "def find_unit_clause(KB,model):\n",
    "    \n",
    "    \"\"\"\n",
    "    \n",
    "    Returns a the unit clause from the remaining unproven clauses given model assignment\n",
    "    \n",
    "    Inputs:\n",
    "        - KB: Knowledge base in the form of a list of sets of Literal objects, where each set\n",
    "              represents a clause in CNF form. \n",
    "        - model(dict): The configuration of the world (assignment of literals). The keys of the \n",
    "                       dictionary represent the Literals and the values of each represents their assignment \n",
    "                       in the model (either True or False).\n",
    "    \n",
    "    Output:\n",
    "        - symbol, sign: Return a pure symbol and the sign the assignment that makes it True in \n",
    "                        the unit clause. In the case of multiple symbols, selected symbol\n",
    "                        for assignment based on alphabetical order\n",
    "                        \n",
    "        - None: Returns None if no unit clause is found\n",
    "    \"\"\"\n",
    "    \n",
    "    \n",
    "    #List to store each symbol that is contained in each unit clause\n",
    "    unit_clause_symbols= []\n",
    "    \n",
    "    #Iterating through all the clauses in the knowledge base\n",
    "    for clause in KB:\n",
    "        \n",
    "        #Get all the unassigned symbols in the clause\n",
    "        unassigned_symbols= [symbol for symbol in clause if symbol not in model]\n",
    "        \n",
    "        #If there is just one unassigned symbol (i.e. if the clause is a unit clause)\n",
    "        if len(unassigned_symbols) == 1:\n",
    "            \n",
    "            #Store the symbol and its assignement that makes the clause True\n",
    "            unassigned_symb= unassigned_symbols[0]\n",
    "            unit_clause_symbols.append((unassigned_symb,unassigned_symb.sign))\n",
    "         \n",
    "\n",
    "    #If there is at least one unit clause\n",
    "    if unit_clause_symbols:\n",
    "        \n",
    "        #If there are multiple unit clauses\n",
    "        if len(unit_clause_symbols) > 1:\n",
    "            \n",
    "            \n",
    "            #Return the symbol that comes first alphabetically & the assignment that makes the clause True\n",
    "            return sorted(unit_clause_symbols)[0]\n",
    "        \n",
    "        #If there is just one unit clause symbol,return it & the assignment that makes it True\n",
    "        else:\n",
    "            return unit_clause_symbols[0]\n",
    "     \n",
    "    #If no unit clause is found, return None\n",
    "    else:\n",
    "        return None, None\n",
    "        \n",
    "\n",
    "def DPLL_Satisfiable(KB, heuristic_level=0):\n",
    "    \n",
    "    ''' satisfiable, model = DPLLSatisfiable(KB)\n",
    "        Takes in a KB and returns whether the KB is satisfiable, and the model that makes it so\n",
    "        \n",
    "        KB: A knowledge base of clauses (CNF) consisting of a list of sets of literals.  A KB might look like\n",
    "            [{A,B},{-A,C,D}]\n",
    "        heuristic_level: An integer that will be passed in to specify which heuristics to implement \n",
    "            (only for the extension activities).\n",
    "        satisfiable: Returns True if the KB is satisfiable, or False otherwise\n",
    "        Model: A dictionary that assigns a truth value to each literal for the model that satisfies KB.\n",
    "            For example, a model might look like {A: True, B: False}\n",
    "    '''\n",
    "    \n",
    "    #A set containing all the propositional symbols in the KB\n",
    "    symbols= reduce(lambda c1, c2: c1.union(c2), KB, set())\n",
    "    \n",
    "    result= DPLL(KB,symbols,{},heuristic_level,[])\n",
    "    \n",
    "    #If the model is unsatisfiable retuen False,None,0\n",
    "    if result is False:\n",
    "        return False, None, 0\n",
    "    #If the model is satisfiable, return satisfiable, model, symbol_list\n",
    "    else:\n",
    "        return result\n",
    "\n",
    "def DPLL(KB,symbols, model,heuristic_level,symbol_list):\n",
    "    \n",
    "    \"\"\"\n",
    "    Implement Davis-Putnam-Logemann-Loveland algorithm to check satisfiability of\n",
    "    a knowledge base in propositional logic.\n",
    "    \n",
    "    \n",
    "    Algorithm adapted from Figure 7.17 of Artificial Intelligence- A modern approach.\n",
    "\n",
    "\n",
    "    Inputs:\n",
    "        - KB: Knowledge base in the form of a list of sets of Literal objects, where each set\n",
    "              represents a clause in CNF form.\n",
    "        - symbols: A set containing all propositional symbols the KB\n",
    "        - model(dict): The configuration of the world (assignment of literals) being tested to \n",
    "                       determine satisfiability of the KB. The keys of the dictionary represent the\n",
    "                       Literals and the values of each represents their assignment in the model\n",
    "                       (either True or False)\n",
    "                 \n",
    "    Outputs:\n",
    "        - satisfiable (bool): Returns True if the KB is satisfiable. Returns False otherwise\n",
    "        - model(dict): If the KB is satisfiable, returns a model (that was found) that \n",
    "                       satisfies the KB.\n",
    "    \n",
    "    \"\"\"\n",
    "    \n",
    "    #Create list to store the clauses that cannot be determined from the a given model\n",
    "    unknown_clauses= []\n",
    "    \n",
    "    #Initialize counter track the number of True clauses that result from a model's assignments\n",
    "    num_true_clauses= 0\n",
    "    \n",
    "    #For each clause in the KB\n",
    "    for clause in KB:\n",
    "        \n",
    "        #If the clause is False, return False\n",
    "        if true_clause(clause,model) is False:\n",
    "            return False\n",
    "        \n",
    "        #If the truth value of the clause cannot be determined, add to unknown_clauses\n",
    "        elif true_clause(clause,model) is None:\n",
    "            unknown_clauses.append(clause)\n",
    "        \n",
    "        #If the clause was proved True, update the counter\n",
    "        else:\n",
    "            num_true_clauses += 1\n",
    "    \n",
    "    #If all the clauses in the KB are True return satisfiable, model, symbol_list\n",
    "    if num_true_clauses == len(KB):\n",
    "        return True, model,symbol_list\n",
    "    \n",
    "    \n",
    "    if heuristic_level==1:\n",
    "        \n",
    "        #Apply the DEGREE HEURISTIC\n",
    "        current_symb, rest = degree_heuristic(symbols,unknown_clauses,model)\n",
    "        \n",
    "        #Add the symbol selected to the symbol_list\n",
    "        symbol_list.append(current_symb)\n",
    "        \n",
    "        #Recursively call DPLL as the model and symbols (among other things) are updated\n",
    "        return (DPLL(KB,set(rest), update(model,current_symb,True),heuristic_level,symbol_list) or \n",
    "                DPLL(KB,set(rest), update(model,current_symb,False),heuristic_level,symbol_list))\n",
    "    \n",
    "    \n",
    "    elif heuristic_level==2:\n",
    "        \n",
    "        #Apply the PURE SYMBOL HEURISTIC\n",
    "        current_symb, value = find_pure_symbol(symbols, unknown_clauses, model)\n",
    "        \n",
    "        #If a pure symbol was found\n",
    "        if current_symb: \n",
    "\n",
    "            #Add it to the symbol_list to indicate assignment\n",
    "            symbol_list.append(current_symb)\n",
    "\n",
    "            #Get the rest of the symbols (after current_symb has been excluded)\n",
    "            rest = symbols.copy()\n",
    "            rest.remove(current_symb)\n",
    "\n",
    "            #Recursively run the pure symbol heuristic assigning values to the pure symbols that\n",
    "            #make them True in all the clauses, while updating the model and symbols\n",
    "            return DPLL(KB, rest,update(model,current_symb,value),heuristic_level,symbol_list)\n",
    "            \n",
    "        #Apply the UNIT CLAUSE HEURISTIC\n",
    "        current_symb, value = find_unit_clause(unknown_clauses, model)\n",
    "        \n",
    "        #If a unit clause was found\n",
    "        if current_symb: \n",
    "\n",
    "            #Add the unit clause symbol to the symbol_list to indicate assignment\n",
    "            symbol_list.append(current_symb)\n",
    "\n",
    "            #Get the rest of the symbols (after current_symb has been excluded)\n",
    "            rest = symbols.copy()\n",
    "            rest.remove(current_symb)\n",
    "\n",
    "            #Recursively run the unit clause heuristic to find unit clauses, and assign values them \n",
    "            #that make them True. This step is especially important given unit propagation\n",
    "            #(assignment of one unit clause could create other unit clauses)\n",
    "            return DPLL(KB, rest,update(model,current_symb,value),heuristic_level,symbol_list)\n",
    "        \n",
    "        \n",
    "        #Apply the DEGREE HEURISTIC when no pure symbols or unit clauses are found\n",
    "        current_symb, rest = degree_heuristic(symbols,unknown_clauses,model)\n",
    "    \n",
    "        \n",
    "        #Add the selected symbol to the symbol list\n",
    "        symbol_list.append(current_symb)\n",
    "        \n",
    "        #Recursively call DPLL on the updated model and symbol set\n",
    "        return (DPLL(KB,set(rest), update(model,current_symb,True),heuristic_level,symbol_list) or \n",
    "                DPLL(KB,set(rest), update(model,current_symb,False),heuristic_level,symbol_list))\n",
    "    \n",
    "    \n",
    "    elif heuristic_level== 3:\n",
    "        \n",
    "        #Apply the ADAPTED PURE SYMBOL HEURISTIC (DEGREE HEURISTIC TYPE ALTERATION)\n",
    "        current_symb, value = find_pure_symbol(symbols, unknown_clauses, model, True)\n",
    "        \n",
    "        #If a pure symbol was found\n",
    "        if current_symb: \n",
    "\n",
    "            #Add it to the symbol_list to indicate assignment\n",
    "            symbol_list.append(current_symb)\n",
    "\n",
    "            #Get the rest of the symbols (after current_symb has been excluded)\n",
    "            rest = symbols.copy()\n",
    "            rest.remove(current_symb)\n",
    "\n",
    "            #Recursively run the pure symbol heuristic assigning values to the pure symbols that\n",
    "            #make them True in all the clauses\n",
    "            return DPLL(KB, rest,update(model,current_symb,value),heuristic_level,symbol_list)\n",
    "        \n",
    "        #Apply the UNIT CLAUSE HEURISTIC\n",
    "        current_symb, value = find_unit_clause(unknown_clauses, model)\n",
    "        \n",
    "        #If a unit clause was found\n",
    "        if current_symb: \n",
    "\n",
    "            #Add the unit clause symbol to the symbol_list to indicate assignment\n",
    "            symbol_list.append(current_symb)\n",
    "\n",
    "            #Get the rest of the symbols (after current_symb has been excluded)\n",
    "            rest = symbols.copy()\n",
    "            rest.remove(current_symb)\n",
    "\n",
    "            #Recursively run the unit clause heuristic to find unit clauses, and assign values them \n",
    "            #that make them True. This step is especially important given unit propagation\n",
    "            #(assignment of one unit clause could create other unit clauses)\n",
    "            return DPLL(KB, rest,update(model,current_symb,value),heuristic_level,symbol_list)\n",
    "        \n",
    "        #Apply the DEGREE HEURISTIC when no pure symbol is found\n",
    "        current_symb, rest = degree_heuristic(symbols,unknown_clauses,model)\n",
    "        \n",
    "        #Add the selected symbol to symbol_list\n",
    "        symbol_list.append(current_symb)\n",
    "        \n",
    "        #Recursively call DPLL\n",
    "        return (DPLL(KB,set(rest), update(model,current_symb,True),heuristic_level,symbol_list) or \n",
    "                DPLL(KB,set(rest), update(model,current_symb,False),heuristic_level,symbol_list))\n",
    "        \n",
    "    #If heuristic_level is 0 (BASIC FUNCTIONALITY TEST)\n",
    "    else:\n",
    "        \n",
    "        #Select a symbol and exclude it from symbols to get rest\n",
    "        current_symb, *rest = symbols\n",
    "        \n",
    "        #Add the selected symbol to the symbol_list\n",
    "        symbol_list.append(current_symb)\n",
    "        \n",
    "        #Recursively call DPLL on the updated model and symbol set\n",
    "        return (DPLL(KB,set(rest),update(model,current_symb,True),heuristic_level,symbol_list) or \n",
    "                DPLL(KB,set(rest),update(model,current_symb,False),heuristic_level,symbol_list))\n",
    "    \n",
    "    \n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "markdown",
     "checksum": "1a373b0f237fb333214a04ced058f50f",
     "grade": false,
     "grade_id": "cell-8c6248549aeaca88",
     "locked": true,
     "schema_version": 3,
     "solution": false,
     "task": false
    }
   },
   "source": [
    "<h1>Question 3</h1>\n",
    "\n",
    "Implement your KB from Russell & Norvig in CNF by filling in the sets inside the list <code>KB</code> below.  Ensure that your KB is in a list of set format as stated in the assignment instructions."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "- **S1: A $\\Leftrightarrow$ (B $\\lor$ E)**\n",
    "    - [A $\\Rightarrow$ (B $\\lor$ E)] $\\land$ [(B $\\lor$ E) $\\Rightarrow$ A]  (Biconditional Elimination)\n",
    "    \n",
    "    - ($\\lnot$ A $\\lor$ B $\\lor$ E) $\\land$ [$\\lnot$(B $\\lor$ E) $\\lor$ A] (Implication Elimination)\n",
    "    \n",
    "    - ($\\lnot$A $\\lor$ B $\\lor$ E) $\\land$ [($\\lnot$B $\\land$ $\\lnot$E) $\\lor$ A] (De Morgan's Law)\n",
    "    \n",
    "    - ($\\lnot$A $\\lor$ B $\\lor$ E) $\\land$ ($\\lnot$B $\\lor$ A) $\\land$ ($\\lnot$E $\\lor$ A) (Distributive law)\n",
    "    \n",
    "    \n",
    "    \n",
    "- **S2: E $\\Rightarrow$ D**\n",
    "    - $\\lnot$E $\\lor$ D (Implication Elimination)\n",
    "    \n",
    "    \n",
    "- **S3: C $\\land$ F $\\Rightarrow$ $\\lnot$ B**\n",
    "    - $\\lnot$(C $\\land$ F) $\\lor$ $\\lnot$ B (Implication Elimination)\n",
    "    \n",
    "    - $\\lnot$C $\\lor$ $\\lnot$F $\\lor$ $\\lnot$ B (De Morgan's Law)\n",
    "    \n",
    "\n",
    "- **S4: E $\\Rightarrow$ B**\n",
    "    - $\\lnot$E $\\lor$ B (Implication Elimination)\n",
    "    \n",
    "    \n",
    "- **S5: B $\\Rightarrow$ F**\n",
    "    - $\\lnot$B $\\lor$ F (Implication Elimination)\n",
    "    \n",
    "    \n",
    "- **S6: B $\\Rightarrow$ C**\n",
    "    - $\\lnot$B $\\lor$ C (Implication Elimination)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {
    "deletable": false,
    "nbgrader": {
     "cell_type": "code",
     "checksum": "a545c5a7e460e8a160a96549fba09556",
     "grade": false,
     "grade_id": "cell-2600ca4ae2649468",
     "locked": false,
     "schema_version": 3,
     "solution": true,
     "task": false
    }
   },
   "outputs": [],
   "source": [
    "# Define some literals\n",
    "A = Literal('A')\n",
    "B = Literal('B')\n",
    "C = Literal('C')\n",
    "D = Literal('D')\n",
    "E = Literal('E')\n",
    "F = Literal('F')\n",
    "\n",
    "#Translating the CNF sentences above into the KB, we get:\n",
    "KB = [{-A,B,E},{-B,A},{-E,A},{-E,D},{-C,-F,-B},{-E,B},{-B,F},{-B,C}]"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "markdown",
     "checksum": "197d7a486e328210a1d13c24747b3111",
     "grade": false,
     "grade_id": "cell-3e6849da5a8eba9a",
     "locked": true,
     "schema_version": 3,
     "solution": false,
     "task": false
    }
   },
   "source": [
    "<h1>Extensions</h1>\n",
    "\n",
    "1. Implement the degree heuristic for choosing symbols.  If <code>heuristic_level=1</code>, then the degree heuristic should be used to select which symbol to assign.\n",
    "2. Implement the pure symbol and unit clause heuristics.  If <code>heuristic_level=2</code>, then these heuristics should be used to find select first a pure symbol, and if one is not found, then a unit clause.  If neither pure symbols nor unit clauses are found, then the degree heuristic should be used to select a symbol.  If there are multiple pure symbols or unit clauses found, then use alphabetical order to select amongst them.\n",
    "3. Modify the pure symbol heuristic to choose the pure symbol that occurs in the most number of clauses.  This should be activated if <code>heuristic_level=3</code>."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "markdown",
     "checksum": "755ed998a518249d48e3e3518ec2ed63",
     "grade": false,
     "grade_id": "cell-f24016ad18be5ed3",
     "locked": true,
     "schema_version": 3,
     "solution": false,
     "task": false
    }
   },
   "source": [
    "<h1>Basic Functionality Tests</h1>\n",
    "\n",
    "All of the tests in this section must be passed for the code to be considered fully functional.  Other unseen test cases will be used after submission to further verify functionality"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "code",
     "checksum": "ea88980a283406b7789cd4f485dc3172",
     "grade": true,
     "grade_id": "cell-6af1cbc180046559",
     "locked": true,
     "points": 1,
     "schema_version": 3,
     "solution": false,
     "task": false
    }
   },
   "outputs": [],
   "source": [
    "# This section will test the correct definition of the literal class\n",
    "\n",
    "\n",
    "# Test the name attribute works correctly\n",
    "assert(A.name == 'A')\n",
    "\n",
    "# Test that negation works correctly\n",
    "assert(not (-C).sign)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "code",
     "checksum": "9264e8da332b50a0adf2a1de4ec4a591",
     "grade": true,
     "grade_id": "cell-76b5f4949b4918a0",
     "locked": true,
     "points": 2,
     "schema_version": 3,
     "solution": false,
     "task": false
    }
   },
   "outputs": [],
   "source": [
    "# This section will test that the KB has been correctly converted to CNF by performing \n",
    "# tests over all possible models\n",
    "import itertools\n",
    "symbols = {A,B,C,D,E,F}\n",
    "symbol_list = [A,B,C,D,E,F]\n",
    "\n",
    "def evaluate_russell_norvig_KB(model):\n",
    "    # Manually evaluate the KB using the model\n",
    "    s = list()\n",
    "    s.append(model[A] == (model[B] or model[E]))\n",
    "    s.append(model[E] <= model[D])\n",
    "    s.append((model[C] and model[F]) <= (not model[B]))\n",
    "    s.append(model[E] <= model[B])\n",
    "    s.append(model[B] <= model[F])\n",
    "    s.append(model[B] <= model[C])\n",
    "    return all(s)\n",
    "\n",
    "def evaluate_KB(KB, model):\n",
    "    model_true = True\n",
    "    model_name_dict = {l.name: model[l] for l in model}\n",
    "    for clause in KB:\n",
    "        evaluation = {l.sign == model_name_dict[l.name] for l in clause if l.name in model_name_dict}\n",
    "        model_true = model_true and any(evaluation)\n",
    "    return model_true\n",
    "\n",
    "all_models = list(itertools.product([False, True], repeat=6))\n",
    "for i in range(0, len(all_models)):\n",
    "    # Test all truth values\n",
    "    test_model = {symbol_list[j]: all_models[i][j] for j in range(0,6)}\n",
    "    \n",
    "    # Test the model\n",
    "    assert(evaluate_russell_norvig_KB(test_model) == evaluate_KB(KB, test_model))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "code",
     "checksum": "bd40af18e4e25d64cb61ca9425b25eeb",
     "grade": true,
     "grade_id": "cell-5007c88f303571cb",
     "locked": true,
     "points": 4,
     "schema_version": 3,
     "solution": false,
     "task": false
    }
   },
   "outputs": [],
   "source": [
    "# This section will test the basic working of DPLL\n",
    "# Satisfiable model\n",
    "test_KB = [{A, C},{-A, C}, {B, -C}]\n",
    "t, model, symbol_trace = DPLL_Satisfiable(test_KB)\n",
    "assert(evaluate_KB(test_KB, model))\n",
    "assert(t)\n",
    "\n",
    "# Unsatisfiable model\n",
    "test_KB = [{A, C},{-A, C}, {-C}]\n",
    "t, model, symbol_trace = DPLL_Satisfiable(test_KB)\n",
    "assert(not t)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "code",
     "checksum": "5d93f38084e3ef0a6cf8b286f3e12054",
     "grade": true,
     "grade_id": "cell-63ce3735a6a8d49e",
     "locked": true,
     "points": 8,
     "schema_version": 3,
     "solution": false,
     "task": false
    },
    "scrolled": true
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "{B: False, F: True, C: True, A: False, E: False}\n"
     ]
    }
   ],
   "source": [
    "# This will test DPLL on the KB from Russell & Norvig\n",
    "t, model, symbol_trace = DPLL_Satisfiable(KB,0)\n",
    "print(model)\n",
    "\n",
    "# This model is satisfiable.  Test that it is so\n",
    "assert(t)\n",
    "\n",
    "# Check that the model found actually works\n",
    "assert(evaluate_KB(KB, model)) "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "markdown",
     "checksum": "f01239be43d1b96af4269b659140441a",
     "grade": false,
     "grade_id": "cell-d4a09c27c6cafd14",
     "locked": true,
     "schema_version": 3,
     "solution": false,
     "task": false
    }
   },
   "source": [
    "<h1>Extension Tests</h1>\n",
    "\n",
    "This section will test that the degree heuristic, pure symbol and unit clause heuristics are correctly implemented.  Note that in your code, the <code>heuristic_level</code> needs to correctly activate the heuristic being tested, and the <code>symbol_list</code> needs to be correctly generated "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "code",
     "checksum": "c22796e4310c481858d9941480d3abc2",
     "grade": true,
     "grade_id": "cell-782f68d63b7be51f",
     "locked": true,
     "points": 16,
     "schema_version": 3,
     "solution": false,
     "task": false
    }
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "{B: False, E: False, A: False}\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "[B, A, C, F, E, A]"
      ]
     },
     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# Degree Heuristic Test for KB from Russell & Norvig\n",
    "t, model, symbol_trace = DPLL_Satisfiable(KB,1)\n",
    "print(model)\n",
    "\n",
    "# This model is satisfiable.  Test that it is so\n",
    "assert(t)\n",
    "\n",
    "# Check that the model found actually works\n",
    "assert(evaluate_KB(KB, model))  \n",
    "\n",
    "# Test the symbol trace to ensure that the correct order is chosen\n",
    "assert([l.name for l in symbol_trace] in [['B','F', 'E', 'C', 'C', 'E', 'A'], ['B', 'A', 'C', 'F', 'E', 'A']])\n",
    "\n",
    "symbol_trace"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "code",
     "checksum": "0257a3a8ed46849441e37da29fdce593",
     "grade": true,
     "grade_id": "cell-1849b5bca210fac7",
     "locked": true,
     "points": 32,
     "schema_version": 3,
     "solution": false,
     "task": false
    }
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "{D: True, B: False, E: False, A: False}\n"
     ]
    }
   ],
   "source": [
    "# Pure Symbol & Unit Clause Heuristic Test for KB from Russell & Norvig\n",
    "t, model, symbol_trace = DPLL_Satisfiable(KB,2)\n",
    "print(model)\n",
    "\n",
    "\n",
    "# This model is satisfiable.  Test that it is so\n",
    "assert(t)\n",
    "\n",
    "# Check that the model found actually works\n",
    "assert(evaluate_KB(KB, model))\n",
    "\n",
    "# Test the symbol trace to ensure that the correct order is chosen\n",
    "assert([l.name for l in symbol_trace] == ['D', 'B', 'E', 'A', 'C', 'F', 'E', 'A'])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "cell_type": "code",
     "checksum": "01a5632a5bf35a1a3a9c8202f7c79b53",
     "grade": true,
     "grade_id": "cell-b9ce4afcdb630096",
     "locked": true,
     "points": 64,
     "schema_version": 3,
     "solution": false,
     "task": false
    }
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "{D: True, B: False, E: False, A: False}\n",
      "[D, B, A, C, F, E, A]\n"
     ]
    }
   ],
   "source": [
    "# Pure Symbol & Unit Clause Heuristic Test, choosing the most-frequently used pure symbol, for KB from Russell & Norvig\n",
    "t, model, symbol_trace = DPLL_Satisfiable(KB,3)\n",
    "print(model)\n",
    "print(symbol_trace)\n",
    "\n",
    "# This model is satisfiable.  Test that it is so\n",
    "assert(t)\n",
    "\n",
    "# Check that the model found actually works\n",
    "assert(evaluate_KB(KB, model))\n",
    "\n",
    "# Test the symbol trace to ensure that the correct order is chosen\n",
    "assert([l.name for l in symbol_trace] == ['D', 'B', 'A', 'C', 'F', 'E', 'A'])"
   ]
  }
 ],
 "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.7.11"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}