On the effective representation of disjunctive normal forms by diagrams of a special kind
For an arbitrary disjunctive normal form of a Boolean function, a disjunctive diagram representation is proposed. This kind of diagrams is constructed in a polynomial time and can be used to reduce the size of conflict databases produced during non-chronological DPLL derivation.
Download file
Counter downloads: 273
Keywords
ДНФ, решающие диаграммы, BDD, ZDD, дизъюнктивные диаграммы, decision diagrams, BDD, ZDD, disjunctive diagramsAuthors
| Name | Organization | |
| Semenov A. A. | Institute of System Dynamics and Control Theory, Siberian Branch of the Russian Academy of Sciences (Irkutsk) | biclop.rambler@yandex.ru |
References
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.
