Метод двійкових діаграм рішень

Нехай F, F₀, F₁ – формули. Розгалуженням називається вираз виду FÞF₁,F₀, який визначається так: FÞF₁,F₀=(FÙF₁)Ú(ØFÙF₀). Формула F називається перевірним виразом, Þ – оператором розгалуження, F₁,F₀ – гілками розгалуження. Будемо називати розгалуження формулою.

З наведеного означення випливає, що логічні зв’язки Ù, Ú, Ø, ®, « можуть бути виражені через оператор розгалуження й логічні константи 0 та 1 таким чином, що: а) перевірні вирази є атомами, б) атоми зустрічаються лише у перевірних виразах. Дійсно, маємо: ØР=(РÞ0,1); PÙQ=PÞ(QÞ1,0),0; Р«Q=PÞ(QÞ1,0),(QÞ0,1); PÚQ=PÞ1,(QÞ1,0); P®Q=PÞ(QÞ1,0),1. Зазна-чимо також, що кожна формула F може бути записана у вигляді FÞ1,0.

Формула F є у нормальній формі розгалуження (нфр), якщо F побудована лише з атомів, операторів розгалуження й логічних констант 0 та 1, перевірними виразами є атоми, атоми зустрічаються лише як перевірні вирази.

Наприклад, формула PÞ(QÞ0,(RÞ0,1)),(RÞ(PÞ1,0),(QÞ1,0)) є у нфр, а формули (РÚQ)ÞR,0 та РÞ(RÙQ),(Q®ØP) – ні.

Позначимо F[0/P] (F[1/P]) формулу, що є результатом заміни у формулі F атома Р на 0 (1). Тоді формулу F, що містить атом Р, можна подати у вигляді

F=РÞF[1/P],F[0/P].                                      (1)

Користуючись цим співвідношенням (застосовуючи його спочатку до формули F, а потім до гілок розгалуження й т.д.), можна кожну формулу логіки висловлень привести до нфр. Нехай, наприклад, F=(P®ØQ)Ù(QÚR). Виберемо за перевірний вираз атом Р та застосуємо перетворення (1). Тоді гілки розгалуження мають вигляд F[1/P]=(1®ØQ)Ù(QÚR)=ØQÙ(QÚR), F[0/P]=(0®ØQ)Ù(QÚR)=QÚR, а F=PÞ(ØQÙ(QÚR)), (QÚR). Позначимо F₁= F[1/P], F₀=F[0/P]. Виконуючи далі підстановки 1 замість атома Q у F₁ й F₀ та 0 замість атома Q у F₁ та F₀, маємо:

F₁=QÞF₁[1/Q], F₁[0/Q]= QÞ(Ø1Ù(1ÚR)),(Ø0Ù(0ÚR))= QÞ0,R;

F₀=QÞF₀[1/Q], F₀[0/Q]= QÞ(1ÚR),(0ÚR)= QÞ1,R.

Оскільки R=RÞ1,0, то маємо: F= PÞ(QÞ0, (RÞ1,0)),(QÞ 1,(RÞ1,0)).

Назвемо орграфом упорядковану пару множин виду (V,E), де V – довільна непорожня множина, EÍV². Множина V називається множиною вершин орграфу, її елементи називаються вершинами, а множина Е називається множиною дуг орграфу, її елементи (якщо ця множина непорожня), називаються дугами. Якщо (u,v) – дуга орграфу, то вершина u називається початком, а вершина v – кінцем цієї дуги, а дуга (u,v) – інцидентною вершинам u та v. Напівстепенем виходу вершини u орграфу називається потужність множини дуг орграфу, для яких вершина u є початком. Вершина, напівстепінь виходу якої дорівнює 0, називається кінцевою. Орграф (V,E) називається позначеним, якщо задана деяка множина Р (множина позначок) й задано відображення h множини V у множину Р. Шляхом у орграфі (V,E) називається така скінченна послідовність вершин орграфу v₁,…v_n, що (v_i,v_i+1)ÎE, 1£i£n-1. Якщо у орграфі існує шлях виду v₁,…v_n, то будемо говорити, що вершина v_n досяжна з вершини v₁. Орграф (V,E) називається ациклічним, якщо у ньому не існує жодного шляху v₁,…v_n, такого що n³2 й v₁=v_n. Орграф називається кореневим, якщо у ньому існує єдина вершина, що не є кінцем жодної дуги, й з якої досяжна будь-яка інша вершина даного орграфу. Орграф, множина вершин якого скінченна, може бути поданий у вигляді діаграми. Щоб подати орграф у вигляді діаграми, треба для кожної його вершини вибрати точку на площині (різні вершини позначаються різними точками), позначити точку іменем вершини, для якої ця точка вибрана, й з’єднати ті пари точок u та v, для яких виконується (u,v)ÎЕ, відрізком лінії зі стрілкою, що вказує на точку v.

Двійковою діаграмою рішень (ДДР) називається ациклічний кореневий позначений орграф, у якому є одна чи дві кінцеві вершини (тобто вершини, напівстепені виходу яких дорівнюють нулю), що мають (різні) позначки 0 або 1, напівстепені виходу некінцевих вершин дорівнюють двом, на множині некінцевих вершин визначено функції var, low, high такі, що коли u – некінцева вершина, то її позначкою є var(u), а (u, low(u)) та (u, high(u)) – дуги, інцидентні вершині u. Областю значень функції var є деяка множина позначок, область значень функцій high, low – множина вершин ДДР.

Двійкова діаграма рішень називається упорядкованою (УДДР), якщо для усіх її шляхів між кореневою та кінцевою вершиною зберігається один і той самий лінійний порядок позначок некінцевих вершин. Двійкова діаграма рішень (упорядкована або ні) називається приведеною (П(У)ДДР), якщо для усіх її некінцевих вершин u, v виконується:

(var(u)=var(v))Ù(low(u)=low(v))Ù(high(u)=high(v))®u=v й low(u)¹high(u).

Визначимо рекурсивну процедуру побудови формули F^u, що визначається вершиною u деякої ПУДДР. Кінцева вершина визначає логічну константу, некінцева вершина u з позначкою Р визначає розгалуження, перевірним виразом якого є Р, а суміжні вершини визначають гілки розгалуження, тобто F⁰=0, F¹=1, F^u=var(u)ÞF^high(u),F^low(u).

За формулою у нфр очевидним чином можна побудувати орграф, який після злиття кінцевих вершин з однаковими позначками перетворюється на ДДР. На рис.1 зображено УДДР, що не є приведеною, бо вона містить дві надлишкові вершини, що позначені перевірними виразами х₁ та х₂. Діаграма на рис.2 є УДДР для формули х₁Úх₃ з однією надлишковою вершиною. Дуги виду (u,high(u)) зображено суцільними лініями, дуги виду (u,low(u)) – пунктирними.

Теорема 5. Для будь-якої формули F(A₁,…,A_n) логіки висловлень існує єдина ПУДДР з лінійним упорядкуванням позначок A₁<…<A_n, така що для кореневої вершини u F^u=F.

Рис. 2

Наведені результати забезпечують такий спосіб перевірки тавтологічності (суперечності) формули логіки висловлень. Побудуємо для даної формули F її нормальну форму розгалуження, вибравши певний лінійний порядок атомів (це можна зробити для будь-якої формули логіки висловлень). Потім за нфр побудуємо УДДР, при потребі здійснивши її приведення. Якщо результатом є діаграма, що складається з однієї кінцевої вершини, яка має позначку 1 (0), то формула F є тавтологією (суперечністю). Якщо побудована ПУДДР має некінцеві вершини, то формула F не є ні тавтологією, ні суперечністю, але має моделі.

Розглянемо формулу (х₁«y₁)Ù(x₂«y₂). Зафіксуємо лінійний порядок атомів: x₁<y₁<x₂<y₂. На рис.3 зображено ПУДДР даної формули. Діаграма показує, що формула не є тавтологією й не є суперечністю. За допомогою цієї діаграми можна побудувати моделі формули, наприклад, х₁=y₁=1, х₂=y₂=0.

Рис.1	Рис.2	Рис. 3

Доведення теореми 5 проведемо індукцією за кількістю n атомів у формулі F(A₁,…,A_n). Нехай n=0. Існує лише дві формули, що не містять атомів: тотожно істинна формула (1) й тотожно хибна формула (0). Оскільки будь-яка ПУДДР, що має хоча б одну некінцеву вершину, визначає формулу, яка не є логічною константою, то для кожної з констант існує лише одна ПУДДР: кінцева вершина з позначкою 1 для 1 та кінцева вершина з позначкою 0 для 0.

Нехай теорема правильна для усіх формул, що містять n атомів. Розглянемо формулу F(A₁,…,A_n+1), що містить n+1 атомів. Надаючи значення 0 або 1 першому атому (A₁), одержимо формули F₀ та F₁, що мають по n атомів: F_b(A₂,…,A_n+1)=F(b,A₂,…,A_n+1), bÎ{0,1}. Для цих формул виконується умова: F(A₁,A₂,…,A_n+1)=A₁ÞF₁(A₂,…,A_n+1),F₀(A₂,…,A_n+1). Оскільки F₀ (F₁) має n атомів, за припущенням індукції існує єдина ПУДДР, така що для кореневої вершини u₀ (u₁) F^u0=F₀ (F^u1=F₁). Розглянемо два випадки. Якщо ПУДДР з коренями u₀ та u₁ збігаються, то F₀=F₁=F. Отже, маємо ПУДДР для F, причому єдину. Якщо ПУДДР з коренями u₀ та u₁ не збігаються, то, згідно з припущенням індукції, F^u0¹F^u1. Побудуємо УДДР з коренем u так, що var(u)=A₁, low(u)=u₀, high(u)=u₁. Тоді F^u=A₁ÞF^u1,F^u0, а побудована діаграма є, очевидно, приведеною. За припущенням, F^u1=F₁ й F^u0=F₀, отже, F^u=F. Припустимо, що існує інша ПУДДР, скажімо, з коренем v, така що F^v=F. Тоді F^v має залежати від A₁, тобто F^v₀¹F^v₁, тому що інакше маємо суперечність: F₀=(F^v)₀=(F^v)₁=F₁. Згідно з порядком, заданим на множині атомів формули F, var(v)=A₁=var(u). З того, що F^v=F, випливає: F^low(v)=F₀=F^u0 й F^high(v)=F₁=F^u1. Отже, за припущенням індукції, low(v)=u₀=low(u) й high(v)=u₁=high(u). Оскільки діаграма є приведеною, то u=v. Теорему доведено.

 

Контрольні питання

1. Що таке розгалуження?

2. Що таке перевірний вираз?

3. Що таке нормальна форма розгалуження?

4. Які формули логіки висловлень можна подати у нормальній формі розгалуження?

5. Як подати логічні зв’язки Ù, Ú, Ø, ®, « за допомогою оператору розгалуження й логічних констант 0 та 1?

6. Що таке двійкова діаграма рішень?

7. Яка двійкова діаграма рішень називаєтья: а) упорядкованою, б) приведеною?

8. Як побудувати формулу у нфр за ПУДДР?

9. Як визначити за ПУДДР, побудованою за формулою F, чи є F:
а) тотожно істинною, б) тотожно хибною?

Задачі та вправи

І. Перевірити суперечність поданих формул: а) шляхом побудови днф,
б) методом Девіса й Патнема, в) методом резолюцій, д) шляхом побудови ПУДДР.

1. (ØPÚQ)ÙØQÙP                           2. (PÚQ)Ù(ØPÚQ)Ù(ØRÚØQ)Ù(RÚØQ)

3. (PÚQ)ÙØQÙ(ØPÚQÚØR)        4. (PÚQÚØR)Ù(PÚØQ)ÙØPÙRÙT

5. PÙQÙRÙSÙ(ØPÚØQÚØRÚØS) 6. (PÚØQ)Ù(ØPÚQ)Ù(QÚØR)Ù(ØQÚØR)

7. (PÚQ)Ù(RÚQ)ÙØRÙØQ          8. (PÚQ)Ù(PÚØQ)Ù(RÚQ)Ù(RÚØQ)

9. (AÚB®CÙD)Ù(DÚE®G)Ù(AÚØG)

10. (PÚQ)Ù(QÚR)Ù(RÚS)Ù(ØRÚØP)Ù(ØSÚØQ)Ù(ØQÚØR)

11. (A®Ø(BÙC))Ù(DÚE®G)Ù(G®Ø(HÚI))Ù(ØCÙEÙH)

12. (A®B)Ù(C®D)Ù(B®D)Ù(ØC®A)Ù(E®G)Ù(G®ØD)Ù(ØE®E)

13. (A®BÙC)Ù(D®BÙE)Ù((G®ØA)ÙH®I)Ù((H®I)®GÙD)ÙØ(ØC®E).

ІІ. Побудувати приклади суперечних множин диз’юнктів, для яких не існує вхідних виведень порожнього диз’юнкту.

IIІ. Знайти усі моделі формули F шляхом побудови: а) днф, б) ПУДДР.

1. (СÙ(ØАÚ(В®С)))®(ВÙС)     2. (A®(ØBÚC))Ù(C®A)

3. Ø(ØА«(ВÙС)ÚВ)                  4. (АÚØ(ВÚ(С«ØА)))

5. СÙ(Ø((ØАÚВ)®С))          6. АÙØ(С®Ø(ВÚА))

7. (СÚ(ØА«(ВÙС)))®А            8. Ø(АÚ(В«С))®(АÙС)

9. Ø(АÚВ)Ù((С«А)ÚВ)                 10. (ВÙ(А®Ø(СÚА)))«А.

IV. Нехай F – формула логіки висловлень. Як, використавши метод Девіса й Патнема, дізнатися, чи є F тавтологією? Чи можна встановити тавтологічниість формули F за допомогою методу резолюцій?

V. Чи однаковими є ПУДДР, побудовані за формулою (А1«В1)Ù(А2«В2) з використанням різних лінійних порядків на множині атомів (A1<B1<A2<B2 та А1<А2<В1<В2 відповідно)?

VI. Нехай S – множина диз’юнктів, до якої застосовне правило тавтології методу Девіса й Патнема, й S1 – результат застосування цього правила до S. Довести, що S суперечна Û S1 суперечна.

VII. Нехай S – множина диз’юнктів, до якої застосовне правило розщеплення методу Девіса й Патнема, й S1 та S2 – результат застосування цього правила до S. Довести, що S суперечна Û S1 та S2 суперечні.

VIII. Нехай S – множина диз’юнктів, до якої застосовне правило чистих літер методу Девіса й Патнема, й S1 – результат застосування цього правила до S. Довести, що S суперечна Û S1 суперечна.

IX. Нехай S – множина диз’юнктів, до якої застосовне правило однолітер-них диз’юнктів методу Девіса й Патнема, й S1 – результат застосування цього правила до S. Довести, що S суперечна Û S1 суперечна.

Х. Нехай існує доведення несуперечності формули F методом Девіса й Патнема. Сформулюйте правило побудови моделі F за цим доведенням.

 

⇐ Предыдущая12345678910Следующая ⇒

Поделиться: