RESOLUTION STRATEGIES 1. Simplification Strategies 2. Unit Preference: Complete 3. AF (Ancestry-Filtered) Form Strategy: Complete 4. Set of Support Strategy: Complete 5. Unit Strategy: Complete only for Horn clauses (those with at most one positive literals) 6. (Linear) Input Strategy: Complete only for Horn clauses 7. Ordered Resolution Strategy: Complete only for Horn clauses. Simplification Strategies a. Elimination of Tautologies Any clause containing a literal and its negation may be eliminated since any unsatisfiable set containing such a tautology is still unsatisfiable after removing it. Examples: P(S) + B(X) + ~B(X) P(X) + ~P(X) // P(X) + ~P(Y) is NOT a tautology b. Elimination of Subsumption A clause C1 subsumes another C2 if there is a substitution k such that C1 k <= C2, i.e., after applying the substitution to C1, C1 contains all literals of C2 and possibly some more. P(X) subsumes P(a) P(X) subsumes P(Y) + Q(Y) P(Y) subsumes P(X) + ~Q(Z) c. Elimination of Pure-Literals A literal of a clause is pure iff it has no complementary instance in Other clauses in the set S of clauses. A clause that contains a pure literal is useless for the purpose of Refutation since the literal can never be resolved away. P(X) + Q(Y): P(X) is pure for this set of four clauses. ~Q(Z) + R(Z) ~R(U) + S(U) ~S(V) + R(W) UNIT PREFERENCE STRATEGY 1. This strategy does not rule out any possible pair of clauses that can be resolved. Hence, it is complete. 2. This simply sets an order of selecting pairs of clauses to resolve such that a. a unit clause and another, and then b. a unit and a doubleton, and then c. a doubleton and a double, and so forth. 3. In order to prevent the refutation search from running away along some unprofitable chain of endless unit resolutions, it is often necessary to set a LEVEL BOUND such that only within this set level bound, unit resolutions will be attempted. UNIT STRATEGY: Incomplete This requires that at least one clause to be resolved must be a unit clause. Counterexample: P(X)+Q(X) ~P(Y)+Q(Y) P(Z)+~Q(Z) ~P(U)+~Q(U) INPUT STRATEGY: Incomplete This requires that at least one clause to be resolved must be an input clause. Hence, after the first resolution of two input clauses, we must keep resolving the previous resolvent just obtained. The refutation tree will look like a VINE, a special case of AF Form strategy. The same counterexample above shows that it is NOT complete. Ordered Resolution Strategy: Complete for Horn clauses. 1. Each clause is treated as a linearly ordered set of literals. 2. Resolution is permitted only on the first literal of the clause. 3. Literals in a resolvent preserve the order from their parent clauses with literals from positive parent followed by literals from the negative parent. Example: 1: P+Q 2: ~P+R 3: ~Q+R 4: ~R ---------- 5: Q+R (but not R+Q) :from 1 and 2 6: R :from 3 and 5 7: Nil :from 4 and 6 ---------- In this case, the following two are not to be resolved: a. 1 and 3 b. 2 and 4 c. 3 and 4 AF Form Strategy Criteria for resolving two clauses. a. At least one must be an Input (or Base) clause. A clause is an Input clause if it is one of those we have in the initial set of clauses obtained from all premises and the negated conclusion. b. Or (that is, if neither is an Input clause) one must be an ancestor (not necessarily immediate) of the other. KEY to this strategy: Choosing a top clause (i.e., the first two clauses being resolved) as this strategy is complete provided a clause is selected as a TOP node that is included any refutation graph for the set S of clauses we have. A TOP node in a refutation graph is a node such that every node in the graph is either an input clause or else a descendant of this TOP node. Example. 1: Q(X) + P(X) 2: ~Q(Y) + P(Y) 3: ~Q(Z) + ~P(Z) 4: Q(U) + ~P(U) 1 2 \ / \ / P(Y) 3 | \ / | \ / | ~Q(Z) 4 | \ / | \ / | ~P(U) | / | / NIL SET OF SUPPORT STRATEGY: Complete as it is a general case of AF FORM once a TOP node is selected appropriately Definition: A subset P of a set S of clauses is called "A Set of Support" iff S-P is satisfiable. This strategy is based upon the selection of a set P of support. Criterion for selecting two clauses to resolve: Given a set P of support, at least one of them must be from the set P as each resolvent is included to the set P. The key to this strategy: Selecting this set of support. Usually, we can take those clauses obtained from negated conclusion as this set of support.