|
Prikladnaya Diskretnaya Matematika, 2010, Number 1(7), Pages 86–104
(Mi pdm164)
|
|
|
|
This article is cited in 1 scientific paper (total in 1 paper)
Computational Methods in Discrete Mathematics
Algorithms using ROBDD as a base for Boolean constraints
A. S. Ignatiev, A. A. Semenov Institute of System Dynamics and Control Theory, Siberian Branch of the Russian Academy of Sciences, Irkutsk, Russia
Abstract:
In the paper, we study algorithmic properties of ROBDD considered in the role of Boolean constraints in the hybrid (SAT+ROBDD) logical derivation. We suggest ROBDD-analogs for the basic algorithmic procedures used in DPLL-derivation such as variable assignment, unit clause, clause learning, and the techniques of delayed computations. A new algorithm intended for ROBDD reordering is proposed. Computational complexity of all the considered algorithms is provided.
Keywords:
logical equations, binary decision diagrams, hybrid logical derivation.
Citation:
A. S. Ignatiev, A. A. Semenov, “Algorithms using ROBDD as a base for Boolean constraints”, Prikl. Diskr. Mat., 2010, no. 1(7), 86–104
Linking options:
https://www.mathnet.ru/eng/pdm164 https://www.mathnet.ru/eng/pdm/y2010/i1/p86
|
Statistics & downloads: |
Abstract page: | 471 | Full-text PDF : | 253 | References: | 56 |
|