CSCI-UA.0472 Programming Assignment 2: Davis-Putnam algorithm
Programming Assignment 2
Overview
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 maximum number of steps. If a player goes to a node, then they get all the treasures at that node. The object is to find a path through the maze starting at START in at most the given number of steps that collects all the different types of treasure.
Example: Suppose that the maze is as follows:
Then the path "START, C, G, H" succeeds in collecting all three types of treasure in 3 steps. The path "START, A, D, C, F" succeeds in 4 steps.
You may assume that START has no treasure. The player is only required to get one of each type of treasure.
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 (2) and translates it into a solution to the original problem.
Compiling the maze puzzle to propositional logic
The MAZE puzzle can be expressed propositionally as follows: There are two kinds of atoms:
- 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. (Note: in propositional logic, a construction like "At(C,2)" is considered a single symbol of 7 characters. The parentheses and comma are not punctuation, they are just characters in the symbol, to make it easier for the human reader.)
- Has(T,I) means that the player is in possession of treasure T at time I. For example, Has(Gold,3) means that the player has the gold at time 3.
If there is a maximum of K steps, then for each time I=0 ... K, there should be an atom At(N,I) for each node N, and an atom Has(T,I) for each treasure T.
There are 7 categories of propositions.
-
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)). In CNF this becomes ¬At(M,I) ∨ ¬At(N,I). For example, ¬At(C,2) ∨ ¬At(F,2).
-
The player must move on edges. Suppose that node N is connected to M1 ... Mq. For any time I, if the player is at node N at time I, then the player moves to M1 or to M2 ... or to Mq at time I+1. Thus At(N,I) → At(M1,I+1) ∨ ... ∨ At(Mq,I+1). In CNF, ¬At(N,I) ∨ At(M1,I+1) ∨... ∨ At(Mk,I+1). For example, ¬At(C,2) ∨ At(START,3) ∨ At(D,3) ∨ At(F,3) ∨ At(G,3)
-
Suppose that treasure T is located at node N. Then if the player is at N at time I, then at time I the player has T. At(N,I) → Has(T,I). In CNF, ¬At(N,I) ∨ Has(T,I).
For example ¬At(C,2) ∨ Has(Ruby,2)
-
If the player has treasure T at time I-1, then the player has T at time I. (I=1..K) Has(T,I-1) → Has(T,I) In CNF, ¬Has(T,I-1) ∨ Has(T,I) For example ¬Has(GOLD,2) ∨ Has(GOLD,3).
-
Let M1 ... Mq be the nodes that supply treasure T. If the player does not have treasure T at time I-1 and has T at time I, then at time I they must be at one of the nodes M1 ... Mq. [¬Has(T,I-1) ∧Has(T,I)] → At(M1,I) ∨ At(M2,I) ∨ ... ∨At(Mq,I). In CNF Has(T,I-1) ∨ ¬Has(T,I) ∨ At(M1,I) ∨ At(M2,I) ∨ ... ∨At(Mq,I). For example Has(GOLD,1) ∨ ¬Has(GOLD,2) ∨ At(A,2) ∨ At(H,2).
-
The player is at START at time 0. At(START,0).
-
At time 0, the player has none of the treasures. For each treasure T, ¬Has(T,0). For instance: ¬Has(GOLD,0).
-
At time K, the player has all the treasures. For each treasure T, Has(T,K). For instance: Has(GOLD,4).
In the theory of logic-based planning, axioms such as 1 which characterize what conditions can hold at a single time, are called "domain constraints". Axioms such as 2 which characterize what states can follow one another are called "feasibility axioms" or "precondition axioms"; the form of these here is a little unusual since we aren't explicitly representing action. Axioms such as 3 which characterize what changes between successive states are called "causal axioms". Axioms such as 4,5 which characterize what remains unchanged between successive states are called "frame axioms". Axioms 6 and 7 is initial conditions and axiom 8 is a goal condition.
Specifications
Input / Output.
All three programs take their input from a text file and produce their output to a text file. (If you want, you may use standard input and output.)
Davis-Putnam
The input to the Davis-Putnam procedure has the following form: An atom is denoted by a natural number: 1,2,3 ... The literal P is the same number as atom P; the literal ¬P is the negative. A clause is a line of text containing the integers of the corresponding literals. After all the clauses have been given, the next line is the single value 0; anything further in the file is ignored in the execution of the procedure and reproduced at the end of the output file. (This is the mechanism we will use to allow the front end to communicate to the back end.) 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 ∨ Q ∨ R. ¬Q∨ 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 Maze program. And it must be easy for the grader, without editing your code, to run the Davis-Putnam code separately.
Front end
The front end takes as input a specification of a maze and a problem and generates as output a set of clauses to be satisfied.
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.
- Remaining lines: The encoding of the maze. Each line consists
- A node N.
- The keyword "TREASURES" followed by the list of treasures, separated by white space.
- The keyword "NEXT" followed by the list of nodes that N is connected to, separated by white space.
Thus, the above maze, with a maximum of 5 steps,
START A B C D E F G H GOLD WAND RUBY 5 START TREASURES NEXT A C
A TREASURES GOLD NEXT START B D B TREASURES RUBY NEXT A D E C TREASURES RUBY NEXT START D F G D TREASURES NEXT A B C E G E TREASURES NEXT B D H F TREASURES WAND NEXT C G G TREASURES NEXT C D F H H TREASURES GOLD WAND NEXT G
You may assume that the input is correctly formatted. You do not have to do any error checking on the input.
The output consists of
- 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.
- 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"
Back-end
The back end takes as input the output that Davis-Putnam generates when run on the output of the front end. It generates as output the path that solves the problem. If the input indicates that the clauses have no solution, the back end should output the message "NO SOLUTION".
Another example for Davis-Putnam
The following is the input-output pair just for the Davis-Putnam module --- not the front and back ends --- corresponding to the example in the class notes. Input for Davis-Putnam Output from Davis-Putnam
A Simpler Maze Example
It would probably be a mistake to begin your testing using the above example, with its 70+ propositional atoms and hundreds of propositions. Rather, I would suggest that you start by working on the following maze with a search limit of 3.
Input for the front end for this small maze Clauses for this small maze in symbolic form. Output from front end for this small maze Output from Davis-Putnam for this small maze The output from the back end should be just START A START B or START B START A.
Deliverable You should submit to BrightSpace (a) the source code; (b) instructions for running it, if there's anything at all non-obvious about it. Nothing else.
