Assigned: Feb. 27
Due: Mar. 6
1. P => ~(Q ^ R). 2. R <=> ~(W V X). 3. W => Q 4. X => Q 5. (W^X) => ~Q ^ P 6. W <=> X.
This problem can be compiled into a satisfiability problem using propositional atoms of the following form: Let N be the number of vertices. For each vertex V and number K, let VK be the proposition that V is the Kth vertex in the cycle. For the problem above, since there are 8 vertices, one would define 64 atoms A1, A2 ... H7, H8. The cycle above would correspond to a solution in which A1, H2, E3, C4, B5, G6, D7, and F8 are true and the other 56 atoms are false.
A. You need four kinds of constraints:
B. Actually, you don't need sentences of type 4 above. Explain why, if you've satisfied all the sentences of types 2 and 3, the sentences of type 4 must be true. (You do not have to refer to your propositional encoding to answer this.)
C. (1 point extra credit) Continuing (B), explain further why, though sentences of type 4 may not be necessary, they may be useful for a SAT solver. Give an example where including sentences of type 4 will enable Davis-Putnam to find a solution much more quickly. You do not have to give a complete trace of the running of Davis-Putnam for this case; just explain the example, and explain why adding this constraint will result in a speed-up.
D. (1 point extra credit). If there is a solution, then you can obviously choose any particular vertex to be vertex number 1, since the path is a cycle. So we could, for example, posit that the atom A1 is true. How much more efficient will that make the execution of the Davis-Putnam algorithm, if there is a solution? How much more efficient will it make the execution if there is no solution? (Hint: Think about the first thing that Davis-Putnam does.)