Алгоритм резолюции в логике высказываний при 0-1-ном представлении дизъюнктов

Размещено на http://www.allbest.ru/

Институт прикладной математики и механики НАН Украины, Донецк, Украина

Государственный университет информатики и искусственного интеллекта, Донецк, Украина

Алгоритм резолюции в логике высказываний при 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) по правилу:

3. Описание алгоритма резолюции на матрице связей

Неопределяемые понятия общеприняты и их можно найти в [Вагин и др., 2004].

Предлагаемый алгоритм состоит из следующих процедур: предобработка матрицы, выбор связи для резольвирования, резольвирование дизъюнктов, добавление полученного вектора-резольвенты в матрицу связей.

3.1 Процедура предобработки матрицы

Выполняется удаление дизъюнктов-тавтологий, поглощенных и чистых дизъюнктов для всех связей матрицы. В матрице связей если для наборов и количество нулей в связи R(l,j) больше одного, то в результате резольвирования соответствующей пары дизъюнктов будет получен дизъюнкт-тавтология, и такую связь необходимо удалить.

Если , то дизъюнкт поглощает дизъюнкт , удаляем j-е строку и столбец.

Если достигнут конец первой строки, значит, получен чистый дизъюнкт, удаляем первую строку.

3.2 Выбор связи для резольвирования

Наиболее важным этапом реализации алгоритма является выбор связи для резольвирования, так как при неправильном выборе связи возможно увеличение количества дизъюнктов до , где n - первоначальное количество дизъюнктов. В [Волченко, 2009] были предложены эвристики позволяющие в частных случаях повысить эффективность предложенного алгоритма:

- Последовательное резольвирование связей треугольной матрицы связей от столбца с минимальным номером до столбца с максимальным номером.

- Резольвирование связей с максимальным количеством единиц.

- Резольвирование связей с минимальным количеством единиц.

- Выбирается та связь, количество `_' которой минимально отличается от количества `_' второго дизъюнкта.

В результате проведения экспериментов с предложенными эвристиками на ряде частных случаев было получено, что резольвирование связей с максимальным числом единиц позволяет получить результат за минимальное число итераций, но при этом наблюдается кратковременный рост количества обрабатываемых дизъюнктов. Выбор связи по числу `_' позволяет уменьшить такой рост, но при этом для получения результата требуется большее число итераций. На основе полученных данных был предложен комплексный подход к выбору связи для резольвирования:

1. Выбирается та связь, количество `_' которой минимально отличается от количества `_' второго дизъюнкта.

2. Если таких дизъюнктов несколько, то происходит резольвирование связей с максимальным количеством единиц.

3.3 Операция резольвирования дизъюнктов

Операция резольвирования осуществляется по построенной матрице связей. Наличие в 0,1-ном наборе связи одного нуля показывает, что дизъюнкты образуют контрарную пару, то есть возможно их резольвирование.

Операция резольвирования заключается в получении из векторов и нового вектора - резольвенты , который определяется по правилу:

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

3.4 Алгоритм резолюции для матричного представления дизъюнктов

1. Построение треугольной матрицы связей.

2. Предобработка матрицы связей:

Если , то дизъюнкт X_i поглощает дизъюнкт X_j, удаляем j-ю строку и столбец, j=j+1.

Если для наборов X_l и X_j количество нулей в связи R(l,j) больше одного, то такую связь необходимо удалить, j=j+1.

3. Последовательный выбор связи для резольвирования. Выбирается связь, количество `_' которой минимально отличается второго дизъюнкта и имеет максимальное число единиц. Если таких дизъюнктов несколько, то происходит резольвирование связей с максимальным количеством единиц.

Если для наборов X_l и X_j количество нулей в связи R(l,j) равно одному, то проводим резольвирование, иначе j=j+1.

Если j больше количества дизъюнктов, удалить первую строку (чистый дизъюнкт).

4. Если , то удачное завершение, иначе добавление резольвенты в начало отсортированного списка, переход к шагу 2.

4. Экспериментальные исследования

Для оценки эффективности предложенного в работе алгоритма были выполнены серия экспериментов. Критериями эффективности метода были выбраны число итераций (резольвирований) и максимальное число дизъюнктов за время работы алгоритма.

Анализ эффективности предложенного алгоритма проводился на множествах дизъюнктов различной мощностью и различной длиной алфавита (табл. 1). Результаты оценки являются средними по результатам 30 экспериментов.

Табл. 1.

Анализ экспериментальных исследований предложенного алгоритма на ряде частных случаев показал существенное уменьшение числа выполняемых итераций при незначительном росте пространства поиска.

Выводы

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

Экспериментальными данными показано, что алгоритм для матричного представления дизъюнктов позволяет уменьшить пространство поиска, количество сравнений дизъюнктов, а также уменьшено количество резольвирований.

Список литературы

[Аверин, 2004] Аверин А.И. Исследование и разработка алгоритмов параллельного вывода на графовых структурах. Автореферат. - М.: МЭИ, 2004.

[Вагин и др., 2004] Вагин В.Н., Головина Е.Ю., Загорянская А.А., Фомина М.В. Достоверный и правдоподобный вывод в интеллектуальных системах / Под ред. В.Н. Вагина, Д.А. Поспелова. - М.: ФИЗМАТЛИТ, 2004.

[Волченко, 2009] Волченко М.В. Представление термов для алгоритма резолюции логики высказываний. Информатики и компьютерные технологии / Материалы V международной конференции. - Донецк: Изд-во ДГТУ, 2009.

[Gomez et al., 2008] Gomez C.P., Kautz H., A. Sabharawal and B.Selman. Satisfability Solvers// Handbook of Knowledge Representaton, 2008.

Размещено на Allbest.ru