{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# CS 4100 Homework 02 \n",
    "\n",
    "#### Due Thursday  2/2 at midnight (1 minute after 11:59 pm) in Gradescope (with a grace period of 6 hours)\n",
    "#### You may submit the homework up to 24 hours late (with the same grace period) for a penalty of 10%. \n",
    "\n",
    "You must submit the homework in Gradescope as a zip file containing <b>two files:</b>\n",
    "- The <code>.ipynb</code> file (be sure to <code>Kernel -> Restart and Run All</code> before you submit); and\n",
    "- A <code>.pdf</code> file of the notebook. \n",
    "\n",
    "For best results obtaining a clean PDF file on the Mac, select <code>File -> Print Review</code> from the Jupyter window, then choose <code>File-> Print</code> in your browser and then <code>Save as PDF</code>.  Something  similar should be possible on a Windows machine. \n",
    "\n",
    "\n",
    " \n",
    "All homeworks will be scored with a maximum of 100 points; if point values are not given for individual\n",
    "problems, then all problems will be counted equally. \n",
    "\n",
    "Note: I have uploaded my solution for HW 01 on the class web page if you wish to use it; some of the code in HW 01 will be needed in this homework. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Here are some useful utility functions for examining the results of your code. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "-B\n",
      "{ C, -B }\n",
      "[ { A }, { B, -A }, { C, -B, -A } ]\n",
      "[ { A }, {}, { -B } ]\n"
     ]
    }
   ],
   "source": [
    "# This will pretty-print literals, clauses, and clause lists.\n",
    "# It will print out propositional letters as A, B, C, ...\n",
    "    \n",
    "def literal2String(L):\n",
    "    return ('-' if (L<0) else '') + chr(ord('A')+abs(L)-1)\n",
    "\n",
    "def clause2String(C):\n",
    "    if(C=={}):\n",
    "        return '{}'\n",
    "    else:\n",
    "        return '{ '+(', '.join([literal2String(L) for L in C]))+' }'\n",
    "\n",
    "def clauseList2String(A):\n",
    "    return '[ '+(', '.join([clause2String(C) for C in A]))+' ]'\n",
    "\n",
    "def pprint(X):\n",
    "    if(type(X)==int):              # X is literal\n",
    "        print(literal2String(X))\n",
    "    elif(type(X)==set):            # X is a clause\n",
    "        print(clause2String(X))\n",
    "    elif(type(X)==list):           # X is a clause list\n",
    "        print(clauseList2String(X))\n",
    "    else:\n",
    "        print('Error in pprint!')\n",
    "\n",
    "        #test\n",
    "\n",
    "pprint(-2)\n",
    "pprint({3,-2})\n",
    "pprint([ {1},{-1,2}, {-2,-1,3} ])\n",
    "pprint([ {1}, {}, {-2} ])\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Problem One: Resolution Theorem Proving in Propositional Logic (30 pts)\n",
    "\n",
    "In this problem we will explore the resolution calculus, using breadth-first search to find the empty clause (if it exists) in the resolvents generated from the input set. \n",
    "\n",
    "### Part A: Resolution Rule\n",
    "\n",
    "Complete the following template according to the definition of resolution given in your text and in lecture. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "{ A } { -A }\n",
      "[  ] \n",
      "\n",
      "{ A, B } { -C, -A }\n",
      "[  ] \n",
      "\n",
      "{} { A, -B }\n",
      "[  ] \n",
      "\n",
      "{ A, -C } { A, -B }\n",
      "[  ] \n",
      "\n",
      "{ A, B, C } { -C, -A, -B }\n",
      "[  ] \n",
      "\n"
     ]
    }
   ],
   "source": [
    "# Return all possible resolvents of clauses C1 and C2 (sets)\n",
    "\n",
    "def resolve(C1,C2):\n",
    "    pass\n",
    "    return [ ]               # just to get it to compile, replace with your code\n",
    "                \n",
    " \n",
    "# Tests -- Note that your sets may occur in a different order than shown here\n",
    "\n",
    "C1 = {1}\n",
    "C2 = {-1}\n",
    "print(clause2String(C1),clause2String(C2))                      \n",
    "print(clauseList2String(resolve(C1,C2)),'\\n')   # should be [ {} ]\n",
    "\n",
    "C1 = {1,2}\n",
    "C2 = {-1,-3}\n",
    "print(clause2String(C1),clause2String(C2))                      \n",
    "print(clauseList2String(resolve(C1,C2)),'\\n')   # should be [ { B, -C } ]\n",
    "\n",
    "C1 = {}\n",
    "C2 = {1,-2}\n",
    "print(clause2String(C1),clause2String(C2))                      \n",
    "print(clauseList2String(resolve(C1,C2)),'\\n')   # should be [  ]\n",
    "\n",
    "C1 = {1,-3}\n",
    "C2 = {1,-2}\n",
    "print(clause2String(C1),clause2String(C2))                      \n",
    "print(clauseList2String(resolve(C1,C2)),'\\n')   # should be [  ]\n",
    "\n",
    "C1 = {1,2,3}\n",
    "C2 = {-1,-2,-3}\n",
    "print(clause2String(C1),clause2String(C2))                      \n",
    "print(clauseList2String(resolve(C1,C2)),'\\n')   # should be [ { B, C, -C, -B }, { A, C, -C, -A }, { A, B, -A, -B } ]"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Part B: Resolution Rule Continued\n",
    "\n",
    "Complete the following template according to the definition of resolution given in your text and in lecture. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[ { C, -B, -A } ]\n",
      "{ -C }\n",
      "[  ]\n",
      "\n",
      "[ { A }, {}, { -C, -B, -A } ]\n",
      "{ -C }\n",
      "[  ]\n",
      "\n",
      "[  ]\n",
      "{ -C }\n",
      "[  ]\n",
      "\n",
      "[ { A }, { B, -A }, { C, -B, -A } ]\n",
      "{ A, -C }\n",
      "[  ]\n"
     ]
    }
   ],
   "source": [
    "# A is a list of clauses, C is a clause\n",
    "# Return list of all possible resolvents of C with a clause in A\n",
    "\n",
    "def resolveAll(A,C):   \n",
    "    pass\n",
    "    return [ ]               # just to get it to compile, replace with your code\n",
    "\n",
    "# tests\n",
    "\n",
    "KB = [ {-2,-1,3} ]\n",
    "NQ = {-3}\n",
    "\n",
    "pprint(KB)\n",
    "pprint(NQ)\n",
    "pprint(resolveAll(KB,NQ))     # should be [ { -B, -A } ]\n",
    "print()\n",
    "\n",
    "KB = [ {1}, {}, {-2,-1,-3} ]\n",
    "NQ = {-3}\n",
    "\n",
    "pprint(KB)\n",
    "pprint(NQ)\n",
    "pprint(resolveAll(KB,NQ))     # should be [  ]\n",
    "print()\n",
    "\n",
    "KB = [ ]\n",
    "NQ = {-3}\n",
    "\n",
    "pprint(KB)\n",
    "pprint(NQ)\n",
    "pprint(resolveAll(KB,NQ))     # should be [  ]\n",
    "print()\n",
    "\n",
    "KB = [ {1}, {-1,2}, {-2,-1,3} ]\n",
    "NQ = {-3,1}\n",
    "\n",
    "pprint(KB)\n",
    "pprint(NQ)\n",
    "pprint(resolveAll(KB,NQ))     # should be [ { B, -C }, { A, -B, -A }, { C, -C, -B } ]"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Part C:  Breadth-first Prover\n",
    "\n",
    "Write a function `prove1` which takes a set `CL`\n",
    "and searches for the empty clause by inserting all members of CL into a queue, and generating\n",
    "resolvents from the clause popped off the front of the queue with any member of the rest of queue, \n",
    "and adding them to the back of the queue. It should behave as shown below:\n",
    "\n",
    "- If the empty clause is found, report \"Unsatisfiable\";\n",
    "- If the queue empties out, report \"Satisfiable\"; \n",
    "- If the prover can not find the empty clause after 'limit' steps, report that fact. \n",
    "\n",
    "In each case, you should also report the number of steps (= times you popped the front off the queue);\n",
    "\n",
    "If the parameter `trace` is true, you should print out the queue at each step. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [],
   "source": [
    "# perform breath-first search from a set of clauses CL, by\n",
    "# inserting all of CL into a queue\n",
    "# and then searching using BFS by generating resolvents of head of queue with any\n",
    "# clause in the queue\n",
    "\n",
    "def prove1(CL,limit=30,trace=True):\n",
    "\n",
    "    pass                      # just to get it to compile, replace with your code\n",
    "               \n",
    "  "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\n",
      "test a \n",
      "------\n",
      "CL1a: [ { B }, { -B } ]\n",
      "\n",
      "\n",
      "test b \n",
      "------\n",
      "CL1b: [ { A }, { B, -A }, { C, -B }, { D, -C }, { -D } ]\n",
      "\n",
      "\n",
      "test c \n",
      "------\n",
      "CL1c: [ { A }, { B, C, -A }, { D, -C }, { E, -C }, { -E }, { -B } ]\n",
      "\n",
      "\n",
      "test d \n",
      "------\n",
      "CL1d: [ { A }, { B, C, -A }, { D, -C }, { E, -C }, { -E } ]\n",
      "\n",
      "\n"
     ]
    }
   ],
   "source": [
    "# tests: first 3 are unsatisfiable, test 4 is satisfiable\n",
    "\n",
    "print('\\ntest a','\\n------')\n",
    "CL1a = [ {2}, {-2} ]     \n",
    "\n",
    "print('CL1a: ',end=''); pprint(CL1a); print()\n",
    "prove1(CL1); print()\n",
    "\n",
    "print('test b','\\n------')\n",
    "CL1b = [ {1}, {-1,2}, {-2,3}, {-3,4}, {-4} ]\n",
    "\n",
    "print('CL1b: ',end=''); pprint(CL1b); print()\n",
    "prove1(CL1b); print()\n",
    "\n",
    "print('test c','\\n------')\n",
    "CL1c = [ {1}, {-1,2,3}, {-3,4}, {-3,5}, {-5}, {-2} ]\n",
    "\n",
    "print('CL1c: ',end=''); pprint(CL1c); print()\n",
    "prove1(CL1c); print()\n",
    "\n",
    "print('test d','\\n------')\n",
    "CL1d = [ {1}, {-1,2,3}, {-3,4}, {-3,5}, {-5} ]\n",
    "\n",
    "print('CL1d: ',end=''); pprint(CL1d); print()\n",
    "prove1(CL1d); print()\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Problem Two (10 pts)\n",
    "\n",
    "In this problem, we will experiment with our prover to understand its behavior. \n",
    "\n",
    "### Part A\n",
    "\n",
    "Generate a list of clauses `CL2a` such that\n",
    "\n",
    "-  CL2a is satisfiable, but \n",
    "-  It will make the prover run forever (in this case, not terminating with \"Satisfiable!\" within 30 steps)\n",
    "\n",
    "You must \n",
    "\n",
    "- Pretty-print CL2a\n",
    "- Prove that it is satisfiable (using your code from HW 01), \n",
    "- Show that it fails to terminate after 30 steps, and\n",
    "- Explain why your example behaves in this way. \n",
    "\n",
    "Note: Your example should be such that no matter how large `limit` is, it will not terminate; however,\n",
    "for purposes of grading, you should leave `limit=30` but `trace=False`.  \n",
    "\n",
    "Hint: See if you can get the prover to loop uselessly on the same clauses. It may help to\n",
    "think about the order in which clauses will be processed. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "scrolled": false
   },
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Part B  \n",
    "\n",
    "In this problem we will explore what happens when the clause set causes an exponential explosion \n",
    "in the search space. We will use a classic example of a clause set which requires exponential time (assuming\n",
    "$P\\ne NP$). \n",
    "\n",
    "First create a clause list `CL2b` from only 2 symbols which is unsatisfiable but causes\n",
    "exponential behavior. The easiest way to do this is to create a clause set with 4 clauses, each of\n",
    "which makes one row of the truth table for two symbols (say A and B) false. For example,\n",
    "for a row that has **(True,False)**, you would create $\\{ \\neg A, B \\} = \\neg A\\vee B.$ If you\n",
    "make sure that no row of the truth table is a model, then it must be unsatisfiable, but\n",
    "each clause is necessary to prove this fact (if you leave a clause out, then that row\n",
    "of the table would be a model). \n",
    "\n",
    "It should take 7 steps to determine unsatisfiability. \n",
    "\n",
    "As in Part A, \n",
    "\n",
    "- Pretty-print CL2b\n",
    "- Verify that it is unsatisfiable using code from HW 01\n",
    "- Show that it takes 7 steps to find the empty clause. \n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Part C\n",
    "\n",
    "Now, create a clause list `CL2d`from 3 symbols, with 8 clauses, along the same lines as the previous example (each\n",
    "clause makes one line of the truth table false).  \n",
    "\n",
    " \n",
    "\n",
    "To do:\n",
    "\n",
    "- Pretty-print CL2d\n",
    "- Prove that it is unsatisfiable as above\n",
    "- Run this with a limit of 3, 4, and 5 to get a sense for what this will do. Then turn off tracing and try it for a few more (very soon it will simply get lost in an exponential explosion).\n",
    "- Answer this question: How large could you make limit and still get \"Empty clause not found after ...\" to print out within say a minute?"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "scrolled": false
   },
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    " "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Refinements of Resolution\n",
    "\n",
    "There are various ways to make resolution more efficient, including\n",
    "\n",
    "- Set of Support Strategy: partition your clause set into subsets KB and SOS, such that KB is satisfiable, but KB + SOS is unsatisfiable; \n",
    "- Removing useless clauses such as tautologies and duplicates\n",
    "- Shortest-Clauses-First: use a priority queue instead of a queue, and keep it ordered by size, with\n",
    "smaller clauses to the front.\n",
    "\n",
    "The motivation for all of these is to prevent doing useless work, and--in the case of the shortest-first--to try to focus on creating short clauses as soon as possible. \n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Problem 3 (Set of Support) (10 pts)\n",
    "\n",
    "\n",
    "### Part A \n",
    "\n",
    "Rewrite your prover to create a function `prove3` which uses the set of support strategy, \n",
    "where the set of unsatisfiable clauses is separated into KB and SOS, in such a way that KB is\n",
    "known to be satisfiable. \n",
    "\n",
    "- Your prover will take KB and SOS as separate arguments;\n",
    "- Create your initial queue from SOS alone;\n",
    "- In each step, remove the head of the queue, and form resolvents between that clause\n",
    "and any clause in KB + Queue. \n",
    "\n",
    "Rewrite the tests from Problem One, Part A, such that the *last* clause in each list is removed\n",
    "and put in the SOS. The first one is done for you to show what is needed. \n",
    "\n",
    "Run your prover on these four examples to verify that all is working as expected. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "\"\\nprint('\\ntest 1','\\n------')\\nKB3a1 = [ {2} ]\\nSOS3a1 = [ {-2} ]\\n\\nprint('KB3a1: ',end=''); pprint(KB3a1); \\nprint('SOS3a1: ',end=''); pprint(SOS3a1); print()\\nprove3(KB3a1,SOS3a1); print()\\n\\n# etc for other 3\\n\""
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "'''\n",
    "print('\\ntest 1','\\n------')\n",
    "KB3a1 = [ {2} ]\n",
    "SOS3a1 = [ {-2} ]\n",
    "\n",
    "print('KB3a1: ',end=''); pprint(KB3a1); \n",
    "print('SOS3a1: ',end=''); pprint(SOS3a1); print()\n",
    "prove3(KB3a1,SOS3a1); print()\n",
    "\n",
    "# etc for other 3\n",
    "'''"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Part B\n",
    "\n",
    "Now take the same clause set as in Problem Two Part B, but move the last clause into the SOS and keep the other three in KB. Run this example with prove3. \n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Part C\n",
    "\n",
    "Now take the same clause set as in Problem Two Part C, but put the last clause in the SOS and the other 7 in KB.\n",
    "Experiment in the same way you did in Problem Two Part C. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "scrolled": true
   },
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Part D\n",
    "\n",
    "Provide a brief statement of what you observed using the set of support strategy. Explain why you think this behavior is happening.  "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": []
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Problem 4 (Removing Useless Clauses) (10 pts)\n",
    "\n",
    "Keeping the set of support strategy, in this problem you must rewrite your prover from Problem 3 as `prove4`, which\n",
    "checks clauses as they are generated by resolution, and does NOT put them in the queue\n",
    "if\n",
    "\n",
    "- They are tautologies (some symbol and its negation both appear in the clause);\n",
    "- They have already been generated before.\n",
    "\n",
    "For the second, you must create a set `Visited` which is a set (hash table) containing\n",
    "copies of all clauses generated at any time in the past; in order to create a set of\n",
    "sets, you will need to make copies of the clauses as `frozenset`s. Here is a brief\n",
    "example of how to do that:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "{frozenset({1, 2})}\n",
      "True\n"
     ]
    }
   ],
   "source": [
    "S = set()\n",
    "A = {1,2}\n",
    "\n",
    "S.add( frozenset(A) )\n",
    "print(S)\n",
    "print( A in S)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Part A\n",
    "\n",
    "Write `prove4` as specified; you probably want to create a separate function `isTautology(C)`. \n",
    "Test it on examples as in Problem 3, Part A, just to verify you have done it correctly. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "4"
      ]
     },
     "execution_count": 9,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": []
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Part B\n",
    "\n",
    "Now test it on the example from Problem Three, Part B. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "scrolled": false
   },
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Part C\n",
    "\n",
    "Now test it on the example from Problem Three, Part C, and experiment with it as\n",
    "before to see how far you can search in about one minute. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Part D\n",
    "\n",
    "Summarize what you observed. Does this strategy make a significant difference?\n",
    "\n",
    "(If you have an interest, you might try this on a similar example with 4 symbols....)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": []
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Problem Five (Shortest-Clauses-First) (10 pts)\n",
    "\n",
    "Now you should take your latest `prove4` and add one more refinement:  make your queue\n",
    "a priority queue ordered by size, with smaller clauses to the front.\n",
    "\n",
    "The easiest way to do this (certainly not the most efficient) is to simply sort the queue every time\n",
    "you add something to the end. You can sort a list of sets/lists using as key the size of the member\n",
    "set/list, as illustrated here:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "[{2, 3, 4}, {1, 2}, {3, 4}, {1}, {3}]"
      ]
     },
     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "A = [ {1,2}, {2,3,4}, {1}, {3}, {3,4}]\n",
    "\n",
    "A.sort(reverse=True, key=(lambda x: len(x)))            # sorts in place\n",
    "\n",
    "A"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Part A\n",
    "\n",
    "Rewrite `prove4` as `prove5` with a priority queue instead of a queue, as suggested, and test it\n",
    "on the same simple examples as in Part A of the previous two problems, to verify that it works as expected. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Part B\n",
    "Again, test your new prover on the example from Part B of the previous two problems. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Part C\n",
    "Again, test your new prover on the example from Part C of the previous two problems. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Part D\n",
    "\n",
    "What did you observe?  Did this make a significant difference in the amount of time it took to complete\n",
    "the proof?  \n",
    "\n",
    "Finally, do you think these refinements would reduce the exponential search space for such\n",
    "problems to polynomial size, or\n",
    "is exponential growth still a problem? (Hint: think about what you learned in your algorithms or\n",
    "complexity class about the Satisfiability Problem.)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Problem Six (10 pts)\n",
    "\n",
    "In this problem, we will use the fastest method, `prove5`, to solve some word problems which can\n",
    "be encoded as problems in propositional logic. For each, give the encoding of the statements\n",
    "in the problem as symbols. (You might want to review pp.32-33 in the textbook before starting.)\n",
    "\n",
    "\n",
    "### Part A\n",
    "\n",
    "Do problem 2.10 from your textbook. \n",
    "\n",
    "### Part B\n",
    "\n",
    "A man and a woman are talking. “I am a\n",
    "man” said the person with black hair. “I am a woman” said the person with white hair.\n",
    "At least one of them is lying.  Formalize the puzzle using propositional logic and show using resolution that both of them are lying.\n",
    "\n",
    "### Part C\n",
    "\n",
    "Three boxes are presented to you. One contains gold, the other two are empty.\n",
    "Each box has imprinted on it a clue as to its contents; the clues are:\n",
    "\n",
    "- Box 1 “The gold is not here”\n",
    "- Box 2 “The gold is not here”\n",
    "- Box 3 “The gold is in Box 2”\n",
    "\n",
    "Only one message is true; the other two are false. Which box has the gold?\n",
    "\n",
    "Formalize the puzzle using propositional logic and find the solution using resolution. \n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Problem Seven (First-Order Logic) (5 pts)\n",
    "\n",
    "Do problem 3.1 from your textbook. You may provide your solution using ASCII text; by hand-writing, scanning, and pasting; or (preferably) in Latex. "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Problem Eight (First-Order Logic)  (5 pts)\n",
    "\n",
    "Do problem 3.2 from your textbook. You may provide your solution using ASCII text; by hand-writing, scanning, and pasting; or (preferably) in Latex. "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Problem Nine (First-Order Logic)  (5 pts)\n",
    "\n",
    "Do problem 3.4 from your textbook. You may provide your solution using ASCII text; by hand-writing, scanning, and pasting; or (preferably) in Latex. "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Problem Ten (First-Order Logic)  (5 pts)\n",
    "\n",
    "Do problem 3.5 from your textbook. You may provide your solution using ASCII text; by hand-writing, scanning, and pasting; or (preferably) in Latex. "
   ]
  }
 ],
 "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.8"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}