Laboratory of Mathematical Logic

Вторник, 30 ноября, комната 106. Начало в 18:00.

30 ноября.
В.Жижкун "Представление булевых функций ациклическими направленными графами"
АБСТРАКТ
Binary Decision Diagrams (BDDs) - способ представления логических функций, позволяющий эффективно реализовать различные операции над ними. В том, что такая проблема достаточно актуальна, можно убедиться, например, построив КНФ отрицания формулы в КНФ. Преимущество BDD в том, что результаты операций над булевыми формулами представляются компактно.
Кроме того, BDD - каноническая форма, поэтому проверка двух функций на эквивалентность заключается в сравнении двух направленых ациклических размеченых графов, а выполнимость формулы - сравнение соответствующего графа с тривиальным.
Существенный недостаток этого способа - необходимость фиксировать порядок переменных. Кроме того, размер графов существенно зависит от выбора такого порядка. Помимо этого, известно, что представление функции умножения двоичных чисел с помощью BDD требует экспоненциального числа узлов при любой перестановке переменных.
Доклад будет сделан на основе статьи Randal E. Bryant "Graph-Based Algorithms for Boolean Function Manipulation".