2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 60
Текст из файла (страница 60)
дпя представления мегабайтного изображения нужна булева функция от 23 переменных (поскольку ~ 1об(йе10 )1 23, и В00 функции от такого числа переменных абмчно легко предстахяяются в памяти компьютера. Очевншю, что эту технику легко рааширазь и на изобрюкения с несколькимн градашшмн серого цвета, и на шмтные.
Использование ВРР для ииформвшюввагв нюшка. Дяя представления информации в поисковых системах испаяьзуются инверзпроааннме списки, В работе 19б) обсуждааюя использованиа В00 дия сжатия ннформашш, аодсрхшщейся в инвертированных списках. Рна.9.18 демонстрирует идшо, обсу~кдаемую в этой работе. глвее а 001~ 001 О10 Рис. 9Л7. Компрессия шсбрнксняя: г) Вй!Г, прелставляюшш юсбрвяииве О1О стн 0111 100' 100 1О1 Ы01 Задача о расстановке ферзей. Одной из знаменитых задач на шахматной доске является ангача о восьми ферзях: расстыппь на шахматной доске $ ферзей тмс чтобы онн не били друг друга. Известно много способов реше- ния этой задачи, все они сводятся к организации перебора.
Дпя кюкдого термина в инвертированном файле хравмтся список номеров документов, в которых этот термин встречается. Тмь на рис. 9.10, а показано, что термин "!пгсыве" встречаегся в документехО, 2, 3,...,15, термин "!птегзюп" в докумензах 2, б, 7, ... и т. д. Пусть всего имеем 1б документов. Закодируем все докуменгы двоичными иодами. Документ 0 закодируем колом 0000, документ 1 — 0001 и т. д.
Для каждого термина построим булеву функцию от 4 аргументов. Эта функция будет равна 1 на двоичных наборах, которыми закодированы те дозументы„в которых этот термин встречается. Рнс. 9.18, б показывает тасую функцию лля термина "!пыпз1те". При большом числе документов хранить такую функцию удобно в форме ВОР (рис. 9.13, е). Этот подход существенно ускоряет обработку сложных запросов в больших БД, котла требуется выполнение булевых операций И, ИЛИ, НЕ и других над инвертированными списками. перов аман :нтов. м ко. улеву айвах, естся. баль- ВРР апро- ИЛИ, в пмой асеан МШФ- Рнс.
Р.!й. Испальтоввнне ВРР лля прелставленна . ннвертнрованных файлов: а) фрммент ннвертнраванного файла лля терминов; б) булава фуняпня ляя термина "пненя! те", в) ВРР зюй фуняпнн Для решения задачи без перебора построим булеву фушщео г', аргумеитамм которой являются 64 переменных .т г, г У н (1,...,8) . причем х г --1, если на 1-й пзрнэо~пали н г'-й вертикали стоит ферзь, н,т,ц =О, если ферм в этой позиции нет.
Функция / строится таким обрмом: ряли решс иогр чсни ЕСЛИ ферзь стоит в позиции (Г,)), ТО (х, ю) г О на)-йгорзпошалмнстфершй: (Лг з Кг тсв) И О на э'-й вертикали нетферзей: (Лгязякгсг хзг) И Слов ств03 сгеш попс нт. г О на С-Э диагонали нет ферзайг О на С-В диагонали иег ферзей: Л, ы, „,.,-*„„,,) И ( (Лызяз, гзгтг-ьяв,зяг тз.гьмз) )и Если роше с поь О на каждой горгпошвли есть ферзь: (Л, з (х, г ч х, з г с. н хш) ) . ные: дое г Конъюнкция всех этих формул двя всех 1, /н (1, ...,8) даст булаву функцию ,г" от 64 переменных, такую, что любая интерпретация <набор значений дво- ичных переменных), на которой Г" =1, булст решением проблемы. зады Решс Как ~ числ, поэм пии ~ Прзи Рассь цнй э Программирование в ограничениях. Программировзэее в ограничениях состоит не в описании алгоритма решенна задачи, а дмшвратняной спецификации допустимых состояний среды, которые задмотся набором отношений между параметрамн среды.
Формально постановка задачи в парадигме программирования в ограничениях формулируется следующим образом. Пусть на мншксстве переменных Х, ..., Х", обласшмн значений которых являются мнояиства О', ..., 0", 1 заданы ограничения Сг (Х', ..., Х" ), й н (1, ..., К) . Ограниченна аыражакпся уравнениями, неравенствами, логическими соотношенивмн и т. п. Требуется найти множество допустимых состояний среды, т.
е. такие наборы чисеэ мено являя кюы! часть набо1 Представление булевой функции от 64 двоичных переменных в любой другой форме, кроме ВОО, нереально. В то же время построение бинарной решаюшей диаграммы этой функции с испольюванием одмой из перечисленньш выше библиотек является простмм делом. Перечисление тех интерпретаций булевой функции, предсшвленной в ВОО, нв которых функция равна 1, является спшдартной операцией этих библиотек. шмн цию лру- 1 ре- леи- пре- «иях «фн- ший (а«, ..., ае) («гг и !уг) значений переменных Ал, ...,А'", которые удоаветво- ряли бы всем ограничениям одновременно.
Подобныезадачи возникают при решении задач планирования, проевтнровашш, щюгнознрования и др. В мо. нографни (169] этот класс задач называется "Задачи удоашмеорения ограничений (Сопя!пип«Зм!зуаспоп Рго!«!ешь, СЗР)". Слояаюсть решения задач этого класса обуславливаеюя огромным прос«рпяспюм поиске, в то время как вычислительные алгоригмы играют здесь второстепенную роль.
В качестве основного метода решения задач СЗР обычно исполь«уюттл эвриогнчесюю авгоригмы направленного поиска, аегорнтмы поиска с возврагами, методы, позволшощие сократить пространспю поискц ит. п. Если миакества !У, ..., !У«возможных значений переменных конечны, то решение шдачи СЗР может быль выпоянено без перебора и бев эвристнк с помощью построения булевых функций сяедующим образом, Вес во«пенные значения в калщой области й«закоднруем двончнымн наборамн. Ешш дое о«раниченне С«представим логической функцией гю а все мнолмизшз.
заданных ограничений продолжим конъюнкцией этих функций Р=й«у'„. Решенме задачи определится такими наборами кодировок, на кочорых Р "-1. Как правила, построенная таким образом функция Р зависит ст бояьпюго числа двоичных переменных, и обычные формы представления функции не позволяют решать сколько-нибудь сложные задачи СЗР.
Если булевы функции предетввнть в форма ВПВ, то решение задач может существенно упро-, ститься. Приыпр О.У Рассыотриы задачу нз обявстн СЗР. в которой нспслиованне булевмх функций заменяет поиск. Задача эта называется З11ВЗЕТ'-ЗИМ, оиа состоит в том, что дла заданного конечного множества З=(мп мз, ..., м«~ иатуразьных чисел и некоторого целого М необходимо найти подмнвкества таких элементов из 8, сумма которых равна М. Известно, что щкача ЗПВЗЕТ-3!1М является Хр-полной.
Построим булеву функцию Р, которая ммеет я двоичных входов и рвана! на таких двоичнмх наборах (х«, ..., х«), что ~, «(х хш 1=М. Рис 919показывает, как можно построить такую функцию. Ее основной составной частью явяяется функция 1«:(О, 11 -+(0,1!", которая кшкдому двоичному набору '(х«, ..., к«) ставит в соответствие двоичный код суммы чисел главе з 2.',м(х„хш,). Инымн словами, результатом функции Г является вектор двоичных функций (уп ..., уь') ллиной л, представляющий собой двоичные рюряды этой ~у~~~. Каждая фуиюзнв ~~ предсшялшт у-й ра~р~д двоичного кода сумм соответствующих целых из мнакестаа Я (здесь л — число двоичных разрядов, достаточное для представления в двоичном виде суммы всех чисел множесша Я). Функшяя Р опредехяетсв соотношением Р м,(У; ну;), где у; — 1-йрззряддвончного предсгавленгш числа М.
Пусть, например, множество Я такое: (шь шз, шз5 (4, 5, 12). Тогда вектор фушшнй Д, мшкет быть запал следующей таблицей истинности: Решение задачи БОВЗБТ-БОМ состопт в построении шкгорй булевых функпий (ун ..., У„) . Функции эти можно построить, перебирая все возможные йаборы двоичных переменных хн ..., хь и подсчитьпжя деоичимй код сумм ~,„м(х, хм„). Очевидно, что слшкность такого алгоритма зкспонеициаяьиа. Более эффективный алгоритм построения вектора функций у; состоит в построении их сразу в форме ВОР с последовательнмм увеличением числа аргументов функций.
Очевидно, что при числе вргумеигов 0 все функции Ун ..., 4 Раним О. ПУсть все фУнкции Ун ..., ~„Уже постРоены дда пеРемеиных кц ..., х,. Рассмотрим, как юменятся зтн функции при добзнлеиии еше ОДИОй ПЕРЕМЕННОЙ Хил. Главв в Очевидно, что добавление переменной «„< к числу переме1шмх вектора Функций /=(/и'-.„У„) — зто, фактически, учет возмолшости добавление очередного числа ш, < к комбинацнвм подмншкеств мномсства 8: все векторы значений функции / на тех наборах аргументов, в которых «„< -"1, дола<им быль увеличены на двоичный код числа эи, <. Пусть («„,...,«<)— код числа и,, Тогда для всех разрядов / = 1,..., л последовательно выполняем следующие вычисления; / («< .",«<ь<) гич л//(«< - «<) "фт~, "',«<) где функция /' («и,«<) определяется следующим образом.
Сначшш вы- чншшешл булава фунюшя переноса в следунлций разряд (она%идно, что перенос С, =0 Е Сгь<(«<, ...,«) еглп«/ =О,шв~~(««...,«<) «Сг(«<, ...,«) и<гаев//(«<,...,«<) ч Сг(«< ...т) Затем вычислветсв зта функция /Г («<, ...,«<) — значения /-го разряда сум- мы двух слапемых: двоичного кода чнсяа м<м и полученного ранее кода суммы /,, (х,хш„)< /;(«,, „«)-если «,=0 аю /,(х,,...,«<)ЕС,(х,, „«,) плече (~~(«<,..., «,)9Сг(«<, ..., «,)) Проведенные зксперименты показвш, что слакносгь посцюення такой функции растет полиномиалыю с ростом мощности мномества б до несколышх сотен. Иными словами, переборная задача Я!ВЕЕТ Я1М с про. страиством поиска порядка 10" при использовании ВПП маке~ быть решена за линейное время прн росте значения л до -1 00. Пр р 0.0 Классическим примером задач "в ограничениях" явлшотся буквенноарнфметическне головоломки.
Например, возьмем шутливую фразу: РЕШИ ЕСЛИ СИЛЕН Необходимо найти такую подстановку цифр вместо букв, при которой сумма двух первмх чисел равна тршъему. Разные буквы обозначают резные цифры, а старшие разряды чисел не равны нушо. Хата вуя " болю пайп букв. Двя < вии < кото! Доно< всех у Поскс стев! меннь Текин Конка иерем набор фуикц Опыт лепны завися Хозя задача формулируется просто, решение ее не совсем тривиально: действуя "в лоб", простым перебором, для решения этой задачи нужно рассмотреть более 60тысяч явривпгов рвзвичных подствновок, аккольку необходимо найти подстановку одной нз 1О различных цифр лля кязаой из 7 различных букв.
Для формализации огрвничшшй звдвчн рвсположим слоев заданной в уело. вин фразы в форме дпя слшкения "в сюлбик" с явной записью переносов, юторые обозначим с, (от англ, сшту — переносй тора ения пто. с, сз / ОΠ— перенос ю 1-го смоябьш Р Е Ш 'И + Е С Л Н С И Л Е Н Ограничение задачи макно зишсвть в виде линейных целочисленных уравнений, сввзмввющнх буквм из одпопз н того же столбце с учетом пере- иосоа'.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
