Beth Таблиці
Вашій програмі потрібно перевірити правильність заданої логічної формули. Якщо формула E є некоректною (тобто оцінюється в 0 для деякого присвоєння булевих значень змінним), вам також потрібно знайти таке присвоєння значень.
Зазвичай такі завдання вирішуються шляхом перевірки всіх можливих присвоєнь значень змінним, що зустрічаються у E; якщо є k таких змінних, це вимагає розгляду 2^k таких присвоєнь. Звісно, це майже неможливо для великих значень k. Крім того, цей процес значно відрізняється від того, як люди зазвичай перевіряють (тобто доводять) логічні формули.
У цьому завданні вам потрібно реалізувати природний спосіб перевірки правильності логічних формул, заснований на так званих таблицях Бета. Цей спосіб перевірки правильності формул певною мірою моделює процес знаходження доказів або протилежних прикладів, що використовуються людьми, принаймні, короткий строгий доказ зазвичай можна отримати досить швидко з побудованих таблиць Бета.
Визначимо синтаксис розглянутих логічних формул:
Константи 1 і 0;
Змінні — літери від A до Z і від a до z;
Дужки — якщо E є формулою, то (E) є іншою;
Заперечення — ¬E є формулою для будь-якої формули E;
Кон'юнкція — E_1 ∧ E_2 ∧ ... ∧ E_n. Зверніть увагу, що кон'юнкція оцінюється зліва направо: E_1 ∧ E_2 ∧ E_3 = (E_1 ∧ E_2) ∧ E_3.
Диз'юнкція — E_1 ∨ E_2 ∨ ... ∨ E_n. Те ж саме зауваження застосовується.
Імплікація — E_1⇒E_2. На відміну від попередніх двох операцій, вона оцінюється справа наліво: E_1⇒E_2⇒E_3 означає E_1⇒(E_2⇒E_3).
Еквівалентність — E_1 ≡ E_2 ≡ ... ≡ E_n. Цей вираз за визначенням обчислюється наступним чином: (E_1 ≡ E_2) ∧ (E_2 ≡ E_3) ∧ ... ∧ (E_{n-1} ≡ E_n).
Операції перераховані від найвищого пріоритету до найнижчого.
Визначимо основну операцію складної формули E як операцію у E, яка виконується останньою (звісно, формули, що складаються лише з однієї константи або змінної, не мають основної операції). Також припустимо, що наша формула не містить операцій еквівалентності, оскільки ми завжди можемо замінити E_1 ≡ E_2 на (E_1⇒E_2) ∧ (E_2⇒E_1).
Тепер визначимо таблицю Бета як таблицю з двома стовпцями, в яких записані деякі формули. Порядок, в якому формули записані в стовпцях, і кількість разів, коли формула з'являється в стовпці, не мають значення: ми можемо припустити, наприклад, що всі формули в стовпці різні і що вони впорядковані лексикографічно.
Неофіційно лівий стовпець відповідає формулам, які ми хочемо, щоб були істинними, а правий стовпець — тим, які ми хочемо, щоб були хибними; весь процес можна розглядати як спробу створити протилежний приклад для даної формули E. Таблиця Бета вважається суперечливою, якщо якась формула E* зустрічається в обох стовпцях цієї таблиці, або якщо 0 зустрічається в лівому стовпці, або якщо 1 зустрічається в правому стовпці.
На кожному кроці процесу ми маємо колекцію таблиць Бета. Ми починаємо з однієї таблиці Бета з порожнім лівим стовпцем і правим стовпцем, що містить лише дану формулу E. Крок процесу полягає у виборі складної формули C з несуперечливої таблиці Бета з колекції та застосуванні правила, обраного основною операцією C та стовпцем (лівим або правим), в якому C знаходиться. У результаті деякі формули додаються до лівого або правого стовпця цієї таблиці Бета (або обох); звісно, якщо ці формули, які ми хочемо додати, вже там, таблиця Бета не зміниться, тому в цьому випадку ми кажемо, що відповідне правило є незастосовним. Є також деякі правила, які створюють дві копії оригінальної таблиці Бета і додають деякі формули в одну з цих копій і деякі інші в другу. У цьому випадку ми кажемо, що правило є незастосовним, якщо обидві таблиці Бета, отримані таким чином, вже були в колекції до застосування правила.
Процес зупиняється, коли жодне правило не є застосовним. Зверніть увагу, що всі формули, що зустрічаються у всіх таблицях Бета, будуть підформулами оригінальної формули, тому є лише скінченна кількість таблиць Бета, які можуть бути отримані, і, отже, лише скінченна кількість колекцій таблиць Бета може бути отримана. Тому процес повинен зупинитися в якийсь момент. Якщо в цей момент всі таблиці Бета в колекції є суперечливими, оригінальна формула E була доведена як коректна. Інакше, якщо τ є несуперечливою таблицею Бета з колекції, будь-яка змінна x, що зустрічається в E, повинна зустрічатися рівно в одному стовпці τ (вона не може зустрічатися в обох стовпцях, оскільки τ не є суперечливою; вона повинна зустрічатися принаймні в одному стовпці, оскільки інакше правило було б застосовним до найкоротшої формули в τ, що містить x). Тоді призначимо 1 всім змінним з лівого стовпця і 0 змінним з правого стовпця τ. Це дасть нам протилежний приклад для E, тобто присвоєння значень змінним, для якого наша оригінальна формула E оцінюється в 0.
Тепер перелічимо всі можливі правила. Вже було пояснено, що правило визначається основною операцією * формули C та стовпцем (лівим або правим), в якому C була знайдена. Ми будемо позначати ці правила як *, і *, де * є операцією (однією з ∧, ∨, ⇒ або ¬). Якщо * є бінарною, ми припускаємо, що C = A * B; інакше ми припускаємо C = ¬A.
Перелічимо правила, які не збільшують кількість таблиць (тобто вони просто додають деякі формули до стовпців вибраної таблиці Бета):
Це означає наступне: наприклад, якщо ми застосовуємо правило ⇒ до формули A⇒B у правому стовпці таблиці Бета, тоді ми повинні додати формулу A до лівого стовпця і B до правого стовпця цієї таблиці.
Наступні правила створюють дві таблиці Бета з однієї. Використовується подібна нотація, але для кожного правила показані дві таблиці Бета:
Ці три правила інтерпретуються наступним чином: якщо ми застосовуємо, наприклад, ∨ до формули A ∨ B у лівому стовпці таблиці Бета τ, ми повинні замінити τ двома копіями самої себе τ' і τ", а потім додати A до лівого стовпця τ' і B до лівого стовпця τ".
Вхідні дані
Єдиний рядок введення містить формулу, представлену у вигляді рядка, що складається з токенів '0', '1', 'A' ... 'Z', 'a' ... 'z', '(', ')', ' ', '', '|', '=>', '='. Останні п'ять токенів позначають ¬, ∧, ∨, ⇒ і ≡ відповідно. Токени можуть бути розділені довільною кількістю пробілів. Рядок міститиме не більше 1000 символів. Формула на вході буде синтаксично коректною.
Вихідні дані
Вихід повинен містити рівно один рядок. Виведіть просто "true", якщо формула є коректною, або "false" з подальшим присвоєнням змінних, яке робить формулу некоректною. Перерахуйте змінні в лексикографічному порядку. Дотримуйтесь зразка виходу якомога точніше.