CS 141 Introduction to AI Greenwald
TBA
10:00 PM, Apr 2, 2009
|
Project 3: Chip’s Challenge Due: |
Contents
![[chips-Z-G-1.gif]](chips-Z-G-1.gif)
|
Chip’s Challenge is an old tile-based puzzle game that was played on early Windows and DOS systems. The game stars Nerdy Chip McCallahan, a young man who dreams of becoming a member of the prestigious Bit Buster Club. In order to gain access to this club, Chip must pass a series of challenging tests to prove that he is, indeed, Bit Buster material. Each of these challenging tests is represented by a level in the game. The player’s goal at each level is simply to navigate Chip to a blue portal (the exit), through which he can advance to the next level, where an even more difficult challenge awaits. However, every level’s portal is blocked by a chip socket that Chip cannot pass through until all the computer chips on the level have been collected. Chip picks up any items he walks over. As he traverses the level collecting chips, Chip may come across different colored locked doors that obstruct his path; these can only be opened by finding a key of the corresponding color. Take a moment to identify the blue portal, chip socket, computer chips, locked doors, keys, and Nerdy Chip McCallahan in the given figure.
1 Planning as Satisfiability
Chip1 faces a planning problem: a problem in which Chip resides at some initial state and wishes to reach some goal state, namely the level’s exit. Our goal is to use logic to solve Chip’s problem, so you will encode his problem in some logical language, like propositional or first-order logic. To do so, you will write down effect axioms that (unsurprisingly) describe the effects of his actions. Such axioms are of the form: if the preconditions that enable an action hold at time t, and the action is taken, then the action’s postconditions hold at time t + 1. For example, if, at time t, Chip walks on a tile in which a computer chip lies, Chip possesses that computer chip at time t + 1. You will also need so-called frame axioms. These axioms describe what does not change with each of Chip’s actions. For example, if Chip possesses chip n at time t, then Chip also possesses chip n at time t + 1, regardless of his action at time t.
Given such axioms, there are two basic approaches to planning. The classic approach is to search for a proof of the existence of a plan. In particular, you can try to prove, using for example a resolution theorem prover, that there exists a sequence of actions that leads from the initial state to the goal state. You will not take this approach here. Instead, you will be taking an approach that has been dubbed planning as satisfiability. That is, you will formulate Chip’s problem as an instance of SAT, and you will implement a satisfiability solver to search for a model of his problem. The hope is that that model will correspond to a valid plan, and it will if you include some additional axioms that rule out spurious models. Specifically, you will need to add axioms that state: if an action is taken, then its preconditions must have been satisfied. (Otherwise, you will find that your SAT solver can return models with no actions, satisfying most axioms vacuously.)
2 Chip’s Knowledge Base
The main intellectual challenge of this project is to formulate the rules of Chip’s Challenge as an instance of SAT in such a way that the only models of your formulation indicate to Chip how to proceed from the start state to the goal. This will likely be an iterative process: your early formulations may admit rather nonsensical models (e.g., plans without any actions), but your later formulations will include additional axioms ruling out any anomalous models.
The rules of Chip’s Challenge can be expressed in first-order logic using predicates like the following:
on(x, y, t) iff Chip is on tile (x, y) at time t
hasKey(c, t) iff Chip has the key of color c at time t
hasChip(n, t) iff Chip has the nth computer chip at time t
move(x1, y1, x2, y2, t) iff Chip moves from (x1, y1) to (x2, y2) at time t (and, hence, Chip arrived at (x2, y2) at time t + 1)
Chip begins on the starting tile (at time 0), and his goal is to reach the exit at time t. Using the above predicates, if the starting tile is (0,0) and the exit is (7,7), we would write:
Now how can Chip move from the starting tile to the exit? If he is on a tile at time t, he can move to an adjacent tile (that is not a wall), so that he is on that adjacent tile at time t + 1:
Of course, he cannot move through a door unless he has the key. Nor can move into a socket without the requisite computer chips. These rules can also be expressed in first-order logic.
Furthermore, these first-order logic predicates and formulas can be converted to variables and formulas of propositional logic. For example, one could restate on(x, y, t) using the propositional variable on_x_y_t. In a similar fashion, one can create a propositional variable hasKey_c_t, representing whether or not Chip has the key of color c at time t. And so on.
3 What to Do
Your mission is to solve Nerdy Chip McCallahan’s planning problem. You must write a program that takes as input a level, and outputs a plan that Chip can follow to complete that level. To do so, you will formulate a description of the problem Chip faces at each level in propositional logic—as an instance of SAT—and you will create a SAT solver to determine how to direct Chip from the starting tile to the level’s exit. In fact, you will formulate each problem multiple times, first in search of a goal in 0 steps, then in 1 step, then 2, and so on, up to some upper bound on the number of steps. More specifically, your tasks include the following:
First, formulate Chip’s Challenge in propositional logic, only taking into account walls and the exit. Make sure your description is in CNF form, and run the given WALKSAT algorithm (incrementally) on your formulation to verify its correctness.
These levels are located in the mazes.dac level set.
Second, extend your formulation to take account of all aspects of Chip’s Challenge relevant in CS 141, namely keys, doors, chips, chip sockets, walls, and the exit. Again, run the given WALKSAT algorithm (incrementally) on your formulation to verify its correctness.
These levels are located in the keysnchips.dac level set.
Third, and finally, implement the DPLL algorithm as an alternative SAT solver to WALKSAT. Record the time to run WALKSAT and DPLL on various levels. Do you observe any noticeable differences?
4 Handing In
Please hand in the following:
All the code necessary to solve the assignment (including our support code).
A README file that includes the following:
Standard bug reports.
Anything that might help us read your code: design quirks, conventions, etc.
Comments that might help us improve this project in the future.
A short report tabulating the results of running DPLL vs. WALKSAT on various levels of Chip’s Challenge.
Hand in by typing cs141_handin chips in the shell from the directory containing your work.
5 Support Code
As usual, install the support code by running the install script:
The support code will be installed into your /course/cs141/projects/ directory.
Much of the support code is for interfacing with Tile World, an open source emulation of the Chip’s Challenge game, and you need not worry about it. The classes you will need to concern yourself with are listed below.
The Frontend class : You do not need to modify this class, but this is where the main method for the project is found. Call the main method to run the project.
The ChipPlanner class : This is where the bulk of your planning work will be done. See the comments in this class’s methods to see what needs to be filled in.
The LevelMap class and the tiles package : The LevelMap class represents a map of a game level. It contains an array of AbstractTiles, the subclasses of which can be found in the tiles package. You do not need to modify any of these classes, but you will need to interact with them when creating your plan.
The sat package : This package contains many classes which are useful for representing SAT problems. Chief among them is SatInstance, which represents a SAT problem in its entirety. A SAT problem is made up of several Clauses and Variables, and a solution to a SAT problem is represented by a Map of Variables to Asgns. Be sure to read over the comments in these classes so you can familiarize yourself with how they are used.
WalkSatSolver and DpllSatSolver : These two classes take as input a SatInstance and solve it, the former using the WalkSAT algorithm and the latter using DPLL. The WalkSatSolver class is filled in for you, and will be useful when testing your planner. You must fill in the DpllSatSolver class as part of the project.
When the main routine in Frontend.java is run, TileWorld will be started. Select a level set using the arrow keys. Every time a new level is started, the frontend will request a solution by calling getPlan in ChipPlanner with the current LevelMap. After your code returns a solution, you can use the frontend’s buttons to execute it either step by step or all at once.
6 Resources
Tile World Home Page:
http://www.muppetlabs.com/~breadbox/software/tworld/Original Planning as Satisfiability Paper:
http://www.cs.rochester.edu/u/kautz/papers/satplan.psFirst Follow-on Paper:
http://www.cs.rochester.edu/u/kautz/papers/plan.psOne of the latest follow-on papers (there are many in between):
http://www.aaai.org/Papers/AAAI/2006/AAAI06-241.pdf
1 More specifically, the player of the game acting on his behalf.