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" с последующим присвоением переменных, которое делает формулу некорректной. Перечислите переменные в лексикографическом порядке. Строго следуйте примеру вывода.