diff --git a/README.md b/README.md index 4b8b4528f..96f2e6994 100644 --- a/README.md +++ b/README.md @@ -102,7 +102,7 @@ Here is a table of algorithms, the figure, name of the algorithm in the book and | 7.17 | DPLL-Satisfiable? | `dpll_satisfiable` | [`logic.py`][logic] | Done | Included | | 7.18 | WalkSAT | `WalkSAT` | [`logic.py`][logic] | Done | Included | | 7.20 | Hybrid-Wumpus-Agent | `HybridWumpusAgent` | | | | -| 7.22 | SATPlan | `SAT_plan` | [`logic.py`][logic] | Done | | +| 7.22 | SATPlan | `SAT_plan` | [`logic.py`][logic] | Done | Included | | 9 | Subst | `subst` | [`logic.py`][logic] | Done | | | 9.1 | Unify | `unify` | [`logic.py`][logic] | Done | Included | | 9.3 | FOL-FC-Ask | `fol_fc_ask` | [`logic.py`][logic] | Done | | diff --git a/logic.ipynb b/logic.ipynb index 92b8f51ed..3097b7609 100644 --- a/logic.ipynb +++ b/logic.ipynb @@ -23,9 +23,7 @@ { "cell_type": "code", "execution_count": 1, - "metadata": { - "collapsed": true - }, + "metadata": {}, "outputs": [], "source": [ "from utils import *\n", @@ -79,9 +77,7 @@ { "cell_type": "code", "execution_count": 3, - "metadata": { - "collapsed": true - }, + "metadata": {}, "outputs": [], "source": [ "(x, y, P, Q, f) = symbols('x, y, P, Q, f')" @@ -409,9 +405,7 @@ { "cell_type": "code", "execution_count": 15, - "metadata": { - "collapsed": true - }, + "metadata": {}, "outputs": [], "source": [ "wumpus_kb = PropKB()" @@ -429,9 +423,7 @@ { "cell_type": "code", "execution_count": 16, - "metadata": { - "collapsed": true - }, + "metadata": {}, "outputs": [], "source": [ "P11, P12, P21, P22, P31, B11, B21 = expr('P11, P12, P21, P22, P31, B11, B21')" @@ -448,9 +440,7 @@ { "cell_type": "code", "execution_count": 17, - "metadata": { - "collapsed": true - }, + "metadata": {}, "outputs": [], "source": [ "wumpus_kb.tell(~P11)" @@ -466,9 +456,7 @@ { "cell_type": "code", "execution_count": 18, - "metadata": { - "collapsed": true - }, + "metadata": {}, "outputs": [], "source": [ "wumpus_kb.tell(B11 | '<=>' | ((P12 | P21)))\n", @@ -485,9 +473,7 @@ { "cell_type": "code", "execution_count": 19, - "metadata": { - "collapsed": true - }, + "metadata": {}, "outputs": [], "source": [ "wumpus_kb.tell(~B11)\n", @@ -1196,9 +1182,7 @@ { "cell_type": "code", "execution_count": 30, - "metadata": { - "collapsed": true - }, + "metadata": {}, "outputs": [], "source": [ "%psource eliminate_implications" @@ -1207,9 +1191,7 @@ { "cell_type": "code", "execution_count": 31, - "metadata": { - "collapsed": true - }, + "metadata": {}, "outputs": [], "source": [ "%psource move_not_inwards" @@ -1218,9 +1200,7 @@ { "cell_type": "code", "execution_count": 32, - "metadata": { - "collapsed": true - }, + "metadata": {}, "outputs": [], "source": [ "%psource distribute_and_over_or" @@ -1831,9 +1811,7 @@ { "cell_type": "code", "execution_count": 42, - "metadata": { - "collapsed": true - }, + "metadata": {}, "outputs": [], "source": [ "clauses = ['(B & F)==>E', \n", @@ -1857,9 +1835,7 @@ { "cell_type": "code", "execution_count": 43, - "metadata": { - "collapsed": true - }, + "metadata": {}, "outputs": [], "source": [ "definite_clauses_KB = PropDefiniteKB()\n", @@ -2303,7 +2279,7 @@ { "data": { "text/plain": [ - "{C: False, A: True, D: True, B: True}" + "{A: True, B: True, C: False, D: True}" ] }, "execution_count": 51, @@ -2330,7 +2306,7 @@ { "data": { "text/plain": [ - "{C: True, D: False, B: True}" + "{B: True, D: False}" ] }, "execution_count": 52, @@ -2379,7 +2355,7 @@ { "data": { "text/plain": [ - "{C: True, A: True, B: False}" + "{A: False, B: True, C: True}" ] }, "execution_count": 54, @@ -2399,7 +2375,7 @@ { "data": { "text/plain": [ - "{C: True, A: True}" + "{B: True, C: True}" ] }, "execution_count": 55, @@ -2586,9 +2562,7 @@ { "cell_type": "code", "execution_count": 57, - "metadata": { - "collapsed": true - }, + "metadata": {}, "outputs": [], "source": [ "A, B, C, D = expr('A, B, C, D')" @@ -2602,7 +2576,7 @@ { "data": { "text/plain": [ - "{C: False, A: True, D: True, B: True}" + "{A: True, B: True, C: False, D: True}" ] }, "execution_count": 58, @@ -2629,7 +2603,7 @@ { "data": { "text/plain": [ - "{C: True, A: True, B: True}" + "{A: True, B: True, C: True}" ] }, "execution_count": 59, @@ -2649,7 +2623,7 @@ { "data": { "text/plain": [ - "{C: True, A: True, D: True, B: True}" + "{A: True, B: True, C: True, D: True}" ] }, "execution_count": 60, @@ -2689,9 +2663,7 @@ { "cell_type": "code", "execution_count": 62, - "metadata": { - "collapsed": true - }, + "metadata": {}, "outputs": [], "source": [ "def WalkSAT_CNF(sentence, p=0.5, max_flips=10000):\n", @@ -2713,7 +2685,7 @@ { "data": { "text/plain": [ - "{A: False, D: False, C: True, B: False}" + "{A: False, B: False, C: True, D: False}" ] }, "execution_count": 63, @@ -2741,9 +2713,7 @@ { "cell_type": "code", "execution_count": 64, - "metadata": { - "collapsed": true - }, + "metadata": {}, "outputs": [], "source": [ "sentence_1 = A |'<=>'| B\n", @@ -2760,7 +2730,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "100 loops, best of 3: 2.46 ms per loop\n" + "6.78 ms ± 238 µs per loop (mean ± std. dev. of 7 runs, 100 loops each)\n" ] } ], @@ -2780,7 +2750,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "100 loops, best of 3: 1.91 ms per loop\n" + "4.64 ms ± 65.3 µs per loop (mean ± std. dev. of 7 runs, 100 loops each)\n" ] } ], @@ -2801,6 +2771,280 @@ "Feel free to play around with this to understand the trade-offs of these algorithms better." ] }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "### SATPlan" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "In this section we show how to make plans by logical inference. The basic idea is very simple. It includes the following three steps:\n", + "1. Constuct a sentence that includes:\n", + " 1. A colection of assertions about the initial state.\n", + " 2. The successor-state axioms for all the possible actions at each time up to some maximum time t.\n", + " 3. The assertion that the goal is achieved at time t.\n", + "2. Present the whole sentence to a SAT solver.\n", + "3. Assuming a model is found, extract from the model those variables that represent actions and are assigned true. Together they represent a plan to achieve the goals.\n", + "\n", + "\n", + "Lets have a look at the algorithm" + ] + }, + { + "cell_type": "code", + "execution_count": 67, + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "\n", + "\n", + "\n", + "\n", + " \n", + " \n", + " \n", + "\n", + "\n", + "

\n", + "\n", + "
def SAT_plan(init, transition, goal, t_max, SAT_solver=dpll_satisfiable):\n",
+       "    """Converts a planning problem to Satisfaction problem by translating it to a cnf sentence.\n",
+       "    [Figure 7.22]"""\n",
+       "\n",
+       "    # Functions used by SAT_plan\n",
+       "    def translate_to_SAT(init, transition, goal, time):\n",
+       "        clauses = []\n",
+       "        states = [state for state in transition]\n",
+       "\n",
+       "        # Symbol claiming state s at time t\n",
+       "        state_counter = itertools.count()\n",
+       "        for s in states:\n",
+       "            for t in range(time+1):\n",
+       "                state_sym[s, t] = Expr("State_{}".format(next(state_counter)))\n",
+       "\n",
+       "        # Add initial state axiom\n",
+       "        clauses.append(state_sym[init, 0])\n",
+       "\n",
+       "        # Add goal state axiom\n",
+       "        clauses.append(state_sym[goal, time])\n",
+       "\n",
+       "        # All possible transitions\n",
+       "        transition_counter = itertools.count()\n",
+       "        for s in states:\n",
+       "            for action in transition[s]:\n",
+       "                s_ = transition[s][action]\n",
+       "                for t in range(time):\n",
+       "                    # Action 'action' taken from state 's' at time 't' to reach 's_'\n",
+       "                    action_sym[s, action, t] = Expr(\n",
+       "                        "Transition_{}".format(next(transition_counter)))\n",
+       "\n",
+       "                    # Change the state from s to s_\n",
+       "                    clauses.append(action_sym[s, action, t] |'==>'| state_sym[s, t])\n",
+       "                    clauses.append(action_sym[s, action, t] |'==>'| state_sym[s_, t + 1])\n",
+       "\n",
+       "        # Allow only one state at any time\n",
+       "        for t in range(time+1):\n",
+       "            # must be a state at any time\n",
+       "            clauses.append(associate('|', [state_sym[s, t] for s in states]))\n",
+       "\n",
+       "            for s in states:\n",
+       "                for s_ in states[states.index(s) + 1:]:\n",
+       "                    # for each pair of states s, s_ only one is possible at time t\n",
+       "                    clauses.append((~state_sym[s, t]) | (~state_sym[s_, t]))\n",
+       "\n",
+       "        # Restrict to one transition per timestep\n",
+       "        for t in range(time):\n",
+       "            # list of possible transitions at time t\n",
+       "            transitions_t = [tr for tr in action_sym if tr[2] == t]\n",
+       "\n",
+       "            # make sure at least one of the transitions happens\n",
+       "            clauses.append(associate('|', [action_sym[tr] for tr in transitions_t]))\n",
+       "\n",
+       "            for tr in transitions_t:\n",
+       "                for tr_ in transitions_t[transitions_t.index(tr) + 1:]:\n",
+       "                    # there cannot be two transitions tr and tr_ at time t\n",
+       "                    clauses.append(~action_sym[tr] | ~action_sym[tr_])\n",
+       "\n",
+       "        # Combine the clauses to form the cnf\n",
+       "        return associate('&', clauses)\n",
+       "\n",
+       "    def extract_solution(model):\n",
+       "        true_transitions = [t for t in action_sym if model[action_sym[t]]]\n",
+       "        # Sort transitions based on time, which is the 3rd element of the tuple\n",
+       "        true_transitions.sort(key=lambda x: x[2])\n",
+       "        return [action for s, action, time in true_transitions]\n",
+       "\n",
+       "    # Body of SAT_plan algorithm\n",
+       "    for t in range(t_max):\n",
+       "        # dictionaries to help extract the solution from model\n",
+       "        state_sym = {}\n",
+       "        action_sym = {}\n",
+       "\n",
+       "        cnf = translate_to_SAT(init, transition, goal, t)\n",
+       "        model = SAT_solver(cnf)\n",
+       "        if model is not False:\n",
+       "            return extract_solution(model)\n",
+       "    return None\n",
+       "
\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "psource(SAT_plan)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Let's see few examples of its usage. First we define a transition and then call `SAT_plan`." + ] + }, + { + "cell_type": "code", + "execution_count": 68, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "None\n", + "['Right']\n", + "['Left', 'Left']\n" + ] + } + ], + "source": [ + "transition = {'A': {'Left': 'A', 'Right': 'B'},\n", + " 'B': {'Left': 'A', 'Right': 'C'},\n", + " 'C': {'Left': 'B', 'Right': 'C'}}\n", + "\n", + "\n", + "print(SAT_plan('A', transition, 'C', 2)) \n", + "print(SAT_plan('A', transition, 'B', 3))\n", + "print(SAT_plan('C', transition, 'A', 3))" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Let us do the same for another transition." + ] + }, + { + "cell_type": "code", + "execution_count": 69, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "['Right', 'Down']\n" + ] + } + ], + "source": [ + "transition = {(0, 0): {'Right': (0, 1), 'Down': (1, 0)},\n", + " (0, 1): {'Left': (1, 0), 'Down': (1, 1)},\n", + " (1, 0): {'Right': (1, 0), 'Up': (1, 0), 'Left': (1, 0), 'Down': (1, 0)},\n", + " (1, 1): {'Left': (1, 0), 'Up': (0, 1)}}\n", + "\n", + "\n", + "print(SAT_plan((0, 0), transition, (1, 1), 4))" + ] + }, { "cell_type": "markdown", "metadata": {}, @@ -3816,7 +4060,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.1" + "version": "3.6.4" } }, "nbformat": 4,