25.Метод резолюций Робинсона для задачи выполнимость.

Принцип резолюций. Принцип резолюций заключается в систематическом построении следствий из текущей системы дизъюнктов на основе операции резолюционирования. Следствия называются резольвентами. Резольвенты строятся для пары дизъюнктов, содержащей контрарную пару литер (булевских переменных). Например, пусть даны два дизъюнкта

Эти дизъюнкты содержат контрарную пару литер - (одна входит в дизъюнкт D₁ без отрицания, вторая – в дизъюнкт D₂ с отрицанием).

Резольвентой дизъюнктов D₁ и D₂ является новый дизъюнкт D_1,2 , который не содержит контрарной пары литер, но содержит все другие литеры из D₁ и D₂. Согласно этому определению, получим D_1,2= .Целью построения резольвент является достижение следующих возможных исходов:

Резольвента оказалась пустой. Например, пустую резольвенту дает следующая пара дизъюнктов

В случае пустой резольвенты делается вывод о невыполнимости системы дизъюнктов (т.е. задача ВЫПОЛНИМОСТЬ не имеет решения в этом случае).

• Невозможно построить новую резольвенту (началось зацикливание). В этом случае делается вывод о выполнимости исходной системы дизъюнктов.

Рассмотрим некоторый полный пример.

Решить следующую задачу ВЫПОЛНИМОСТЬ.

Находим резольвенту D₁ и D₂ :

D_1,2=

Находим резольвенту D_1,2 и D₃ :

D_1,2,3=

Дизъюнкты D_1,2,3 и D₄ дают пустую резольвенту. Вывод – исходная задача ВЫПОНИМОСТЬ не имеет решения.

Проблема метода резолюций – его неэффективность в сложностном смысле. Найти эффективный алгоритм для задачи ВЫПОЛНИМОСТЬ или доказать, что такого алгоритма нет – одна из глобальных нерешенных задач современности. Различные модификации принципа резолюций направлены на сокращение перебора.

26.Метод отсечения литер для задачи выполнимость.

Рассмотрим одну из заслуживающих внимания модификаций принципа резолюций.

Этот метод заключается в последовательном исключении булевских переменных из системы. Сначала избавляемся, скажем, от переменной , затем – от переменной и т.д. Такой систематический процесс рано или поздно завершится и по получению (не получению) пустого дизъюнкта можно будет судить о противоречивости системы (или нет). Рассмотрим пример из задания 1. Для начала избавимся от переменной . С этой целью выпишем все дизъюнкты, содержащие переменную :

Теперь найдем все возможные резольвенты выписанных дизъюнктов с исключаемой литерой . Выпишем эти резольвенты отдельно и добавим к ним те дизъюнкты из исходной системы, которые не содержали литеры . Получим следующую систему:

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

Продолжаем процесс избавления от переменных. На этот раз исключим переменную

Получим следующую систему

Теперь ясно, что никакого пустого дизъюнкта получить не удастся. Делаем вывод, что система выполнима (не противоречива).