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.