Fix PlanRoute, WumpusPosition and WumpusKB inference; correct last-action axiom (#1249, partial #961)

Several independently-verifiable defects in the Hybrid Wumpus Agent stack:

- PlanRoute (search.py) mutated the search state in place (corrupting A*'s
  tree), wrote the y coordinate as a list (set_location(x, [y])), and its
  goal_test/h assumed a single (x, y) goal while callers pass a list of
  cells. Rewrite result() to return a fresh state, and make goal_test/h
  accept a collection of goal cells or position objects (matching
  orientation too, for shooting positions).
- WumpusPosition (logic.py) defined __eq__ but no __hash__, so it was
  unhashable and could not be used in A*'s explored set or plan_shot's set.
  Add __hash__.
- WumpusKB.ask_if_true used pl_resolution (full resolution closure), which
  does not terminate on the wumpus clause set. Use SAT entailment
  (KB & ~query unsatisfiable); verified to match tt_entails and to answer
  in well under a second.
- The 'rules about last action' axiom used a biconditional, wrongly forcing
  MoveForward whenever the agent is not turning; it must be an implication
  (the agent may instead grab/shoot/climb) (#1249).

Add a PlanRoute route-planning test. The remaining HybridWumpusAgent
work (execute() unvisited/orientation logic and WumpusEnvironment
integration) is tracked in #961.

Author: dmeoli

logic.py

@@ -1441,8 +1441,9 @@ def add_temporal_sentences(self, time):
         s = equiv(facing_south(time), a | b | c)
         self.tell(s)
 
-        # Rules about last action
-        self.tell(equiv(move_forward(t), ~turn_right(t) & ~turn_left(t)))
+        # Rules about last action: moving forward implies the agent did not turn
+        # (the converse does not hold -- the agent may instead grab, shoot or climb)
+        self.tell(implies(move_forward(t), ~turn_right(t) & ~turn_left(t)))
 
         # Rule about the arrow
         self.tell(equiv(have_arrow(time), have_arrow(t) & ~shoot(t)))
@@ -1451,7 +1452,10 @@ def add_temporal_sentences(self, time):
         self.tell(equiv(wumpus_alive(time), wumpus_alive(t) & ~percept_scream(time)))
 
     def ask_if_true(self, query):
-        return pl_resolution(self, query)
+        # the KB entails the query iff KB & ~query is unsatisfiable; using a SAT
+        # solver here instead of pl_resolution keeps inference tractable on the
+        # large wumpus clause set (full resolution closure does not terminate)
+        return not dpll_satisfiable(associate('&', self.clauses + conjuncts(to_cnf(~query))))
 
 
 # ______________________________________________________________________________
@@ -1482,6 +1486,9 @@ def __eq__(self, other):
         else:
             return False
 
+    def __hash__(self):
+        return hash((self.X, self.Y, self.orientation))
+
 
 # ______________________________________________________________________________
 

search.py

@@ -779,67 +779,61 @@ def actions(self, state):
 
     def result(self, state, action):
         """ Given state and action, return a new state that is the result of the action.
-        Action is assumed to be a valid action in the state """
+        Action is assumed to be a valid action in the state. A fresh state object is
+        returned; the input state is never mutated, so the search tree stays consistent. """
         x, y = state.get_location()
-        proposed_loc = list()
+        orientation = state.get_orientation()
+        proposed_loc = None
+        new_orientation = orientation
 
         # Move Forward
         if action == 'Forward':
-            if state.get_orientation() == 'UP':
+            if orientation == 'UP':
                 proposed_loc = [x, y + 1]
-            elif state.get_orientation() == 'DOWN':
+            elif orientation == 'DOWN':
                 proposed_loc = [x, y - 1]
-            elif state.get_orientation() == 'LEFT':
+            elif orientation == 'LEFT':
                 proposed_loc = [x - 1, y]
-            elif state.get_orientation() == 'RIGHT':
+            elif orientation == 'RIGHT':
                 proposed_loc = [x + 1, y]
             else:
                 raise Exception('InvalidOrientation')
 
         # Rotate counter-clockwise
         elif action == 'TurnLeft':
-            if state.get_orientation() == 'UP':
-                state.set_orientation('LEFT')
-            elif state.get_orientation() == 'DOWN':
-                state.set_orientation('RIGHT')
-            elif state.get_orientation() == 'LEFT':
-                state.set_orientation('DOWN')
-            elif state.get_orientation() == 'RIGHT':
-                state.set_orientation('UP')
-            else:
-                raise Exception('InvalidOrientation')
+            new_orientation = {'UP': 'LEFT', 'DOWN': 'RIGHT', 'LEFT': 'DOWN', 'RIGHT': 'UP'}[orientation]
 
         # Rotate clockwise
         elif action == 'TurnRight':
-            if state.get_orientation() == 'UP':
-                state.set_orientation('RIGHT')
-            elif state.get_orientation() == 'DOWN':
-                state.set_orientation('LEFT')
-            elif state.get_orientation() == 'LEFT':
-                state.set_orientation('UP')
-            elif state.get_orientation() == 'RIGHT':
-                state.set_orientation('DOWN')
-            else:
-                raise Exception('InvalidOrientation')
+            new_orientation = {'UP': 'RIGHT', 'DOWN': 'LEFT', 'LEFT': 'UP', 'RIGHT': 'DOWN'}[orientation]
 
-        if proposed_loc in self.allowed:
-            state.set_location(proposed_loc[0], [proposed_loc[1]])
+        new_x, new_y = x, y
+        if proposed_loc is not None and proposed_loc in self.allowed:
+            new_x, new_y = proposed_loc[0], proposed_loc[1]
 
-        return state
+        return type(state)(new_x, new_y, new_orientation)
 
     def goal_test(self, state):
-        """ Given a state, return True if state is a goal state or False, otherwise """
-
-        return state.get_location() == tuple(self.goal)
+        """ Return True when the state matches any goal position. The goal is a
+        collection of [x, y] cells or of position objects; for the latter the
+        orientation must match too (e.g. a shooting position). """
+        for goal in self.goal:
+            if hasattr(goal, 'get_location'):
+                if (state.get_location() == goal.get_location() and
+                        state.get_orientation() == goal.get_orientation()):
+                    return True
+            elif list(state.get_location()) == list(goal):
+                return True
+        return False
 
     def h(self, node):
-        """ Return the heuristic value for a given state."""
-
-        # Manhattan Heuristic Function
+        """ Manhattan distance from the node's location to the nearest goal cell. """
         x1, y1 = node.state.get_location()
-        x2, y2 = self.goal
-
-        return abs(x2 - x1) + abs(y2 - y1)
+        distances = []
+        for goal in self.goal:
+            x2, y2 = goal.get_location() if hasattr(goal, 'get_location') else (goal[0], goal[1])
+            distances.append(abs(x2 - x1) + abs(y2 - y1))
+        return min(distances) if distances else 0
 
 
 # ______________________________________________________________________________

tests/test_search.py

@@ -1,5 +1,6 @@
 import pytest
 from search import *
+from logic import WumpusPosition
 
 random.seed("aima-python")
 
@@ -443,5 +444,31 @@ def search(self, problem):
 (['E', 'P', 'R', 'D', 'O', 'A', 'G', 'S', 'T'], 123)
 """
 
+def test_plan_route():
+    dim = 4
+    allowed = [[i, j] for i in range(1, dim + 1) for j in range(1, dim + 1)]
+    start = WumpusPosition(1, 1, 'UP')
+
+    # a route to a goal cell: the planned actions must actually reach it
+    problem = PlanRoute(start, [[3, 3]], allowed, dim)
+    state = start
+    for action in astar_search(problem).solution():
+        state = problem.result(state, action)
+    assert list(state.get_location()) == [3, 3]
+    # the A* search must not mutate the initial state
+    assert start.get_location() == (1, 1) and start.get_orientation() == 'UP'
+
+    # a position goal also constrains the final orientation
+    problem = PlanRoute(start, [WumpusPosition(2, 1, 'RIGHT')], allowed, dim)
+    state = start
+    for action in astar_search(problem).solution():
+        state = problem.result(state, action)
+    assert state.get_location() == (2, 1) and state.get_orientation() == 'RIGHT'
+
+    # forward into a cell that is not allowed (unsafe) leaves the agent in place
+    problem = PlanRoute(start, [[2, 2]], [[1, 1]], dim)
+    assert problem.result(WumpusPosition(1, 1, 'RIGHT'), 'Forward').get_location() == (1, 1)
+
+
 if __name__ == '__main__':
     pytest.main()