CS447 Lecture 1: L16.pdf
Document Summary
So, in general, we can"t evaluate every value of every clause, because there are too many of them. The next best thing is to focus on each clause and make sure it a ects the predicate. That is, we"ll test each clause while it is active. Consider the following clause: p = x y (z w) Let"s say that we focus on y; we"ll call it the major clause. (we may designate any clause as a major clause at our whim. ) We want to make y determine p with certain minor clause values. That is: if we set y to true, then p evaluates to some value x, if we set y to false, then p must evaluate to x. The truth assignment: x = z = w = will make y determine p; in particular, y true makes p true and t false makes p false.
