On one class of decision diagrams

Abstract

A class of decision diagrams for representation of the normal forms of Boolean functions was introduced. Consideration was given, in particular, to the disjunctive diagrams representing the disjunctive normal forms (DNF). In distinction to the binary decision diagrams (BDD) and reduced ordered binary decision diagram (ROBDD), the disjunctive diagram representing an arbitrary DNF is constructed in a time which is polynomial of the size of the DNF binary code. Corresponding algorithms were described, and the results were presented of the computer-aided experiments where the proposed diagrams were used to reduce the information content accumulated in the course of deciding hard variants of Boolean satisfiability problem (SAT).