Complete your implementation of the resolution algorithm from Lab 7. You may copy your lab code to a new file ‘resolve_hw2.py’.
Problem 1: In the lab, you used the following set of clauses,
CLS = [[‘notP’, ‘notQ’, ‘R’], [‘P’, ‘R’], [‘Q’, ‘R’], [‘notR’]]
and resolution should find that it is contradictory. The algorithm should eventually produce an empty clause [] and terminate with the message that the set of clauses is UNSATISFIABLE. If necessary, complete Lab 7. Then continue with the below.
The given algorithm, when properly implemented, also handles the case where the set of clauses is not contradictory. Demonstrate this as follows:
Let CLS_SAT be a copy of CLS with one small modification that makes CLS_SAT satisfiable (= no longer contradictory).
Run resolve for CLS_SAT and show that it will report SATISFIBILITY of the set of clauses.
Problem 2: Manually apply CNF conversion to the H2CO3 example form the lecture. Cast the resulting clauses into a Python list representation analogous to CLS and CLS_SAT.
Add to your list of clauses one more clause [notH2CO3]. The run the resolve function -- you should be able to arrive at a clauses [ ], indicative that the set of clauses is unsatisfiable. The meaning of that – and why this is exactly the result we want – will be explained in the upcoming lectures.
Hand in: (1) Hardcopy of your file resolve_hw2.py with completed code form Lab7, and two additional lists of clauses CLS_SAT and CLS_H2CO3. (2) A script file that shows your successful loading of module resolve_hw2.py and 3 runs: resolve(CLS), resolve(CLS_SAT), and resolve(CLS_H2CO3).
