General Purpose Heuristics

Unit Preference Strategy

This strategy causes shorter clauses to be selected from the ToBeUsed set in preference to longer clauses.

Example to try using BFS then Unit Preference 
S1 = { ~p(X) | q(X) | r(X),
       p(a) | p(b),
       ~q(Y),
       ~r(X) }

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 below).

Example to try with Unit Preference then Least Symbol Count 
S1 = { p(X) | ~p(f(X))      [5]
       ~p(a)                [2]
       p(S) | q(S)          [4]
       p(T) | ~q(T) }       [4]

Example to try with Unit Preference then Least Symbol Count 
S1 = { 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]

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) }