cho.sh

직관주의 논리

아직 제출이 없습니다시간 제한2초메모리 제한128 MB

문제

바샤는 얼마 전 수학과 논리학의 한 갈래인 "직관주의"를 알게 되었다. 이 갈래의 중심 생각은 배중률, 즉 어떤 명제든 참이거나 거짓이라는 논리 법칙을 인정하지 않는 것이다. 바샤는 이 생각이 마음에 들었다. "고전 수학은 페르마의 마지막 정리가 참이거나 거짓이라고 말한다. 하지만 증명이나 반례를 보기 전까지 그 말은 나에게 아무 쓸모가 없다." 그래서 바샤는 직관주의자가 되었고, 연구를 비롯한 모든 일에 직관주의 논리를 쓰려고 한다. 그런데 이 논리는 고전 논리보다 훨씬 까다롭다. 바샤는 고전 논리에서는 성립하지만 직관주의 논리에서는 성립하지 않는 논리식을 자주 쓴다.

바샤는 이제 논리식이 성립하는지 자동으로 검사하는 프로그램을 갖고 싶어 한다. 방법을 설명한 책은 찾았지만 프로그래밍에 서툴러서 당신이 도와주기로 했다.

구성은 임의의 비순환 유향 그래프 X=(X,G)X = (\mathcal{X}, G)에서 출발한다. 여기서 X\mathcal{X}는 정점의 집합이다. 먼저 X\mathcal{X} 위에 부분 순서를 정한다. XX 안에 xx에서 yy로 가는 경로(길이가 00이어도 된다)가 있으면, 그리고 그때만 x≤yx \le y로 쓴다. 다음으로 X\mathcal{X}의 모든 부분집합을 모은 것을 B\mathcal{B}라 하고, B\mathcal{B}의 원소 가운데 서로 다른 두 원소 xx, yy가 언제나 비교 불가능한(x≤yx \le y도 y≤xy \le x도 아닌) 집합 α⊆X\alpha \subseteq \mathcal{X}만 모은 것을 H⊂B\mathcal{H} \subset \mathcal{B}라 한다. H\mathcal{H}에는 공집합과 원소가 하나인 부분집합이 언제나 들어 있다.

이제 사상 Max:B→H⊂BMax : \mathcal{B} \to \mathcal{H} \subset \mathcal{B}를 정의한다. M⊆XM \subseteq \mathcal{X}이면 Max(M)={x∈M:¬∃y∈M, x≠y, x≤y}Max(M) = \{x \in M : \neg \exists y \in M,\ x \ne y,\ x \le y\}, 곧 MM의 극대 원소를 모두 모은 집합이다.

H\mathcal{H} 위의 연산은 다음과 같다. α,β∈H\alpha, \beta \in \mathcal{H}일 때

α∧β=Max(α∪β)\alpha \wedge \beta = Max(\alpha \cup \beta)

α∨β=Max({x∈X:∃y∈α, ∃z∈β, x≤y, x≤z})\alpha \vee \beta = Max(\{x \in \mathcal{X} : \exists y \in \alpha,\ \exists z \in \beta,\ x \le y,\ x \le z\})

α⇒β={x∈β:¬∃y∈α, x≤y}\alpha \Rightarrow \beta = \{x \in \beta : \neg \exists y \in \alpha,\ x \le y\}

0=Max(X),1=∅0 = Max(\mathcal{X}), \qquad 1 = \varnothing

¬α=(α⇒0),α≡β=((α⇒β)∧(β⇒α))\neg \alpha = (\alpha \Rightarrow 0), \qquad \alpha \equiv \beta = ((\alpha \Rightarrow \beta) \wedge (\beta \Rightarrow \alpha))

논리식은 다음 기호로 이루어진다.

  • 상수 11과 00
  • 변수: AA부터 ZZ까지의 대문자
  • 괄호: EE가 논리식이면 (E)(E)도 논리식이다.
  • 부정: EE가 논리식이면 ¬E\neg E도 논리식이다.
  • 논리곱: E1∧E2∧⋯∧EnE_1 \wedge E_2 \wedge \dots \wedge E_n. 논리곱은 왼쪽에서 오른쪽으로 계산한다. 즉 E1∧E2∧E3=(E1∧E2)∧E3E_1 \wedge E_2 \wedge E_3 = (E_1 \wedge E_2) \wedge E_3이다.
  • 논리합: E1∨E2∨⋯∨EnE_1 \vee E_2 \vee \dots \vee E_n. 계산 순서는 논리곱과 같다.
  • 함의: E1⇒E2E_1 \Rightarrow E_2. 앞의 두 연산과 달리 오른쪽에서 왼쪽으로 계산한다. 즉 E1⇒E2⇒E3E_1 \Rightarrow E_2 \Rightarrow E_3은 E1⇒(E2⇒E3)E_1 \Rightarrow (E_2 \Rightarrow E_3)을 뜻한다.
  • 동치: E1≡E2≡⋯≡EnE_1 \equiv E_2 \equiv \dots \equiv E_n. 이 식은 (E1≡E2)∧(E2≡E3)∧⋯∧(En−1≡En)(E_1 \equiv E_2) \wedge (E_2 \equiv E_3) \wedge \dots \wedge (E_{n-1} \equiv E_n)과 같다.

위 목록은 우선순위가 높은 연산부터 낮은 연산까지 차례로 적은 것이다.

논리식 EE에 들어 있는 변수 자리에 H\mathcal{H}의 원소를 어떻게 넣어도 값이 항상 11이면, EE는 그래프 XX가 정하는 모형에서 유효하다고 한다. 그렇지 않으면 유효하지 않다고 한다.

그래프 XX와 논리식 여러 개가 주어진다. 각각이 유효한지 판정하라.

입력

입력은 테스트 케이스 여러 개로 이루어지고 파일 끝에서 끝난다.

각 테스트 케이스의 첫 줄에는 XX의 정점 수 NN(1≤N≤1001 \le N \le 100)과 간선 수 MM(0≤M≤5 0000 \le M \le 5\,000)이 공백 하나를 사이에 두고 주어진다. 다음 MM개의 줄에는 각각 ii번째 간선의 시작점 sis_i와 끝점 tit_i가 주어진다. 그다음 줄에는 처리할 논리식의 개수 KK(1≤K≤201 \le K \le 20)가 주어지고, 이어지는 KK개의 줄에 논리식이 한 줄에 하나씩 주어진다.

논리식은 0, 1, A ... Z, (, ), ~, &, |, =>, = 토큰으로 이루어진 문자열이다. 뒤의 다섯 토큰은 차례로 ¬\neg, ∧\wedge, ∨\vee, ⇒\Rightarrow, ≡\equiv를 뜻한다. 토큰 사이에는 공백이 얼마든지 들어갈 수 있다. 한 줄의 길이는 254254자를 넘지 않으며, 입력에 주어지는 논리식은 모두 문법에 맞다. 또한 H\mathcal{H}의 원소 개수 H=∣H∣H = |\mathcal{H}|는 100100을 넘지 않고, jj번째 논리식에 쓰인 서로 다른 변수의 개수를 v[j]v[j]라 할 때 ∑1≤j≤KHv[j]≤106\sum_{1 \le j \le K} H^{v[j]} \le 10^6이다.

출력

각 테스트 케이스마다 KK개의 줄을 출력한다. jj번째 줄에는 jj번째 논리식이 유효하면 valid를, 유효하지 않으면 invalid를 출력한다.