Диаграммы решений
Вот есть ROBDD - reduced (нет двух разных узлов с одинаковыми подузлами) ordered (переменные имеют некоторый порядок, во всех ветвях диаграммы) binary decision (решение принимается по значению переменной - истина или ложь) diagram.
А недавно появились SDD - sentential decision diagrams.
Я не большой спец в SDD, поэтому могу говорить, что угодно, что я сейчас и буду делать.
Давайте разобьём наши переменные из логической формулы на два подмножества - верхнее и нижнее. На две неравных половины.
Для любой RODBB мы можем перечислить все значения, при которых она истинна, и задать им порядковые номера (это, так сказать, представление в виде дизъюнктивной нормальной формы). Давайте сделаем это для части формулы, что содержит только переменные из верхнего подмножества - мы будем считать, для простоты построения, что части формулы только с нижними переменными истинны.
Далее, для каждого истинного присваивания значения верхней половины мы задаём ROBDD для соответствующей ему формулы с переменными только нижней половины.
В чём прикол? В том, что ROBDD нижней половины могут разделять узлы, как и узлы верхней половины, это раз. Второе - ROBDD без разделения на два класса переменных будет стремиться иметь размер пропорциональный произведению размеров ROBDD (если я всё правильно понимаю), здесь же мы пытаемся уменьшить совокупный размер через вычленение некоторых "общих подвыражений".
Коли мы смогли поделить наши переменные на две половины, мы можем поделить и половины как-то. Это может уменьшить размер представления формулы ещё сильнее. Для некоторых задач разница экспоненциально большая.
Собственно, всё. ;)
А недавно появились SDD - sentential decision diagrams.
Я не большой спец в SDD, поэтому могу говорить, что угодно, что я сейчас и буду делать.
Давайте разобьём наши переменные из логической формулы на два подмножества - верхнее и нижнее. На две неравных половины.
Для любой RODBB мы можем перечислить все значения, при которых она истинна, и задать им порядковые номера (это, так сказать, представление в виде дизъюнктивной нормальной формы). Давайте сделаем это для части формулы, что содержит только переменные из верхнего подмножества - мы будем считать, для простоты построения, что части формулы только с нижними переменными истинны.
Далее, для каждого истинного присваивания значения верхней половины мы задаём ROBDD для соответствующей ему формулы с переменными только нижней половины.
В чём прикол? В том, что ROBDD нижней половины могут разделять узлы, как и узлы верхней половины, это раз. Второе - ROBDD без разделения на два класса переменных будет стремиться иметь размер пропорциональный произведению размеров ROBDD (если я всё правильно понимаю), здесь же мы пытаемся уменьшить совокупный размер через вычленение некоторых "общих подвыражений".
Коли мы смогли поделить наши переменные на две половины, мы можем поделить и половины как-то. Это может уменьшить размер представления формулы ещё сильнее. Для некоторых задач разница экспоненциально большая.
Собственно, всё. ;)