OK_metodichka_part_2 (1132797), страница 5
Текст из файла (страница 5)
, Fn ) и Fb 00 = F00 (F1 , . . . , Fn ), которое нагде Fзывается подстановкой для тождества t.Напомним, что формулы, полученные в процессе индуктивного построения (см. §1 данной главы и §1 главы 1) формулы F, называются ее подформулами. Из определений следует, что для формул имеет место так называемый принципэквивалентной замены. Это означает, что если подформулуb 0 (подформулу Fb 00 ) формулы F заменить, учитывая тождеFb 00 (соответственно Fb 0 ),ство bt, эквивалентной ей формулой Fто полученная в результате такой замены формула F̌ будетэквивалентна формуле F, то есть будет справедливо тождествоť : F = F̌.Указанный переход от F к F̌ (от t к ť) будем записыватьв виде однократной выводимости вида F 7→ F̌ (соответственte в результате прино t 7→ ť). Аналогичный переход от F к F28Глава 2.
Основные классы управляющих системменения одного из тождеств системы τ (нескольких последовательных применений тождеств из τ ) будем записыватьв виде однократной (соответственно кратной) выводимостиe (соответственно F |⇒ F).e При этом считается,вида F 7→ Fττчто тождествоeet: F=Fвыводится из системы тождеств τ , и этот факт записывается в виде выводимости τ 7→ et или τ |⇒ et в зависимости отe бучисла использованных переходов. Переход вида F |⇒ Fτдем называть также эквивалентным преобразованием форe на основе системы тождеств τ . Замулы F в формулу Feметим, что в силу обратимости ЭП, из выводимости F |⇒ Fτe |⇒ F.
Система тождествследует обратная выводимость Fττ называется полной для ЭП формул над Б, если для любых двух эквивалентных формул F0 и F00 над Б имеет местовыводимость F0 |⇒ F00 .τРассмотрим, в частности, систему, которая состоит изтождествtM& : (x1 · x2 ) = x1 ∨ x2 ,tM∨: (x1 ∨ x2 ) = x1 · x2 ,tM¬ : (x1 ) = x1— тождеств де Моргана для конъюнкции, дизъюнкции и отрицания соответственно, а также тождестваtПK1,& : x1 (x2 ∨ x2 ) = x1 ,— тождества подстановки константы 1 = x2 ∨ x2 в конъюнкцию (см.
тождества (2.2) из главы 1). Пример ЭП формул§3. Эквивалентные преобразования формул29из UΦ с помощью этой системы тождеств дает следующаяцепочка выводимостей:x1 (x2 x3 ∨ x2 ∨ x3 ) 7→ x1 (x2 x3 ∨ x2 · x3 ) 7→ x1 .tM&tΠK1,&(3.1)Формулы, получающиеся друг из друга эквивалентнымипреобразованиями на основе тождеств коммутативности tK&AAи tK∨ , а также тождеств ассоциативности t& и t∨ для конъюнкции и дизъюнкции соответственно (см. §2 главы 1), называются подобными. Легко видеть, что подобные формулы получаются друг из друга перестановкой аргументов иизменением порядка выполнения однотипных двуместныхбазисных операций, образующих соответствующую многоместную операцию, и поэтому могут отличаться друг от друга только глубиной.Заметим, что сложность характеризует время вычисления формулы на одном процессоре, а глубина — время ее параллельного вычисления на неограниченном числе процессоров.
Поэтому оптимизация подобных формул по глубинеявляется частным случаем «распараллеливания» вычислений.Формулы из UΦ можно оптимизировать также по числуотрицаний с помощью эквивалентных преобразований на осMMнове тождеств де Моргана tM¬ , t& , t∨ и преобразований подобия. Тождество tM¬ используется при этом для устранениянескольких последовательных вхождений ФС ¬ в оптимиMзируемой формуле, а тождества tM& , t∨ — для выполненияпереходаF0 = F1 ◦ · · · ◦ Ft = (F1 · · · Ft ),где (◦, ) ∈ {(&, ∨), (∨, &)} и t > 2, во всех ее максимальных по включению подформулах вида F0 , формируемых спомощью преобразований подобия.Формула, в которой все ФС ¬ встречаются только надБП, называется формулой с поднятыми отрицаниями.
Лег-30Глава 2. Основные классы управляющих системко видеть, что с помощью тождеств де Моргана любую формулу из UΦ можно преобразовать в формулу с поднятымиотрицаниями. Заметим, что преобразования подобия и эквивалентные преобразования формул на основе тождеств деМоргана не изменяют ранг этих формул и, следовательно,число ФС {&, ∨} в них.Определим альтернирование Alt (F)) формулы F с поднятыми отрицаниями как максимальное число измененийтипов ФЭ & и ∨ в цепях дерева, соответствующего формулеF.
Заметим, что альтернирование ЭК или ЭД равно нулю,а альтернирование любой (отличной от ЭК и ЭД) ДНФ илиКНФ равно 1.Теорема 3.1. Для любой формулы F с поднятыми отрицаниями из UΦ существует подобная ей формула F̌ такая,чтоD F̌ 6 dlog (L (F) + 1)e + Alt (F) .(3.2)Доказательство.
Доказательство проведем индукцией порангу формулы F. Если R (F) = 1, то формула F имеет видF = xσi , σ ∈ B, и сама удовлетворяет неравенству (3.2).Пусть неравенство (3.2) справедливо для любой подформулы F0 такой, что R(F0 ) 6 a−1, где a > 1, и пусть формулаF имеет ранг a. Представим формулу F в виде:F = Φ (F1 , . .
. , Ft ) ,где t > 2, формула Φ(y1 , . . . , yt ) при некотором ◦, ◦ ∈ {&, ∨},имеет вид y1 ◦ . . . ◦ yt , а альтернирование подформул F1 , . . .. . . , Ft формулы F не больше, чем a0 , где a0 = max{0, (a − 1)}.Положимd = dlog (L (F) + 1)e + a − a0и di = dlog (L (Fi ) + 1)e ,где i = 1, .
. . , t, а затем для каждой формулы Fi построимпо индуктивному предположению подобную ей формулу F̌i§3. Эквивалентные преобразования формул31такую, чтоD F̌i 6 di + a0 .Заметим, что при этомtX2di 6 2d .(3.3)i=1Действительно, если a − a0 = 1, тоd2 > 2 (L (F) + 1) =tX2 (L (Fi ) + 1) >i=1tX2di ,i=1а если a = a0 = 0, то F = xσ1 1 ◦ · · · ◦ xσt t и, следовательно,tXi=12di=tX(L (xσi i ) + 1) = L (F) + 1 6 2d .i=1Заметим также,что перенумерацией формул F̌i , i = 1, . . . , t,можно добиться выполнения неравенств:d1 > d2 > · · · > dt .(3.4)Пусть теперь Φ0 — формула вида y1 ◦ · · · ◦ y2d , которой соответствует полное двоичное d-ярусное дерево, а формула Φ00 получается из Φ0 удалением последних q, где q =2d − 2d1 − · · · − 2dt и q > 0 в силу , вхождений БП вместес теми ФС, которые с ними связаны.
В силу (3.4) первые 2d1вхождений БП в Φ00 составляют подформулу Φ1 , которойсоответствует полное двоичное d1 -ярусное дерево, содержащее 2d1 вхождений БП в Φ00 , следующие 2d2 вхождений БП вΦ00 — подформулу Φ2 , которой соответствует полное двоичное d2 -ярусное дерево, и так далее, вплоть до последних 2dtвхождений БП в Φ00 , составляющих подформулу Φt , которойсоответствует полное двоичное dt -ярусное дерево.32Глава 2. Основные классы управляющих системОбозначим через F̌ формулу, которая получается из Φ00заменой подформулы Φi на формулу F̌i , i = 1, . . . , t. Заметим, что F̌ подобна F, имеет глубину не больше,чемd + a0 = dlog (L (F) + 1)e + a,и поэтому удовлетворяет неравенству (3.2).Теорема доказана.Следствие 1. Для любой ЭК или ЭД Kсуществует подобная формула Ǩ такая, чтоD Ǩ = dlog (L(K) + 1)e ,(3.5)которая, в силу леммы 2.1, минимальна по глубине.Следствие 2. Для любой ДНФ или КНФ A существуетподобная ей формула Ǎ такая, чтоD Ǎ 6 dlog (L (A) + 1)e + 1.Замечание.
Доказательство теоремы дает индуктивный метод оптимизации формул с поднятыми отрицаниями по глубине с помощью преобразований подобия.§4Полнота системы основных тождеств для эквивалентных преобразований формул базиса {&, ∨, ¬}В данном параграфе будем рассматривать только формулынад базисом Б0 , называя их просто формулами.
Заметим,что имеют место (см., в частности, §2 главы 1, а также §3)следующие тождества ассоциативностиtA◦ : x1 ◦ (x2 ◦ x3 ) = (x1 ◦ x2 ) ◦ x3 ,§4. Эквивалентные преобразования формул33тождества коммутативностиtK◦ : x1 ◦ x2 = x2 ◦ x2и тождества отождествления БПtOΠ: x ◦ x = x,◦где ◦ ∈ {&, ∨}, тождества дистрибутивности «◦» относительно «»tD◦, : x1 ◦ (x2 x3 ) = (x1 ◦ x2 ) (x1 ◦ x3 )и тождества («правила») де МорганаtM¬ : (x1 ) = x1 ,tM◦ : (x1 ◦ x2 ) = (x1 ) (x2 ) ,где (◦, ) ∈ {(&, ∨) , (∨, &)}, тождества подстановки констант1ΠKtΠK0,& : x1 (x2 · x2 ) = x2 · x2 , t1,& : x1 (x2 ∨ x2 ) = x1 ,tΠK0,∨ : x1 ∨ x2 · x2 = x1 ,tΠK1,∨ : x1 ∨ (x2 ∨ x2 ) = x2 ∨ x2 ,а также тождество поглощенияtΠ : x1 ∨ x1 x2 = x1 ,тождество обобщенного склеиванияtOC : x1 x2 ∨ x1 x3 = x1 x2 ∨ x1 x3 ∨ x2 x3и другие.Примером ЭП формул с помощью введенных тождествявляется ЭП (3.1).
Докажем, далее, что M M K M t& , t¬ |⇒ tMиt& , τ|⇒ tK∨∨ ,1В отличие от тождеств (2.1)–(2.2) главы 1 данные тождества подстановки констант ориентированы на базис Б0 , где роль константы 0(константы 1) играет формула вида xi · xi (соответственно xi ∨ xi ).34где τ MГлава 2. Основные классы управляющих системM M= tM& , t¬ , t∨ . Действительно,x1 ∨ x2 |⇒ x1 ∨ x2 7→ (x1 ) · (x2 ) 7→ x1 · x2tM&tM¬tM¬иx1 ∨ x2 7→ x1 ∨ x2 7→ x1 · x2 7→ x2 · x1 |⇒ x2 ∨ x1 .tM¬tM∨tK&MtM& , t¬Аналогичным образом доказывается, что OΠ M A M|⇒ tOΠ,|⇒ tAt& , τ∨∨ , t& , τ ΠK D ΠK M DM|⇒ tσ,∨ ,|⇒ t∨,& и tσ,& , τt&,∨ , τгде σ ∈ {0, 1}. Завершая примеры выводимостей, докажем,что ΠK DK OΠ|⇒ tΠ .t1,& , t&,∨ , tA∨ , t∨ , t∨Действительно,x1 ∨ x1 x2 7→ x1 (x2 ∨ x2 ) ∨ x1 x2 7→ x1 ((x2 ∨ x2 ) ∨ x2 )tΠK1,&tD&,∨|⇒ x1 ((x2 ∨ x2 ) ∨ x2 ) 7→ x1 (x2 ∨ x2 ) 7→ x1 .KtA∨ ,t∨tOΠ∨tΠK1,&ПоложимΠK ΠKM A K OΠ Dτ осн = tM& , t¬ , t& , t& , t& , t&,∨ , t1,& , t0,& ,Aτ A = tA& , t∨ ,Kτ K = tK& , t∨ ,OΠτ OΠ = tOΠ,& , t∨DDDτ = t&,∨ , t∨,& ,ΠK ΠK ΠKτ ΠK = tΠK0,& , t1,& , t0,∨ , t1,∨ ,τeосн = τ M , τ A , τ K , τ OΠ , τ D , τ ΠK , tΠ .§4.