CPSC 420 - Homework #2
due: Mon, Apr 2, 2007

1. [Satisfiability] Use the Davis-Putnam procedure to determine one
   possible coloring of the map below using the propositional
   knowledge base (set of clauses) given below.  Trace the algorithm
   by showing the variable bindings (truth assignments) at each stage.
   Clearly indicate all cases of choice-points and back-tracking.
   Show the final truth assignment of all (9) variables. Show each
   case where you use the unit-clause or pure-symbol heuristics.  The
   knowledge base given below uses propositional symbols like AR, AG,
   and AB to represent that region A is red, green, and blue,
   respectively. '-' means negation, as in '-AR' means 'not AR'.

      -------------------
      |   A             |
      -------------------
      |   B   |    C    |
      -------------------

   KB = { // each region is 1 of 3 possible colors
          AR v AG v AB , 
          BR v BG v BB , 
          CR v CG v CB 
          // each region can only be 1 color at a time
          -AR v -AG , -AR v -AB , -AG v -AB , 
          -BR v -BG , -BR v -BB , -BG v -BB , 
          -CR v -CG , -CR v -CB , -CG v -CB ,
	  // adjacency constaints - neighbors can't be same color
          -AR v -BR , -AG v -BG , -AB v -BB ,
          -AR v -CR , -AG v -CG , -AB v -CB ,
          -BR v -CR , -BG v -CG , -BB v -CB }

2. [Back-chaining] Given the following knowledge base (propositional
   rules), trace the back-chaining procedure for proving the query
   'can_leave' (determining whether it is entailed) in the following cases.

KB:
  have_treasure ^ wumpus_dead -> can_leave
  found_gold -> have_treasure
  found_silver -> have_treasure
  heard_screan -> wumpus_dead
  killed_wumpus -> wumpus_dead
  had_weapon ^ was_near_wumpus -> killed_wumpus
  had_arrows -> had_weapon
  had_gun -> had_weapon

case 1:
  facts = { found_silver, heard_screen, carrying_pack, was_near_wumpus }

case 2: 
  facts = { found_gold, had_gun, was_near_wumpus }

case 3: 
  facts = { found_gold, had_arrows, carrying_water }