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