Создать сокращенную упорядоченную диаграмму двоичных решений (ROBDD) из таблицы истинности
Существует ли программный пакет (предпочтительно приложение, а не библиотека), который создает сокращенные упорядоченные двоичные диаграммы принятия решений (ROBDD) из заданной таблицы истинности (в некотором текстовом формате)?
3 ответа
Вы также можете попробовать это: http://formal.cs.utah.edu:8080/pbl/BDD.php
Это лучший инструмент для BDD, который я использовал до сих пор.
BDD - это структура данных с ограниченным объемом памяти из-за сильной зависимости от обнаружения дубликатов неоправданных таблиц. Большинство пакетов BDD, которые вы найдете, не совсем подходят для больших таблиц с общей правдой, вместо этого они оптимизированы для очень разреженных или повторяющихся выражений.
В стандартных пакетах BDD вы работаете с выражениями, работающими с переменными. Поэтому вам придется перебирать свою таблицу истинности, создавая что-то вроде выражения произведения сумм для 1 в таблице. Попутно большинство библиотек будет динамически переупорядочивать переменные в соответствии с ограничениями памяти, вызывая еще одно огромное замедление. После примерно 24 переменных, даже с очень разреженными таблицами истинности, эти библиотеки начнут работать в современных системах.
Если вам нужны только конечные узлы BDD, для которых задана таблица истинности с уже неявно определенным порядком переменных, вы можете пропустить большую сложность с внешними библиотеками и ужасным временем выполнения, просто используя некоторые инструменты обработки текста Unix.
Хороший ресурс по BDD, TAOCP v4.1b Кнута, показывает эквивалентность узлов BDD и их "бусин", неоправданных таблиц, которые не являются квадратными строками. Я собираюсь обратиться к более простой версии, ZDD, которые имеют схожие структуры, называемые "зеадами": субстабильные положительные части, которые не являются полностью нулевыми. Чтобы обобщить обратно в BDD, замените sed+grep в конвейере программой, фильтрующей квадратные строки вместо сохранения ненулевых строк положительной части.
Чтобы напечатать все значения правдоподобной таблицы (представленные в виде однострочного файла с 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, с радостью использует все это для кэширования диска, чтобы сделать его еще быстрее.
С любой библиотекой BDD вы можете делать то, что хотите. Конечно, вы должны написать кусок кода самостоятельно.
Если вы ищете легкий инструмент, я часто использую такой апплет, чтобы быстро взглянуть на BDD функции:
Я тоже искал что-то подобное, но не нашел реализации javascript.
Теперь я создал свой собственный модуль, который способен создавать, минимизировать и оптимизировать сортировку bdd из таблицы истинности.