Soovitusi Otteri otsingu suunamiseks

Põhistrateegia valik

• hyperres ilma goal-directed searchita, kui on horni lähedased reeglid: set(hyper_res).
• binary res koos goal-directed searchiga (kasuta sos ja usable): set(binary_res).
• binary res ilma goal-directed searchita, aga lisapiirangutega: set(binary_res) ja vaata lisaks.
  • üks eeldus peab olema unit
  • mingi spetsiifiline literaalide järjestus, kus tohib kasutada ainult järjestuse mõttes suuremaid disjunkte

Alati ka:

set(factor).

Given ratio valik

• N korda vali kõige väiksem disjunkt
• 1 kord vali queuest

Enamasti on mõistlik panna ratio ca 4: assign(pick_given_ratio,4).

Piirangud järeldatavatele disjunktidele

• piirame ära sügavuse (saab teha weight templatede abil).
• piirame ära literaalide arvu disjunktis, a la assign(max_literals,3).
• piirame ära disjunkti elementide koguarvu (weight), a la assign(max_weight,13).

Splittimine

Vaatame, kas saab ülesande splittida alamülesanneteks a la p(a) | p(b)

Siis teeme kaks eraldi tõestuseotsingut p(a) ja p(b) jaoks.

Võrduse orienteerimine

Võrduse juures on võimalik määrata, kuidas orienteeritakse võrdusi (otteril lex parameeter) a la kas orienteerida f(x)=g(x)

• f(x)->g(x) või
• g(x)->f(x)