CSC244 / CSC444 - Assignment #2 - Part 2 DUE: 5PM, Friday, October 20th, 2006 TURNIN: Please email the following to ardis@cs.rochester.edu : + 1 LISP file (a2.lisp) containing all function and structure definitions used to solve the assignment problems. + 1 text file (a2_usage.txt) containing a text log of using your defined functions/structures to solve the assignment problems. Please include all code usage which you believe helps show the correct behavior of your provided LISP code. + 1 text file (a2_readme.txt) containing a brief description of all defined functions/structures including their intended purpose, input/output, etc. Please indicate here if your code has any problems/incapatabilities/failures, as well as any improvements for efficiency or robustness, for purposes of partial credit and/or extra credit. Your email should have the subject line "CSC244 Assignment 2" if you are in CSC244 and "CSC444 Assignment 2" if you are in CSC444. Multiple submissions are allowed, but only the most recent submission (prior to the deadline) will be graded. Please put your name at the top of your submission email. Late submissions will be accepted for 2 days with a 10% penalty per day. All submissions after October 22nd will not be graded. PROBLEM: *** SATISFIABILITY *** You are to implement a function named "sat" which takes as its input a single parameter which is a list. This list will have lists as its elements, each of which will contain zero or more symbols and/or negated symbols (P, Q, NOT R, etc.) representing propositional facts. Example input: ((P Q) (NOT Q R) (NOT R S)) (() (P) (NOT R NOT S)) The sublists are treated as disjunction, and the main list is treated as conjunction. Thus, the input "((P Q) (NOT Q R))" is logically equivalent to "(P v Q) ^ (~Q v R)". Your task is to determine satisfiability of the input by implementing the Davis-Putnam procedure as described in the text on pages 77 and 78. CSC244: Please choose (from the list on p.78) one method for determining the next atom attempted, implement this method in your function, and mention this choice in your a2_readme.txt file. CSC444: Please choose (from the list on p.78) at least two methods for determining the next atom attempted, implement both in your function, and provide an optional parameter to "sat" which determines the method used. For instance, "(sat '((P)) 1)" would use your first method, while "(sat '((P)) 2)" would use your second. You should mention the exact usage of this parameter in your a2_readme.txt file. If the optional parameter is not set, your function should use your first method. In addition, please briefly explain (again in the same file) one method which is not listed which may provide a good selection strategy. You do not need to implement this method, but should describe concisely how it might be used. Below is a list of sample input and output for your reference. IN: ((P) (NOT P Q)) OUT: T IN: ((P) (NOT P)) OUT: NIL IN: ((NOT P Q) (NOT Q R) (NOT R S) (NOT S)) OUT: T IN: ((P) (NOT P Q) (NOT Q R) (NOT R S) (NOT S)) OUT: NIL When describing your usage (in a2_usage.txt), please include at least one case which uses ten or more unique literals. CONTEST: The student with the most efficient "sat" function (in terms of execution time for a set of challenging satisfiability problems) will receive a prize! Good luck!