Preview

Труды Института системного программирования РАН

Расширенный поиск

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

Полный текст:

Аннотация

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

Об авторах

С. П. Вартанов
ИСП РАН
Россия


Д. В. Сидоров
ИСП РАН
Россия


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

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/)


Для цитирования:


Вартанов С.П., Сидоров Д.В. Оптимизация задачи проверки выполнимости булевских ограничений при помощи кэширования промежуточных результатов. Труды Института системного программирования РАН. 2012;22.

For citation:


Vartanov S., Sidorov D. Optimization of Boolean satisfiability solver by caching intermediate results. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2012;22. (In Russ.)

Просмотров: 50


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


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