15 This question considers representing satisfiability (SAT) problems as CSPs.

a. Draw the constraint graph corresponding to the SAT problem

(￢X1 ∨ X2) ∧ (￢X2 ∨ X3) ∧ . . . ∧ (￢Xn−1 ∨ Xn)

for the particular case n=5.

b. How many solutions are there for this general SAT problem as a function of n?

c. Suppose we apply BACKTRACKING-SEARCH CSP of the type given in (a). (To find all solutions to a CSP, we simply modify the basic algorithm so it continues searching after each solution is found.) Assume that variables are ordered X1, . . . ,Xn and false is ordered before true. How much time will the algorithm take to terminate? (Write an O(・) expression as a function of n.)

d. We know that SAT problems in Horn form can be solved in linear time by forward chaining (unit propagation). We also know that every tree-structured binary CSP with discrete, finite domains can be solved in time linear in the number of variables.

Are these two facts connected? Discuss.