CSCE 625
Homework #7
due: Wed, Nov 30

1. Using Situation Calculus, write axioms to describe the act of buying something. You have to have enough money (more than the cost of them item). Afterwards, you own it but, you have less money. Also, add a frame axiom to capture the fact that buying something doesn't change whether you own other things.

Prove (using back-chaining and unification in first-order logic) that after you buy a coke and some popcorn, you will have a coke and some popcorn (assuming they each cost $1, and you initially have $2).

2. Suppose you are at home and you want to fix a cabinet and make some stir fry for dinner. You have vegetables but you need to get some chicken from the grocery store for the stir fry. To fix the cabinet, you need to buy a hammer and some nails at the hardware store. To buy things things, you need money, for which you will have to go the bank. Show how you can make a partial-order plan to achieve all these things. List your operators in PDDL notation. Describe the order in which nodes and edges are added to the graph, and indicate when ordering links (promotion or demotion) are added to resolve threats. You don't have to worry about back-tracking; you may omnisciently choose the right node to add at each stage. Finally, list all possible sequences of actions consistent with your plan. (In this problem, the main issue to focus on is your location; after you get money, assume you have enough for all purchases - you don't need to track the amount).

3. Consider two friends, Raj and Kreshna, who are about to graduate from college. Each wants to send a picture of themselves and their diplomas to their parents. Raj's parents have a computer with a printer. So he plans to take the picture of himself with his cell phone (a digital phone, which creates an image as a file), download it to his PC, and then scan his diploma and email them to his parent to print out. Kreshna's parents don't have a computer. Therefore, he plans to take his picture with a film-based camera, develop it (from which he will get a print), make a copy of his diploma with a photo-copier (since he wants to keep the orignal), and mail them to his parent using the postal service.

Describe the actions in this domain using PDDL. You will have to find a way of keeping track of where an image is (whose device is it on?), what an image is 'of', and what media/format it is in. (e.g. paper vs. file). Some actions like sending something via postal mail send a physical object, which the sender no longer has. Other actions like printing or scanning make additional copies of an object.

(further things to consider adding: faxes, high- vs. low-resolution)
(these would be interesting extensions, but you don't have to include them)

In the end, you should to able to prove that each set of parents get to see pictures (physical ones) of their graduates and their diplomas. Do this using goal regression.

4. Implement the Flat Tire problem (p. 370) in the book in SatPlan. Propositionalize the problem description. Then use a satisfiability solver to generate a model and show that it encodes the correct sequence of actions to achieve the goal from the initial state.

For a satisfiability solver, you can use zchaff, which is based on DPLL. You will have to download and compile it on a unix system. The input format is ".cnf" files. To convert a set of propositional sentence into this file format, I am providing you a python script.