Есть ли программный пакет (желательно приложение, а не библиотека), который создает сокращенные упорядоченные двоичные диаграммы решений (ROBDD) из заданной таблицы истинности (в некотором текстовом формате)?
Создайте сокращенную диаграмму упорядоченных двоичных решений (ROBDD) из таблицы истинности
Ответы (4)
Вы также можете попробовать следующее: http://formal.cs.utah.edu:8080/pbl/BDD.php
Это лучший инструмент для BDD, который я когда-либо использовал.
С любой библиотекой BDD вы можете делать то, что хотите. Конечно, вы должны написать кусок кода самостоятельно.
Если вам нужен легкий инструмент, я часто использую такой апплет, чтобы быстро взглянуть на BDD функции:
http://tams-www.informatik.uni-hamburg.de/applets/java-bdd/
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, с радостью использует ее все для кэширования диска, чтобы сделать его еще быстрее.
Я тоже искал что-то подобное, но не нашел реализации javascript.
Теперь я создал свой собственный модуль, который способен создавать, минимизировать и оптимизировать сортировку bdd из таблицы истинности.
https://github.com/pubkey/binary-decision-diagram