Рассматриваются диаграммы нового типа, используемые для представления дизъюнктивных нормальных форм. Показано, что данный класс диаграмм можно применять для компактного представления баз конфликтных дизъюнктов, накапливаемых в процессе нехронологического DPLL-вывода.
Скачать электронную версию публикации
Загружен, раз: 171
- Title Об эффективном представлении дизъюнктивных нормальных форм диаграммами специального вида
- Headline Об эффективном представлении дизъюнктивных нормальных форм диаграммами специального вида
- Publesher
Tomsk State University - Issue Прикладная дискретная математика 6 (Приложение)
- Date:
- DOI
Ключевые слова
ДНФ, решающие диаграммы, BDD, ZDD, дизъюнктивные диаграммы, decision diagrams, BDD, ZDD, disjunctive diagramsАвторы
Ссылки
Bryant R.E. Graph-based algorithms for Boolean function manipulation // IEEE Trans. Comput. 1986. V. 35. No. 8. P. 677-691.
Minato S. Zero-suppressed BDDs for set manipulation in combinatorial problems // Proc. DAC-93, June 14-18, 1993, Dallas, Texas. P. 272-277.
Dowling W. and Gallier J. Linear-time algorithms for testing the satisfiability of propositional Horn formulae // J. Logic Programming. 1984. V. 1. No. 3. P. 267-284.
Marques-Silva J. P. and Sakallah K. A. GRASP: A search algorithm for propositional satisfiability // IEEE Trans. Comput. 1999. V.48. No. 5. P. 506-521.
Игнатьев А. С., Семенов А. А. Алгоритмы работы с ROBDD как с базами булевых ограничений // Прикладная дискретная математика. 2010. №1. С. 86-104.
Ignatiev A. and Semenov А. DPLL+ROBDD derivation applied to inversion of some cryptographic functions // LNCS. 2011. V.6695. P. 76-89.
Een N. and Sorensson N. Translating pseudo-Boolean constraints into SAT // J. Satisfiability, Boolean Modeling and Computation. 2006. V.2. P. 1-25.
Об эффективном представлении дизъюнктивных нормальных форм диаграммами специального вида | Прикладная дискретная математика. 2013. № 6 (Приложение).
Скачать полнотекстовую версию
Полнотекстовая версияЗагружен, раз: 1886