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

a. Draw the constraint graph corresponding to the SAT problem (¬ X₁ ∨ X₂) ∧ (¬ X₂ ∨ X₃) ∧ . . . ∧ (¬ X_n−1 ∨ X_n)
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 to find all solutions to a SAT 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 X₁, . . .,X_n 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 (Section 6.5). Are these two facts connected? Discuss.