Представление BDD в CUDD без упрощения
Можно ли получить bdd для (x0 ∧ x1) ∨ (x0 ∧! X1) ∨ (! X0 ∧ x1) ∨ (! X 0 ∧! X 1), в котором все еще есть узлы, представляющие переменные x0 и x1, используя CUDD ? Я знаю, что приведенная выше логическая формула упрощает константу до функции 1. Но я все еще хочу BDD, который не упрощает формулу, а представляет ее как BDD, «содержащий» узлы, соответствующие как x0, так и x1. Если нет в CUDD, возможно ли это сделать с помощью какого-либо другого инструмента?
Решение
Ну, это может быть не очень полезным ответом, но если вы используете ZDD (также называемые 0-sup-BDD) и представляете константу 1, вы получите график со всеми переменными — используется другое правило сокращения. Я сгенерировал его с помощью другого инструмента, но CUDD также поддерживает ZDD.
Другие решения
Вы можете попробовать библиотеку MEDDLY. (https://meddly.sourceforge.io/).
В этой библиотеке можно использовать различные типы редукции. Например, квазиредукция никогда не пропускает уровень (переменную). Это звучит как то, что вы хотите.
Надеюсь, это поможет.