ГлавнаяАрхивАЛГОРИТМЫ РАБОТЫ С ROBDD КАК С БАЗАМИ БУЛЕВЫХ ОГРАНИЧЕНИЙ

АЛГОРИТМЫ РАБОТЫ С ROBDD КАК С БАЗАМИ БУЛЕВЫХ ОГРАНИЧЕНИЙ | Прикладная дискретная математика. 2010. № 1(7).

Исследуются алгоритмические свойства сокращенных упорядоченных диаграмм решений (ROBDD) при их рассмотрении в роли баз булевых ограничений в гибридном (SAT+ROBDD)-выводе. Приведены ROBDD-аналоги основных алгоритмических процедур, используемых в DPLL-выводе (подстановки, правило единичного дизъюнкта, CL-процедура, механизмы отсроченных вычислений). Описан новый алгоритм изменения порядка в ROBDD. Для всех алгоритмов приводятся оценки их трудоемкости.
  • Title АЛГОРИТМЫ РАБОТЫ С ROBDD КАК С БАЗАМИ БУЛЕВЫХ ОГРАНИЧЕНИЙ
  • Headline АЛГОРИТМЫ РАБОТЫ С ROBDD КАК С БАЗАМИ БУЛЕВЫХ ОГРАНИЧЕНИЙ
  • Publesher Tomask State UniversityTomsk State University
  • Issue Прикладная дискретная математика 1(7)
  • Date:
  • DOI
Ключевые слова
логические уравнения, двоичные диаграммы решений, гибридный вывод, logical equations, binary decision diagrams, hybrid logical derivation
Авторы
Ссылки
Воеводин В. В., Воеводин Вл. В. Параллельные вычисления. СПб.: БХВ-Петербург, 2002.
Schubert T., Lewis M., Becker B. PaMiraXT: Parallel SAT Solving with Threads and Message Passing // J. Satisf., Bool. Mod. Comp. 2009. V. 6. P. 203-222.
Левитин А. Алгоритмы. Введение в разработку и анализ. М.: Вильямс, 2006.
Bryant R. E. Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams // ACM Comp. Surv. 1992. V. 24. No. 3. P. 293-318.
Beame P., Kautz H., Sabharwal A. Understanding the power of clause learning // Proc. Of 18th Intern. Joint Conf. on Artificial Intellegence (IJCAI). 2003. P. 1194-1201.
Игнатьев А. С., Семенов А. А., Хмельнов А. Е. Использование двоичных диаграмм решений в задачах обращения дискретных функций // Вестник Томского госуниверситета. Сер.: Управление, вычислительная техника, информатика. 2009. №1(6). С. 115-129.
Цейтин Г. С. О сложности вывода в исчислении высказываний // Записки научных семинаров ЛОМИ АН СССР. 1968. Т. 8. С. 234-259.
Семенов А. А. О преобразованиях Цейтина в логических уравнениях // Прикладная дискретная математика. 2009. № 4. С. 28-50.
Хмельнов А. Е., Игнатьев А. С., Семенов А. А Двоичные диаграммы решений в логических уравнениях и задачах обращения дискретных функций // Вестник НГУ. Сер.: Информационные технологии. 2009. Т. 7. № 4. С. 36-52.
Meinel Ch., Theobald T. Algorithms and Data Structures in VLSI-Design: OBDD-Foundations and Applications. Springer Verlag, 1998.
Bryant R. E. Graph-Based Algorithms for Boolean Function Manipulation // IEEE Trans. Comp. 1986. V. 35. No. 8. P. 677-691.
Lee C. Y. Representation of Switching Circuits by Binary-Decision Programs // Bell Systems Technical J. 1959. V. 38. P. 985-999.
Cook S.A. The complexity of theorem-proving procedures // Proc. 3rd Ann. ACM Symp. on Theory of Computing, ACM. 1971. P. 151-159. [Пер.: Кук С. А. Сложность процедур вывода теорем // Кибернетический сборник. Новая серия. 1975. Вып. 12. С. 5-15.]
Семенов А. А. Трансляция алгоритмов вычисления дискретных функций в выражения пропозициональной логики // Прикладные алгоритмы в дискретном анализе. Сер.: Дискретный анализ и информатика. 2008. Вып. 2. С. 70-98.
Заикин О. С., Семенов А. А. Технология крупноблочного параллелизма в SAT-зада-чах // Проблемы управления. 2008. № 1. С. 43-50.
Семенов А. А., Заикин О. С., Беспалов Д. В. и др. Решение задач обращения дискретных функций на многопроцессорных вычислительных системах // Труды Четвертой Меж-дунар. конф. PACO'2008 (Москва, 26-29 октября 2008).М., 2008. С. 152-176.
Lynce I., Marques-Silva J. P. Efficient data structures for backtrack search SAT solvers // Ann. Mathem. Artific. Intellig. 2005. V. 43. P. 137-152.
Zhang L., Madigan C., Moskewicz M., Malik S. Efficient conflict driven learning in a boolean satisfiability solver // Proc. Intern. Conf. on Computer Aided Design (ICCAD). 2001. P. 279-285.
Семенов А. А., Беспалов Д. В. Технологии решения многомерных задач логического поиска // Вестник Томского госуниверситета. Приложение. 2005. №14. С. 61-73.
Закревский А. Д. Логические уравнения. Минск: Наука и техника, 1975.
Семенов А. А. Декомпозиционные представления логических уравнений в задачах обращения дискретных функций // Изв. РАН. Теория и системы управления. 2009. №5. С. 47-61.
<http://minisat.se/MiniSat.html> - MiniSat.
Семенов А. А., Заикин О. С. Неполные алгоритмы в крупноблочном параллелизме комбинаторных задач // Вычислительные методы и программирование. 2008. Т. 9. 108-118.
Moskewicz M., Madigan C., Zhao Y., et al. Chaff: Engineering an Efficient SAT Solver // Proc. Design Automat. Conf. (DAC). 2001. P. 530-535.
Marqeus-Silva J. P., Sakallah K. A. GRASP: A search algorithm for propositional satisfiability // IEEE Trans. Comp. 1999. V. 48. No. 5. P. 506-521.
Davis M., Logemann G., Loveland D. A machine program for theorem proving // Comm. ACM. 1962. V. 5. P. 394-397.
Системная компьютерная биология / под ред. Н. А. Колчанова, С.С.Гончарова, А. Лихошвая, В. А. Иванисенко. Новосибирск: Изд-во СО РАН, 2008. 767 с.
Семенов А. А., Заикин О. С., Беспалов Д. В., Ушаков А. А. SAT-подход в криптоанализе некоторых систем поточного шифрования // Вычислительные технологии. 2008. Т. 13. №6. С. 134-150.
Гаранина Н. О., Шилов Н. В. Верификация комбинированных логик знаний, действий и времени в моделях // Системная информатика. 2005. Вып. 10. С. 114-173.
Кларк Э. М., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking. М.: МЦНМО, 2002.
Hachtel G. D., Somenzi F. Logic synthesis and verification algorithms. Kluwer Ac. Publ, 2002.
<http://www.satlive.org>
www.isa.ewi.tudelft.nl/jsat <http://www.isa.ewi.tudelft.nl/jsat>
АЛГОРИТМЫ РАБОТЫ С ROBDD КАК С БАЗАМИ БУЛЕВЫХ ОГРАНИЧЕНИЙ | Прикладная дискретная математика. 2010. № 1(7).
АЛГОРИТМЫ РАБОТЫ С ROBDD КАК С БАЗАМИ БУЛЕВЫХ ОГРАНИЧЕНИЙ | Прикладная дискретная математика. 2010. № 1(7).
Полнотекстовая версия