In this assignment, you'll be using propositional logic and a stochastic solver to solve a murder mystery that has stumped the best minds of Scotland Yard. Your task will be to encode a sequence of clues in propositional logic, convert the statements into CNF form and then use a walksat like program to try to find a satisfying assignment for this CNF. If you find an assignment for a given suspect, you will know you that this suspect could have committed the murder.
Question #1: The first step of this task is to convert the following clues to proposition logic. Please use ^ for and, v for or, ~ for not and => for implies. Use the following atomic sentences:
Jeeves = "Jeeves committed the murder"
Lurch = "Lurch committed the murder"
Alfred = "Alfred committed the murder"
pantry = "Murder occured in the pantry"
bedroom = "Murder occured in bedroom"
gun = "the gun was used in the murder"
icepick = "the icepick was used in the murder":
Here are the clues
a) Jeeves or Lurch or Alfred committed the murder.
b) Either the murder occured in the pantry or in the bedroom (but not both)
c) Either the gun was used or the icepick was used as the murder weapon(but not both)
d) If the murder was committed with a gun then Lurch is a murderer
e) Either Lurch was a murderer or it was committed in the bedroom
(but not both)
f) if the murder was done with the gun then either Jeeves was a
murderer or it was done in the bedroom(but not both)
g) Sally lied when saying "If the room is the bedroom then Alfred is a
murderer"
Question #2: Now convert the logic statements from Question #1 to conjunctive normal form. I.e. sequences of or's that are and'ed together.
Question #3 (programming): Fill in the functions for the Gsat framework given here to get a probabilistic sat solver. The above is a link to a directory with three files. You will be using the files Assignment.java and VarRec.java as is. All of your work will be in filling in the function getSatAssign in Formula.java (and adding the other functions needed to implement getSatAssign. Comments in Formula.java will give more information about the specifications for the Gsat algorithm. The given framework handles all of the I/O functions. Please do not change this framework in your solution.
Question #4: Use the solver above to determine who committed the crime. Is there any one person whom the evidence does not rule out? Can you be sure that one of the other people wasn't involved? How can you use an incomplete method (like walksat) to rule out an individual? Can you add an additional clause or clauses? If so, do so. If not, explain why not as succinctly as possible.
How to turn in the assignment: Create an ascii email message with your answers to questions 1,2 and 4. At the end of this message, append the text for your completed Formula.java file. Do not include the Assignment.java and VarRec.java files you used. Email this message(with the answers to the questions AND the completed Formula.java file) to saia@cs.washington.edu.
Please do not compress or use mime or other attachments in this email. Please squelch any creative impulses for exploiting email technology and just send a very low tech, ascii email with the above specifications.