Algorithms using ROBDD as a base for Boolean constraints

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.