Об одном классе решающих диаграмм

Вводится класс решающих диаграмм, предназначенных для представления нормальных форм булевых функций. В частности, рассматриваются дизъюнктивные диаграммы, представляющие дизъюнктивные нормальные формы (ДНФ). В отличие от двоичных решающих диаграмм (BDD, ROBDD), для произвольной ДНФ представляющая ее дизъюнктивная диаграмма строится за полиномиальное от объема двоичного кода ДНФ время. Описаны соответствующие алгоритмы. Приведены результаты вычислительных экспериментов, в которых предложенные диаграммы используются для уменьшения объема информации, накапливаемой в процессе решения трудных вариантов задачи о булевой выполнимости (SAT).

Статья представлена к публикации членом редколлегии: А. А. Лазарев