Exercise 7.19

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

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

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

  3. Suppose we apply {Backtracking-Search} (page backtracking-search-algorithm) 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$.)

  4. 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 csp-structure-section). Are these two facts connected? Discuss.

View Answer