Chaining, unit propagation, and resolution. Recall that the unit propagation inference rule is: given KB containing clauses C_1; : : : ;C_k and a partial assignment if some C{_-i | j } consists of a single literal L, add x_i = b such that L(b) = 1 to . Note that any x_2 element {0; 1}^n satisfying KB that is consistent with p must also have x_i = b. Unit propagation is a particularly ecient inference rule used by SAT-solvers.

Conversely, show that if there is a treelike resolution refutation of KB using clause bspace 2, then unit propagation starting from the empty partial assignment will lead to a refutation. (So actually, unit propagation is equivalent to treelike clause space 2 resolution.)