Эвристики поиска в дереве
Использование эвристики может привести к тому, что доказательство не будет найдено, хотя оно и существует. Однако она может значительно ускорить работу модифицированного метода поиска в глубину. В области доказательства имеется много эвристик. Обсудим некоторые из них:
А. Стратегия отбрасывания.
Говорят, что упорядоченный дизъюнкт С1 поглощает другой упорядоченный дизъюнкт С2, если дизъюнкт, состоящий из необрамленных литер в С1, поглощает дизъюнкт, состоящий из необрамленных литер в С2.
Упорядоченный дизъюнкт называется тавтологией, если он содержит контрарную пару необрамленных литер.
В модифицированном методе поиска в глубину в конце шага 4 нужно проверить, является ли Ri* (i=1,…,m) тавтологией. Если Ri* – тавтология, то отбрасываем его. Кроме того, следует отбросить Ri*, если в CLIST имеется пара (С,В) такая, что Ri* поглощается дизъюнктом С.
В. Стратегия предпочтения кратчайших дизъюнктов.
Эта стратегия вводит в модифицированный метод поиска в глубину упорядочение пар (С,В) в CLIST, чтобы лучшие пары стояли первыми. Оценивать пары рекомендуется по длине получаемого результата Length(R). Чем короче длина, тем лучше пара (С,В).
В действительности не надо вычислять R, чтобы найти ее длину, достаточно оценки: Length (R) £ Length (C) + Length (B) – 2. Смэйгл рекомендует упорядочивать пары (С,В) в списке CLIST по возрастанию.
С. Использование эвристических оценочных функций
Определим h*(C,B) для пары (С,В), как число применений правила резолюции в минимальном доказательстве с верхним укор. дизъюнктом С и первым боковым дизъюнктом В.
Однако h*(C,B) заранее неизвестна, поэтому введем оценку h(C,B) величины h*(C,B). Предположим, что h(C,B) можно выразить в виде: h(C,B) = w0+w1f1(C,B)+…+wnfn(C,B) (1), где fi (i=1,…,n) – вещественная функция от С и В, а wi – вес, сопоставленный величине fi. (fi называют характеристикой пары (С,В)).
Возможны следующие характеристики пар:
1. Число необрамленных литер в C.
2. Число обрамленных литер в С.
3. Число боковых дизъюнктов для С.
4. Число констант в последней литере из С.
5. Число функциональных символов в последней литере из С.
6. Число обрамленных литер в С, поглощающих последнюю литеру из В.
7. Число различных переменных в С и В.
8. length (C) + length (B) – 2
9. Число констант в С / (1+число переменных в С)
10. Число констант в С / (1+число различных переменных в С)
11. Глубина С.
12. Число необрамленных литер, входящих как в С, так и в В.
13. Число литер в В, имеющих обрамленное дополнение в С.
14. Число различных предикатных символов в С и В.
Функция h(C,B) может быть линейной или нелинейной от f1(C,B),…,fn(C,B), будем называть ее эвристической оценочной функцией, или просто оценочной функцией. Будем помещать пары (С,В) в CLIST по возрастанию значений h(C,B). Рассмотрим один из способов определения подходящих величин w0,…,wn.Способ определения значений множества w.
Допустим, что мы знаем величины h*(C1,B1),…,h(Cq,Bq), тогда определение w0,…,wn таких, что минимально выражение (2) – оценка по наименьшим квадратам.
Определим матрицы H, F и W следующим образом:
Тогда W=(F’F)–1F’H (3),где F’ – транспонированная матрица F, (F’F)–1 – обратная матрица к (F’F).
Рассмотрим пример. Занумеруем все дизъюнкты дерева. Используем следующие характеристики.
f1(C,B) = length (C) + length (B) – 2
f2(C,B) = число обрамленных литер в С
f3(C,B) = число необрамленных литер, входящих как в С, так и в В
f4(C,B) = число литер в В, имеющих обрамленное дополнение в С
f5(C,B) = число обрамленных литер в С, поглощающих последнюю литеру из В
Вычисляя характеристики для любой пары дерева, получим:
i | пара | f1(Ci,Bi) | f2(Ci,Bi) | f3(Ci,Bi) | f4(Ci,Bi) | f5(Ci,Bi) | h*(Ci,Bi) |
(1,2) | |||||||
(1,3) | |||||||
(4,6) | |||||||
(4,7) | |||||||
(5,8) | |||||||
(5,9) | |||||||
(10,14) | |||||||
(10,15) | |||||||
(11,16) | |||||||
(11,17) | |||||||
(12,18) | |||||||
(12,19) | |||||||
(13,20) | |||||||
(13,21) |
Вычисляя по (3) W, получим:
w0=0,3 | w2=0,76 | w4=–1,44 |
w1=1,68 | w3=–0,24 | w5=0,6 |
Тогда линейная оценочная функция примет вид:
h(C,B)=0,30+1,68f1(C,B)+0,76 f2(C,B)–0,24 f3(C,B)–1,44 f4(C,B)+0,6 f5(C,B)
Если упорядочить пары в CLIST непосредственно перед 3 шагом модифицированного метода поиска в глубину, то получим 144 ветки дерева.
Конечно, чтобы оценочная функция была хорошей,
Но нас должен волновать вопрос и о том, необходимо рассмотреть как можно больше примеров.является ли выбранное множество характеристик хорошим?
Конечно, если оценочная функция обобщается на новые примеры, то можно считать это множество хорошим, в противном случае его надо менять.
Дата добавления: 2016-03-05; просмотров: 610;