2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 56
Текст из файла (страница 56)
С другой стороны, таблица истинности и двоичное решмощее дерево — зто канонические представления булевой функции. Среди мвшитических прак- Глава в ставлений булевой функции каноническими являются СДНФ, СКНФ и полнном Жегалкина. Недостатком всех этих канонических представлений булевой функции является нх громоздкость. Сл»якность и СДНФ, и СКНФ, и полинома Жегалкина, а также таблицы истинности и бинарных решакхцнх деревьев растет зкспоненцнально с ростом числа переменных.
Например, бинарное решшощее дерево булевой функции от л переменных всегда имеет 2"' -1 +» вершин, таблица истинности имеет 2" строк. сжнкнссть представления функции полиномом Жегалкина О(2") . Кроме того, недостатком аналитических канонических предсшвяений булевой функции является то, что некоторые фунюши не мо»уг быть представ»юиы в соотвеюзпующих классах, Например, невыполнимая функция ие имеет представления в виде полииома Жегвлкина и в классе СДНФ. Общезначимая функция не имеет представления в СКНФ. Задачи» решаемые с помощью булевых функций. Булевы функции используются в огромном числе приложений информатики, не только в логши и прн спите»е логических схем.
Для булевых функций типичнымн задачамн яввяются следующие: П найти значение функции на конкретной интерпретации (наборе значений аргументов); П найти все интерпретации, на когорых функция равна 1; П проверить, является лн булеза функция выполнимой, невмполнимой, общезначимой; П п ронер»пь, совпвдшот лн две булевых функцци; П выполнить булевы операции над булевыми функциями; П провести минимизацию функции в некотором базисе. Если число переменных, от которых зависит булеза функция, равно 3, 4, даже 5, то работать с такими функциями легко и удобно: разработаны многочисленные приемы решения упомянутых выше задач. Например, карты Карно очень улобны для минимизации булевой функции от трех и четырех переменных, Для числа переменных 5 или б представление функций с помощью карт Карно становится громоздким,, а процесс минимизации трудоемким. При 1Π— 20 переменных вирты Корно, формулы, таблицы истинности примешпъ бессмысленно.
При бояьшом числе переменных все вышеперечисленные задачи решаются очень трудно. Причиной этого является экспоненцнаяьный рост слоя»ности представления булевых функций н соответствующий рост времени работы ного г »адан шелия »ввел» Таяня пе по роста Банер форм» Ь1ажн сыван вреде ческе~ Прин Рис. 9 рева, морф» такой тирук Во-пе вует 1 вычи» гольк иаков перев выбр» иой. 1 предо На р» опрея герма шем С > и п>иибулевой полино.
деревьев >ннарное 2"" -1 гавлення ялнтнче- любых алгоритмов с этими представленнтш. Это ятшется отрткением глав- ного положения теории сложности вычислений> задача яеяаеякм практически иеразреиаиюй, если время, требуемое дяя ре- шеяил конкретных эюемптцюе этой задачи растет эксиоиеяяшыьио с уве- личением раз>тров этих экземттрое. Таким образом, булевы функции, представленные сттщартными способами, не позволяют эффективно решать проблемы вследствие экспоненциального роста слшкиости их предспшления.
> некотохтх. Наюли нома шсташм> использке и при ыи явля- значений !мой, об- >3,4, ляы много рты Ка! рех переюмощью доем ким. н приме. юштотся важности и работы 9.2. Бинарные реаающие диаграммы Бинарная решающая диаграмма (В>тпу 0есЬюп 01айгтп, В00) — зто новая форма представления булевых функций а виде ориентированного графа. Можно считать, что В00 получается ю бинарного решающего дерева выбрасыванием всех избыточных подотру«тур (юоморфных подгрвфов). В00 представляет булеву функцию в виде минимального направленного ацикличес кого графа (решаинцей диаграммы). Пример 9.3 Рнс. 9.2 показывает, вак можно перейти к В00 от двоичного решающего дерева, которое глюке явпяетса ацнклическим ар>рафом, но содерятщим и>аморфные (одинаковые) подграфы.
Рассмотрим по шагам, как можно сделать такой переход, избавляясь от всех избыточностей в исходном дереве. Результирующая структура будет уже не деревом, а ориентированным графом. Во-первых, в исходном двоичном решающем дереве нашего примера существует два одинаковых полдерева с вершиной. помеченной т . Ясно, что для вычнсяения значения функции по значениям аргументов можно использовать только один ю одинаковых подгряфов. В частности, можно объединить одинаковые терминальные вершины, оставив только две, О и 1. Кроме того, если из некоторой вершины оба выхода (со значениями О и 1 соответствующей переменной) ведут в одну н ту же подструктуру, то зта вершина может быль выброшена — значение функции на этом пути не зависит ог этой переменной.
Как результат этих двух преобразований, последний граф на рис. 92 представляет В00 исходной функции. На рис. 9.2 макло видеть, что в результирующем графе выделенный пу>ъ, определяемый значениями переменных (хз О,л>=1,х>=О), приводит в терминальную вершину со значением 1, как и в исходном двоичном рештоямм дереве. ббв Глава р баеве б рве.
Ы, о в А Преобревоеавва лавочного ревввовоо» лврева в ВОР ела Дто ее,хе) рно Ы, е н о Преобрвзоввннв неонового рннаоннго вервен в ВВВ да /(тв,хв, тв) нтв) о Ол)зедвление 9.4 (бишцннш ршиающан дннвраммц, Оас/а(оп ОГ, ИЮ) ВРР— это двоичный направленный граф без нзбыточнопгей, т. е. редуцированный (шдпсеб) ациклнческнй орграф, в котором отсутствуют повторения в структуре, с олной корневой вершиной н в общем случае двумя листьамн, помеченными 0 и 1, Корневая и проммкугочные вершины помечены переменными, из кюкдой иэ них выходят ровно два ребра, соответствующие значениям 0 и 1 переменной, помечмошей вершину. бом) уст(л к ре блиц Ншвание В!шиу Рес!еюп Райшш отрекает основную идею этой формы представления булевой функции: (э В!ныу — потому что использунггся двоичные переменные; (У Оеснбоп — потому что эта графическая структура визуально предстаелжт те решения алгоритма движения по графу, которые приводят к результату (значению функции на данном наборе аргументов); (1 О!айшш — поскольку решение о значении функции принимается как результат движения по упорядоченному ацнкяическому графу (лнаграмме).
Можно видать, что ВРР— зго минимальное графическое представление алгоритма вычисления значения булевой функции по набору значений аргументов в заданном их порядке. В00 определяет возможные пути ст корня в терминальную вершину, представляющую значение функции, в кшкдом промежуточном узле осуществляя решение (выбор пути) в соответствии со значением соответствующего аргумента функции. Хотя ВРР не является деревом, у этого направленного графа всегда есть единственная начальнел вершина (корень), это граф без циклов, у него есть е общем случае две терминальные вершины, помеченные б илн 1. ~реобразованне двоичного решающего дерева в ВРР называется алгоритмом редукции (Кейнса). Главная задача алгоритма редукции — устранить избыточность в графическом представлении алгоритма вычисления булевой функции. Как указываюсь выше, этот алгоритм основан только на двух операшшх (рнс, 9.3): 1) С!: Праеюю слышна.
Объединить (слить) любые изоморфнме подграфы (как частный случай, слелует объединить терминальные вершины, помеченные одинаковыми значениями); 1) С2: Приаме удаееннк Удалить из графа любую вершину, у которой оба непосредственных преемника изоморфны. Легко показать, что поиюриое применение операций слияния и удаления в любом порядке к двоичному решающему дереву булевой функцнн или к лю- Клю н цирож челне) 0'ейш бому полученному нэ него графу до тех пор, пока вье нэбытечнгюти не булуг устранены (т.е. ни С!, нн С2 не могут быть дыме применены), приводит к редуцированному представлению этой функции, которое н назывмтпг бинарной решоюыий дгам/кпсногд Мрмы / / / млеет 1ьтату ш ре- ме). гмом пбыевой опе- И1фм оме- 01мрмвв Ся: уяввнве Рнс 9З.
Олервкни Кн)все преобразования семвнгвчеаэго переев в ВОР Ключевмм требованием к ВОР является требование упорядоченности редуцированной бинарной решающей диаграммы. В редуцированной упорддо. чениой бинарной решмощей диаграмме (Кейпсеб Осбек Вшму Оесмюп Овйшш, КОВРО) последовательшкть пометок переменных функции на всех ня в лю- .е. ре'твунуг случае 1Е ВЕР- ю два кошей 1Е ВЛ- умень тор- юмеи со ;я де- ~ вор. фмй" Ь.
1 Овврецвв СП свами .г г г г г г дов Глеее в Рнс.9.4. В00, ио не КОВ00 Винер» в базис путях даскна идти в любом, но одном и том же глсбавьном передке, н на одном пути шременнме не могут повторяться. Например, рис. 9.4 представляет бинарную решающую диаграмму. которая не упорядочена: на разных путях ст корневой вершины к шключительной вершние переменные встречмотсз в ратном порядке. Обычно КОВ00 называют просто В00: при использовании термина В00 обычно понимается, по соответствующий граф и редуцирован, н упорядочен в соответствии с некоторым зафиксированным порядком переменных.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
