Problem set 5

Assigned: Feb. 27
Due: Mar. 6

Problem 1

Translate the following sentences into CNF: (Note: ~X is "not X".)
1. P => ~(Q ^ R).
2. R  <=> ~(W V X).
3. W => Q
4. X => Q
5. (W^X) => ~Q ^ P
6. W <=> X.

Problem 2

Show a trace of the running of the Davis-Putnam algorithm on the clauses that you have derived in problem 1 (the set of all the clauses combined). When you come to a choice point, choose the first unbound symbols in alphabetical order, and try the assignment to TRUE before the assignment to FALSE.

Problem 3

As discussed earlier in class, the HAMILTONIAN CYCLE problem is as follows: You are given a directed graph G. You want to find a cycle of edges in G that contains every vertex exactly once. For instance in the graph below, one Hamiltonian cycle is the path A-->H-->E-->C-->B-->G-->D-->F-->A.

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:

Explain how each of these kinds of constraints can be expressed as a set of sentences in propositional logic. Note that you may need a lot of sentences in some cases, or some fairly long sentences, but you should not have exponentially many sentences or sentences that are exponentially long. Illustrate each of the kinds of sentences with two specific sentences from the above example.

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.)