Сборники трудов ИСП РАН


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

С. П. Вартанов, Д.В. Сидоров.

Аннотация

В статье предложена оптимизация алгоритма проверки выполнимости булевых формул DPLL (Davis — Putnam — Logemann — Loveland) с помощью кэширования промежуточных результатов при решении задачи нахождения входных данных для неинтерактивных программ. Дополнительная информация для оптимизации алгоритма запоминается на одном из предыдущих запусков алгоритма. Возможность подобного рода модификации алгоритма основана на особенности последовательностей проверяемых формул.

В результате модифицированный алгоритм показал ускорение по сравнению с использованием алгоритма DPLL без оптимизаций. Для проверки использовался тестовый солвер, последовательности формул генерировались инструментом Avalanche.

Ключевые слова

проверка выполнимости булевых формул, алгоритм DPLL, оптимизация

Издание

Труды Института системного программирования РАН, том 22, 2012, стр. 281-292.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2012-22-16

Полный текст статьи в формате pdf Вернуться к содержанию тома