Homework Assignment 3
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:
a. Let CLS_SAT be a copy of CLS with one small modification that makes CLS_SAT satisfiable
(= no longer contradictory).
b. 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).
