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

Draw the constraint graph corresponding to the SAT problem for the particular case $n5$.

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

Suppose we apply {BacktrackingSearch} (page backtrackingsearchalgorithm) 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_1,\ldots,X_n$ and ${false}$ is ordered before ${true}$. How much time will the algorithm take to terminate? (Write an $O(\cdot)$ expression as a function of $n$.)

We know that SAT problems in Horn form can be solved in linear time by forward chaining (unit propagation). We also know that every treestructured binary CSP with discrete, finite domains can be solved in time linear in the number of variables (Section cspstructuresection). Are these two facts connected? Discuss.