Источник: Институт системного анализа РАН
УДК 004.832.38
АЛГОРИТМ РЕЗОЛЮЦИИ В ЛОГИКЕ ВЫСКАЗЫВАНИЙ ПРИ 0-1-НОМ ПРЕДСТАВЛЕНИИ ДИЗЪЮНКТОВ
И.С. Грунский (grunsky@iamm.ac.donetsk.ua)
Институт прикладной математики и механики НАН Украины, Донецк, Украина
М.В. Волченко (mitrofany4@gmail.com)
Государственный университет информатики и искусственного интеллекта, Донецк, Украина
В работе рассматривается проблема автоматизации алгоритма резолюции в логике высказываний. Предложено 0,1-ное представление дизъюнктов и матричная структура представления связей дизъюнктов, для которых разработан алгоритм резолюции с эвристической функцией выбора связи для резольвирования. Показана эффективность предложенного алгоритма на серии экспериментальных данных.
Введение
В настоящее время алгоритмы дедуктивного вывода находят широкое применение в системах принятия решений, дедуктивных базах данных, информационно-поисковых системах. В числе других областей использования дедуктивного вывода можно также назвать верификацию спецификаций компьютерного оборудования (процедуры дедуктивного вывода использовались, например, при верификации процессоров компании AMD), проверку корректности систем безопасности, анализ корректности протоколов передачи данных [Вагин и др., 2004.
Одной из основных проблем, встающих перед разработчиками процедур дедуктивного вывода, является экспоненциальный рост пространства поиска. В условиях постоянно растущих объемов обрабатываемых данных особое значение приобретает проблема создания процедур дедуктивного вывода, способных эффективно работать с большими множествами дизъюнктов [Вагин и др., 2004], [Gomez et al., 2008].
Для эффективной обработки множеств дизъюнктов большой мощности процедура вывода должна отвечать следующим требованиям:
- на сколько возможно, сужать пространство поиска контрарной пары на каждом шаге резольвирования;
- исключать из дальнейшего рассмотрения дизъюнкты, которые не могут быть использованы в процессе доказательства;
- в процедуре вывода должен быть реализован эффективный алгоритм выбора контрарных пар для резольвирования[Вагин и др., 2004], [Gomez et al., 2008].
Резольвирование на графовых структурах в качестве основы для построения процедур дедуктивного вывода является одним из способов повышения эффективности процесса вывода. Был создан ряд алгоритмов дедуктивного вывода на графовых структурах. Однако при решении задач практической сложности, которые характеризуются экспоненциальным ростом числа дизъюнктов, данные алгоритмы не всегда показывали удовлетворительные результаты, что привело к дальнейшим исследованиям в области повышения эффективности процедур вывода [Аверин, 2004].
В настоящей работе рассматривается проблема автоматизации алгоритма резолюции в логике высказываний на основе построения матрицы связей в 0-1-ном представлении дизъюнктов.
1. Постановка задачи
Рассматривается классическая задача проверки выполнимости логических высказываний. Исходными данными является множество дизъюнктов S={С1, С2, …, Сk}. Необходимо проверить выводим ли из множества дизъюнктов S заданного высказывания пустой дизъюнкт „. Если это так, то S невыполнимо, иначе – выполнимо [Вагин и др., 2004].
Данная задача является NP-полной за счет экспоненциального роста пространства поиска.
Одним из основных методов повышения эффективности процесса вывода является резольвирование на графе связей [Вагин и др., 2004]. При построении графа связей для последовательности дизъюнктов S=С1, С2, …, Сk, состоящих из конъюнктов K1, K2, …, Km, каждому дизъюнкту ставится в соответствие вершина графа G. Две вершины соединяются ребром, называемым связью, если они образуют контрарную пару, т.е. по этим дизъюнктам может быть проведено резольвирование. Результат резольвирования узлов добавляется в граф G.
Последовательный алгоритм вывода на графе связей имеет следующий вид [Вагин и др., 2004]:
1. Выбор связи из множества связей.
2. Резольвирование связи и получение резольвенты. Удаление связи, по которой производилось резольвирование.
3. Если получена пустая резольвента, то успешное завершение, иначе помещение резольвенты в граф, добавление ее связей, удаление дизъюнктов-тавтологий и чистых дизъюнктов, выполнение операции поглощения дизъюнктов.
4. Если граф не содержит ни одного дизъюнкта, то неуспешное завершение алгоритма, иначе переход к шагу 1.
Графовое представление позволяет существенно сокращать пространство поиска, но в ряде случаев не позволяет получить оптимальное решение. В настоящей работе предложен матричный способ представления дизъюнктов для алгоритма резолюции логики высказываний.
2. Матричное представление дизъюнктов
2.1. Представление дизъюнктов
Пусть задано множество
S дизъюнктов. Пусть 
- алфавит всех букв из всех дизъюнктов.
Считаем, что А линейно упорядочен.
На начальном этапе каждый дизъюнкт будем представлять 0,1-ным набором 
по правилу[Волченко, 2009]:
В результате такого представления будет получено множество 0,1-ных векторов (наборов), соответствующее исходному множеству S.
2.2. Формирование списков дизъюнктов
Полученные наборы 
сортируются по
убыванию числа ‘_’ в наборах. В группах векторов с одинаковым числом ‘_’
проводится дополнительная сортировка по возрастанию числа единиц. Полученное
упорядоченное множество дизъюнктов будем называть списком дизъюнктов.
2.3. Построение треугольной матрицы связей
Каждой паре наборов 
и 
из списка дизъюнктов, ставится в
соответствие связь R(l,j) по правилу:
,
и 
количество нулей в связи R(l,j) больше
одного, то в результате резольвирования соответствующей пары дизъюнктов будет
получен дизъюнкт-тавтология, и такую связь необходимо удалить. 
, то дизъюнкт 
поглощает дизъюнкт 
, удаляем j-е строку
и столбец.
, где n – первоначальное количество дизъюнктов. В 
и 
нового вектора – резольвенты 
, который
определяется по правилу: 
, то удачное
завершение, иначе добавление резольвенты в начало отсортированного списка,
переход к шагу 2.