Создайте сокращенную диаграмму упорядоченных двоичных решений (ROBDD) из таблицы истинности

Есть ли программный пакет (желательно приложение, а не библиотека), который создает сокращенные упорядоченные двоичные диаграммы решений (ROBDD) из заданной таблицы истинности (в некотором текстовом формате)?


person tomash    schedule 25.03.2013    source источник


Ответы (4)


Вы также можете попробовать следующее: http://formal.cs.utah.edu:8080/pbl/BDD.php

Это лучший инструмент для BDD, который я когда-либо использовал.

person remustata    schedule 10.06.2013

С любой библиотекой BDD вы можете делать то, что хотите. Конечно, вы должны написать кусок кода самостоятельно.

Если вам нужен легкий инструмент, я часто использую такой апплет, чтобы быстро взглянуть на BDD функции:

http://tams-www.informatik.uni-hamburg.de/applets/java-bdd/

person Lorenzo    schedule 25.03.2013
comment
Предоставленная страница не совсем то, что я хотел. Я хотел бы предоставить таблицу истинности и вычислить для нее ROBDD (то есть сокращенную OBDD), которая является наименьшим основанным на BDD представлением данной функции. Страница ничего этого не позволяет. - person tomash; 27.03.2013
comment
Что ж, он извлекает ROBDD из функции, заданной в виде выражения (на самом деле, не из таблицы истинности). На выходе получается ROBDD, хотя в названии написано только BDD. Или вы ищете лучший порядок переменных? - person Lorenzo; 27.03.2013

BDD - это структура данных с ограниченным объемом памяти из-за сильной зависимости от обнаружения повторяющихся субтаблиц истинности. Большинство пакетов BDD, которые вы найдете, не совсем подходят для больших общих таблиц истинности, вместо этого они оптимизированы для очень редких или часто повторяющихся выражений.

В стандартных пакетах BDD вы работаете с выражениями, оперирующими с переменными. Таким образом, вам придется перебирать таблицу истинности, создавая что-то вроде выражения произведения сумм для единиц в таблице. Попутно большинство библиотек будут динамически переупорядочивать переменные в соответствии с ограничениями памяти, что вызывает еще одно огромное замедление. После примерно 24 переменных, даже с очень разреженными таблицами истинности, эти библиотеки начнут ломаться в современных системах.

Если вы ищете только конечные узлы BDD с учетом таблицы истинности с уже неявно определенным порядком переменных, вы можете пропустить большую часть сложности с внешними библиотеками и ужасными средами выполнения, просто используя некоторые инструменты обработки текста Unix.

Хороший ресурс по BDD, TAOCP v4.1b Кнута, показывает эквивалентность узлов BDD и их «бусинок», суб-таблиц истинности, которые не являются квадратными строками. Я собираюсь обратиться к более простой версии, ZDD, которые имеют аналогичную структуру, называемую «zeads»: положительные частичные субтаблицы истинности, которые не являются полностью нулевыми. Чтобы вернуться к BDD, замените sed + grep в конвейере программой, фильтрующей квадратные строки вместо сохранения положительных частей ненулевых строк.

Чтобы напечатать все zeads таблицы истинности (заданной как однострочный файл ascii '1 и' 0, новая строка в конце), выполните следующую команду после установки количества переменных и имени файла:

MAX=8; FILENAME="8_vars_truthtable.txt"; for (( ITER=0; ITER<=${MAX}; ITER++ )) ; do INTERVAL=$((2 ** ${ITER})); fold -w ${INTERVAL} ${FILENAME} | sed -n '1~2!p' | grep -v "^0*$" | sort -u ; done

Это имеет много преимуществ по сравнению с пакетами BDD:

  • Просто, практически без посторонних зависимостей.
  • Внешняя сортировка означает отсутствие перебора, в отличие от хеш-таблиц в памяти.
  • Легко распараллеливается и масштабируется, если вы понимаете буферизацию строк и кеширование диска при форковании цикла for.
  • При записи в промежуточные файлы распараллеливается и сортировка.

Я регулярно использую его для таблиц истинности размером до 32 переменных, которые невозможно реально создать с помощью библиотек BDD. Это совсем не требует нагрузки на систему памяти, используя всего несколько мегабайт. Но если у вас есть тонна оперативной памяти, достойная ОС, такая как Linux, с радостью использует ее все для кэширования диска, чтобы сделать его еще быстрее.

person Community    schedule 11.02.2015

Я тоже искал что-то подобное, но не нашел реализации javascript.

Теперь я создал свой собственный модуль, который способен создавать, минимизировать и оптимизировать сортировку bdd из таблицы истинности.

https://github.com/pubkey/binary-decision-diagram

person pubkey    schedule 25.02.2020