베스 도표

주어진 명제(불리언) 논리식 $E$ 가 항진식인지, 즉 변수들에 어떤 불리언 값을 대입하더라도 항상 $\mathbf{1}$(참) 로 평가되는지를 판별하는 프로그램을 작성하세요. 만약 $E$ 가 항진식이 아니라면, 어떤 대입에서는 $\mathbf{0}$(거짓) 이 되며, 그러한 반례 대입도 함께 출력해야 합니다.

가장 단순한 방법은 $k$ 개의 변수에 대해 $2^k$ 가지 대입을 모두 시도하는 것이지만, $k$ 가 크면 사실상 불가능하고 사람이 논리식을 추론하는 방식과도 다릅니다. 고전적인 베스 도표(Beth tableau, 의미론적 도표) 방법은 반례를 직접 찾아 나갑니다. 참으로 만들려는 부분식들과 거짓으로 만들려는 부분식들, 두 묶음을 유지하면서 각 복합식을 가장 바깥 연산자를 기준으로 계속 분해합니다. 모든 분기가 모순(같은 식이 참과 거짓 양쪽으로 강제되거나, $\mathbf{0}$ 이 참으로, $\mathbf{1}$ 이 거짓으로 강제됨)에 도달하면 그 식은 항진식입니다. 반대로 모순 없이 살아남는 분기가 있으면 그것이 반례가 됩니다(참으로 강제된 변수는 $\mathbf{1}$, 거짓으로 강제된 변수는 $\mathbf{0}$). 올바른 방법이라면 무엇이든 사용해도 되며, 채점은 최종 출력만 확인합니다.

문법. 논리식은 다음과 같이 구성되며, 연산자는 우선순위가 높은 것부터 낮은 순으로 나열되어 있습니다.

• 상수 $\mathbf{1}$(참) 과 $\mathbf{0}$(거짓).
• 변수: 문자 A–Z 와 a–z. 대소문자를 구분하므로 A 와 a 는 서로 다른 변수입니다.
• 괄호: $E$ 가 논리식이면 $(E)$ 도 논리식입니다.
• 부정: $\neg E$.
• 논리곱 $E_1 \wedge E_2 \wedge \cdots \wedge E_n$ 은 왼쪽에서 오른쪽으로 계산합니다: $E_1 \wedge E_2 \wedge E_3 = (E_1 \wedge E_2) \wedge E_3$.
• 논리합 $E_1 \vee E_2 \vee \cdots \vee E_n$ 도 왼쪽에서 오른쪽으로 계산합니다.
• 함의 $E_1 \Rightarrow E_2$ 는 오른쪽에서 왼쪽으로 계산합니다: $E_1 \Rightarrow E_2 \Rightarrow E_3$ 는 $E_1 \Rightarrow (E_2 \Rightarrow E_3)$ 을 뜻합니다.
• 동치 $E_1 \equiv E_2 \equiv \cdots \equiv E_n$ 은 $(E_1 \equiv E_2) \wedge (E_2 \equiv E_3) \wedge \cdots \wedge (E_{n-1} \equiv E_n)$ 으로 정의됩니다.

각 연산자는 통상적인 진리표를 따릅니다: $\neg$ 는 논리 부정(NOT), $\wedge$ 는 논리곱(AND), $\vee$ 는 논리합(OR), $A \Rightarrow B$ 는 $\neg A \vee B$ 와 같고, $A \equiv B$ 는 $A$ 와 $B$ 의 값이 같을 때에만 참입니다.

논리식이 적힌 한 줄이 주어집니다. 논리식은 다음 토큰들로 이루어진 문자열입니다: 0, 1, 문자 A–Z 와 a–z, (, ), ~, &, |, =>, =. 마지막 다섯 토큰은 각각 $\neg$, $\wedge$, $\vee$, $\Rightarrow$, $\equiv$ 를 나타냅니다. 토큰 사이에는 공백이 몇 개든 올 수 있습니다. 한 줄의 길이는 최대 $1000$ 자이며, 논리식은 문법적으로 항상 올바릅니다.

정확히 한 줄을 출력합니다.

• 논리식이 항진식이면 true 를 출력합니다.
• 그렇지 않으면 false 를 출력합니다. 논리식에 변수가 하나라도 있으면 뒤에 : 를 붙이고 사전순으로 가장 작은 반례 대입을 이어서 출력합니다. 변수들을 문자 코드 오름차순으로 정렬하고(따라서 대문자가 소문자보다 앞섭니다), 논리식을 $\mathbf{0}$ 으로 만드는 모든 대입 중에서, 첫 번째 변수를 최상위 비트로 두고 $0 < 1$ 로 볼 때 비트열이 가장 작은 대입을 고릅니다. 대입은 변수=값 쌍을 , (쉼표와 공백) 로 이어 붙여 적으며, 예를 들어 false: A=0, B=1 과 같습니다. 변수가 하나도 없으면 그냥 false 만 출력합니다.