General Purpose Heuristics

Unit Preference Strategy

This strategy causes unit clauses to be selected from the ToBeUsed set in preference to non-unit clauses.

Example, using unit preference 
S1 = { p(b) | r(Y) | p(Y),
       ~p(S) | p(b),
       ~p(b),
       ~r(a),
       ~r(c) }

~p(b) is the ChosenClause
~r(a) is the ChosenClause
~r(c) is the ChosenClause
~p(S) | p(b) is the ChosenClause
+ ~p(b) » ~p(S)
~p(S) is the ChosenClause
+ ~p(S) | p(b) » ~p(S) (loop)
p(b) | r(Y) | p(Y) is the ChosenClause
+ ~p(b) » r(Y) | p(Y)
p(b) | r(b)
r(b)
+ ~r(a) » p(b) | p(a)
+ ~r(c) » p(b) | p(c)
+ ~p(S) | p(b) » p(b) | r(Y) | p(Y) (loop)
p(b) | r(Y) | p(b)
r(b) | p(b) (loop)
+ ~p(S) » r(Y) | p(Y) (loop)
r(b) is the ChosenClause
r(Y) | p(Y) is the ChosenClause
+ ~p(b) » r(b) (loop)
+ ~r(a) » p(a)
+ ~r(c) » p(c)
+ ~p(S) | p(b) » r(Y) | p(b)
+ ~p(S) » r(Y)
p(a) is the ChosenClause
+ ~p(S) | p(b) » p(b)
+ ~p(S) » FALSE

Least Symbol Count

This strategy selects the clause with the least number of symbols from the ToBeUsed set. This improves on unit preference, because it prevents the derivation of a stream of short clauses with ever increasing term depth (as happens with the example S10 below).

Example, using least symbol count 
S10 = { p(X) | ~p(f(X))      [5]
        ~p(a)                [2]
        p(S) | q(S) | r(S)   [6]
        ~q(T) | p(a)         [4]
        ~r(T) | p(a) }       [4]

~p(a) is the ChosenClause
~q(T) | p(a) is the ChosenClause
+ ~p(a) » ~q(T) [2]
~q(T) is the ChosenClause
~r(T) | p(a) is the ChosenClause
+ ~p(a) » ~r(T) [2]
~r(T) is the ChosenClause
p(X) | ~p(f(X)) is the ChosenClause
+ ~p(a) » ~p(f(a)) [3]
~p(f(a)) is the ChosenClause
+ p(X) | ~p(f(X)) » ~p(f(f(a))) [4]
~p(f(f(a))) is the ChosenClause
+ p(X) | ~p(f(X)) » ~p(f(f(f(a)))) [5]
~p(f(f(f(a)))) is the ChosenClause
+ p(X) | ~p(f(X)) » ~p(f(f(f(f(a))))) [6]
p(S) | q(S) | r(S) is the ChosenClause
+ ~p(a) » q(a) | r(a) [4]
+ ~q(T) » p(S) | r(S) [4]
q(a) | r(a) is the ChosenClause
+ ~q(T) » r(a) [2]
r(a) is the ChosenClause
+ ~r(T) » FALSE

Exam Style Questions

  1. Show the execution of the ANL loop with unit preference to derive the empty clause from: 
    S = { ~r(Y) | ~p(Y),
      p(b),
      r(a), 
      p(S) | ~p(b) | ~r(S),
      r(c) }
    Number the chosen clause at each iteration.

  2. Show the execution of the ANL loop with unit preference to derive the empty clause from: 
    S = { ~p(b),
      p(X) | l(X) | q,
      ~q | l(Y),
      ~l(Z) | r(Z),
      ~r(b) | ~l(T) }
  3. Show the execution of the ANL loop with least symbol count to derive the empty clause from: 
    S = { p(X) | ~p(f(X))
      ~p(a)
      p(S) | q(S) | r(S)
      ~q(T) | p(a)
      ~r(T) | p(a) }