Представление BDD в CUDD без упрощения

Question

Возможно ли получить bdd для (x0 ∧ x1) ∨ (x0 ∧! X1) ∨ (! X0 ∧ x1) ∨ (! X 0 ∧! X 1), в котором еще есть узлы, представляющие переменные x0 и x1, используя CUDD?Я знаю, что приведенная выше логическая формула упрощает константу до функции 1. Но я все еще хочу BDD, который не упрощает формулу, а представляет ее как BDD, «содержащий» узлы, соответствующие как x0, так и x1.Если нет в CUDD, возможно ли это сделать с помощью другого инструмента?

Answer 1

Возможно, вы захотите попробовать MEDDLY Library.(https://meddly.sourceforge.io/).

В этой библиотеке можно использовать различные типы редукции. Например, квазиредукция никогда не пропускает уровень (переменную). Это звучит так, как вы хотите.

Надеюсь, это поможет.

Answer 2

Что ж, это не может быть полезным ответом, но если вы используете ZDD (также называемые 0-sup-BDD) и представляете константу 1, вы получите график со всеми переменными - используется другое правило сокращения.Я создал его с помощью другого инструмента, но CUDD также поддерживает ZDD.