Due: Oct. 26

In this assignment, you are to implement the Davis-Putnam algorithm and use it to solve a simple form of an adventure game.

The puzzle is as follows: You are given (1) a maze with treasures at particular nodes; (2) a list of treasures to get; (3) a maximum number of steps. The object is to find a path through the maze that collects all these treasures in at most the given number of steps.

Example: Suppose that the maze is as follows:

If the task is "GOLD, RUBY" in 2 steps, then a solution is "START, C, F". If the task is "GOLD, WAND, RUBY" in 4 steps, then a solution is "START,C,D,C,F". If the task is "GOLD,RING" in two steps, then there is no solution.

You will write three programs.

- An implementation of the Davis-Putnam procedure, which takes as input a set of clauses and outputs either a satisfying valuation, or a statement that the clauses cannot be satisfied.
- A front end, which takes as input a maze problem and outputs a set of clauses that can be input to (1).
- A back end, which takes as input the output of (1) and translates it into a solution to the original problem.

- AT_N_I means that the player is on node N at time I. For instance AT_C_2 means that the player is on node C at time 2. If there is a maximum of K steps, then there should be one such atom for each node N and each time I=0 .. K.
- HAS_T_I means that the player has gotten treasure T at time I. For example, HAS_GOLD_3 means that the player has gotten the gold by step 3. If there is a maximum of K steps, there should be 1 such atom HAS_T_I for each treasure T and each I=0 ... K.

- The player is only at one place at a time. For any time I, for any
two distinct nodes M and N, ~(AT_M_I ^ AT_N_I), or in CNF
~AT_M_I V ~AT_N_I.

For example, ~AT_C_2 V ~AT_F_2. - The player must move on edges. Suppose that node N is connected to
M1 ... Mk. For any time I, if the player is
at node N at time I, then the
player either remains at N or moves to M1 or to M2 ... at time I+1.

Thus AT_N_I => AT_N_(I+1) V AT_M1_(I+1) V ... V AT_Mk_(I+1);

in CNF, ~AT_N_I V AT_N_(I+1) V AT_M1_(I+1) V ... V AT_Mk_(I+1).

For example, ~AT_C_2 V AT_C_3 V AT_START_3 V AT_D_3 V AT_F_3 - Suppose that treasure T is at node N.
If the player is on node N at time I, then
the player has T at time I. AT_N_I => HAS_T_I, or in CNF
~AT_N_I V HAS_T_I.

For instance, ~AT_F_3 V HAS_RUBY_3. - If the player has treasure T at time I, then he has treasure T at time I+1, then he has treasure T at time I+1. HAS_T_I => HAS_T_(I+1), or in CNF, ~HAS_T_I V HAS_T_(I+1). For example, ~HAS_GOLD_3 V HAS_GOLD_4.
- Suppose that treasure T is located at nodes N1, N2 ... Nk.
If the player does not have treasure T at time I-1, and does have treasure
T at time I, then at time I he must be either at N1 or at N2 ... or at Nk.

[~HAS_T_(I-1)] ^ HAS_T_(I+1)] => AT_N1_I V AT_N2_I V ... V AT_Nk_T

In CNF, HAS_T_(I-1)] V ~HAS_T_(I+1) V AT_N1_I V AT_N2_I V ... V AT_Nk_T

For example, HAS_GOLD_2 V ~HAS_GOLD_3 V AT_B_3 V AT_C_3. - The player is at START at time 0. AT_START_0.
- If T is a treasure that is not at START, then the player does not
have T at time 0.
If the treasures not at START are T1 ... Tk
then we have ~HAS_T1_0 ^ ~HAS_T2_0 ^ ... ^ ~HAS_Tk_0;

In CNF this is the separate clauses:~HAS_T1_0.

For instance, in the example problem we have

~HAS_T2_0.

...

~HAS_Tk_0.~HAS_GOLD_0.

~HAS_RUBY_0.

~HAS_WAND_0.

~HAS_RING_0.

- At the time limit, the player has all the required treasures. For
instance, in the first problem above, we have
HAS_GOLD_2.

HAS_RUBY_2.

The output from the Davis-Putnam procedure has the following form: First, a list of pairs of atom (a natural number) and truth value (either T or F). Second, a line containing the single value 0. Third, the back matter from the input file, reproduced.

Example: Given the input

1 2 3 -2 3 -3 0 This is a simple example with 3 clauses and 3 atoms.Davis-Putnam will generate the output

1 T 2 F 3 F 0 This is a simple example with 3 clauses and 3 atoms.This corresponds to the clauses

P V Q V R. ~Q V R. ~R.

If the clauses have no solution, then Davis-Putnam outputs a single line containing a 0, followed by the back-matter in the input file.

Note: Your implementation of Davis-Putnam must work on _any_ set of clauses, not just those that are generated by the EXACT SET COVER program.

You may assume that there are no more than 1000 atoms and no more than 10,000 clauses.

The format of the input contains the following elements:

- First line: A list of the nodes, separated by white space. Each node is a string of up to five characters.
- Second line: A list of the treasures, separated by white space. Each treasure is a string of up to ten characters.
- Third line; The number of allowed steps and the list of the treasures to be gotten, separated by white space.
- Remaining lines: The encoding of the maze. Each line consists
of the following parts
- A node N.
- The treasure at node N, or "NONE" if none.
- The nodes connected to N, separated by white space.

START A B C D E F G H GOLD WAND RUBY RING 2 GOLD RUBY START NONE A C A NONE START B D B GOLD A D E C GOLD START D F D WAND A B C E E GOLD B D G H F RUBY C G G NONE E F H H RING E GYou may assume that the input is correctly formatted. You do not have to do any error checking on the input. The output consists of

- 1. A set of clauses suitable for inputting to Davis-Putnam as described above. Note that these constraints are already in clausal form (CNF) and therefore you do not have to implement a program to translate arbitrary Boolean formulas to CNF.
- 2. A key to allow the back end to translate the numbers used for propositional atoms in the clauses into the correct path. The format of this is up to you. My suggestion would be that, for each atom AT_N_I, you have a line of the form "proposition-number N I"

The clauses for the first of these is shown here