Assignment 7
60 points
1. [30 points] Problem 5.4(b). Follow algorithm SAT on slide 13-24. (Ignore the discussion on
terminal MSCS -- slides 13-32 to 13-36 -- that was not covered in class.)
Follow these steps:
(i) List the formulas in the closure of phi.
(ii) List the basic formulas.
(iii) List the atoms.
(iv) Generate the tableau Tphi. DO THIS STEP BEFORE (v).
(v) Generate T(minus)phi by removing all atoms from Tphi that are not reachable from phi-atoms.
(vi) Mark the MSCS in the tableau of (v).
Say which (if any) are transient.
(vii) Is phi satisfiable? If yes, indicate a fulfilling
phi-reachable MSCS. If no, say for each phi-reachable
MSCS (if any) why it is not fulfilling.
2. [30 points] Problem 5.4 (c). Answer the same parts (i)-(vii) as above.