ОПТИМИЗАЦИЯ ЗАДАЧИ ПРОВЕРКИ ВЫПОЛНИМОСТИ БУЛЕВЫХ ОГРАНИЧЕНИЙ ПРИ ПОМОЩИ КЭШИРОВАНИЯ ПРОМЕЖУТОЧНЫХ РЕЗУЛЬТАТОВ

PDF

PDF (12 страниц) на сайте ИСП РАН

Опубликовано в «Трудах Института системного программирования РАН», том 22, 2012 г.

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

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

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

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

  1. Исаев, И. К. Сидоров Д. В. Применение динамического анализа для генерации входных данных, демонстрирующих критические ошибки и уязвимости в программах. Программирование [№ 4]. 2010. 16 с.

  2. С. В. Зеленов, С. А. Зеленова. Автоматическое определение выполнимости наборов формул для операций сравнения. Труды ИСП РАН, том 14. 109-118 с. Москва, 2008.

  3. Davis M., Logemann G., Loveland D. A machine program for theorem proving // Communication of the ACM. 1962. P. 394-397.

  4. Новикова Н. М. Основы оптимизации. Москва. 1998. 17-22 c.

  5. Eén N., Sörensson N. MiniSat solver [HTML] (http://minisat.se/)

  6. Katelman M., Soos M. STP Constraint Solver [HTML] (http://sites.google.com/site/stpfastprover/)

© Сергей Вартанов, 2007—2015see also in English