Стратегии метода резолюций

В множестве дизъюнктов существует, как правило, не одна пара дизъюнктов, к которым можно применить правило резолюций. Способ выбора дизъюнктов и летералов в них, к которым применяется правило резолюций (и правило склейки) для получения резольвенты, называется стратегией метода. В этом параграфе будет рассмотрено три стратегии: стратегия насыщения уровней. Предпочтения более коротких дизъюнктов и вычеркивания. Достаточно полное описание известных стратегий содержится в книге Ч.Ченя и Р.Ли, приведенной в списке литературы.

Стратегия насыщения уровней.Наиболее простой с идейной точки зрения способ выбора дизъюнктов для получения резольвенты состоит в организации полного перебора возможных вариантов. Этот перебор можно организовать следующим образом. Пусть S₀=S – исходное множество дизъюнктов. Будем считать, что S₀ упорядочено. Пусть D₂ пробегает по порядку множество дизъюнктов S₀, начиная со второго. В качестве D₁ берем последовательно дизъюнкты из S₀, предшествующие D₂ начиная с первого, и формируем последовательность S₁, состоящее из всевозможных резольвент дизъюнктов D₁ и D₂. (Порядок на S₁ определяется порядком добавления дизъюнктов в S₁.) Предположим, что получены последовательности дизъюнктов S₀, S₁,…,S_n-1 и n>1. Тогда последовательность S_n получается следующим образом. В качестве D₂ берутся по порядку дизъюнкты из S_n-1, а в качестве D₁ – дизъюнкты из S₀ÈS₁È…ÈS_n-1, предшествующие D₂. Последовательность S_n будет состоять из всевозможных резольвент дизъюнктов D₁ и D₂. Процесс порождения резольвент прекращается, как только получается пустой дизъюнкт.

Описанная в предыдущем абзаце стратегия называется стратегией насыщения уровней. (Уровни – это последовательности S₀, S₁,…,S_n,…) Проследим, как она работает на примере множества дизъюнктов S={XÚY, ØXÚØY, XÚZ, ØXÚZ, ØZ}:

Мы видим, что порождено много лишних дизъюнктов. Так, 6 и 7–тождественно истинные дизъюнкты. Удаление или добавление тождественно истинного дизъюнкта не влияет на выполнимость множества дизъюнктов, поэтому такие дизъюнкты должны быть удалены из вывода. Далее, некоторые дизъюнкты порождаются неоднократно, например, XÚY, ØXÚØY, YÚZ. Это означает, что выбором дизъюнктов для получения резольвенты надо управлять.

Стратегия предпочтения (более коротких дизъюнктов).Эта стратегия является следующей модификацией предыдущей: сначала в качестве D₂ берется самый короткий дизъюнкт из S_n-1 (если таких несколько, то они перебираются по порядку), затем более длинные и т.д. Аналогичные условия налагаются и на D₁. Такая стратегия в применении к тому же множеству дизъюнктов S дает следующее:

Вывод оказался короче, чем в предыдущем примере, но попрежнему содержит повторяющиеся и тождественно истинные дизъюнкты. Свободным от этих недостатков является вывод, полученный в соответствие со следующей стратегией.

Стратегия вычеркивания. Введем вначале следующие понятия.

Определение. Дизъюнкт D называется расширением дизъюнкта C, если существует подстановка σ такая, что σ(C)ÍD.

Для логики высказываний это означает, что просто D=CÚD^/ (при некоторой перестановке литералов). В случае логики предикатов ситуация не столь проста. Например, D=Q(a)ÚP(b,y)ÚR(u) есть расширение дизъюнкта C=P(x,y)ÚQ(z)ÚQ(v).

Стратегия вычеркивания, как и стратегия предпочтения является модификацией стратегии насыщения уровней. Она применяется следующим образом: после того, как получена очередная резольвента D дизъюнктов D₁ и D₂ проверяется, является ли она тождественно истинной формулой или расширением некоторого дизъюнкта C из S₀È...ÈS_n-1, и в случае положительного ответа D вычеркивается, т.е. не заносится в последовательность S_n.

Применение стратегии к прежнему множеству дизъюнктов дает следующее:

Рассмотренные стратегии являются полными в том смысле, что если множество дизъюнктов S невыполнимо, то из S пользуясь стратегией можно вывести пустой дизъюнкт. Для первых двух стратегий это достаточно очевидно. Полнота стратегии вычеркивания следует из того, что если D и C–дизъюнкты из S и D–расширение C, то множество S невыполнимо в том и только в том случае, когда невыполнимо множество S|{D}.