cho.sh

증명 생성기

시간 제한1초메모리 제한128 MB

문제

논리식은 그림 1(a)의 문법으로 만들어진다. 변수는 참/거짓 값을 나타내고, (+F1...Fn)은 논리식 Fi들의 논리합(disjunction), (*F1...Fn)은 논리곱(conjunction), ~F는 F의 부정을 뜻한다. 그림 1(b)의 문법에 맞는 논리식을 ACM 정규형(ACM Normal Form, ACMNF) 이라고 한다.

<formula>  ::= <variable> | ~<formula> | (+<formulae>) | (*<formulae>)
<variable> ::= 영어 소문자 하나
<formulae> ::= <formula> | <formula><formulae>

그림 1(a). 논리식의 일반 문법

<ACMNF_formula> ::= <term> | (+<terms>)
<term>          ::= <literal> | (*<literals>)
<terms>         ::= <term><term> | <term><terms>
<literal>       ::= <variable> | ~<variable>
<literals>      ::= <literal><literal> | <literal><literals>
<variable>      ::= 영어 소문자 하나

그림 1(b). ACMNF 문법

논리식은 아래 재작성 규칙으로 ACMNF로 변환한다. 여기서 F는 논리식, S는 비어 있지 않은 논리식의 나열, s와 s'은 비어 있을 수도 있는 논리식의 나열이다. 규칙 q → r을 적용한다는 것은 패턴 q와 일치하는 부분을 r로 바꾸는 것이며, 그림 2가 그 예이다. 더 이상 적용할 규칙이 없으면 변환이 끝난다. 변환은 항상 종료되며, 어떤 순서로 규칙을 적용하든 결과는 유일하다.

  1. ~~F → F
  2. ~(*FS) → (+~F~(*S))
  3. ~(+FS) → (*~F~(+S))
  4. (+F) → F
  5. (+s(+S)s') → (+sSs')
  6. (*F) → F
  7. (*s(*S)s') → (*sSs')
  8. (*s(+FS)s') → (+(*sFs')(*s(+S)s'))
(+(*(+~(*ab)) (+~a) )c)    -4→
(+(*(+ ~(*ab) )~a)c)       -2→
(+(* (+(+~a~ (*b) ))~a)c)  -6→
(+(* (+(+~a~b)) ~a)c)      -4 or 5→
(+ (*(+~a~b)~a) c)         -8→
(+(+(*~a~a)(* (+~b) ~a))c) -4→
(+(+(*~a~a)(*~b~a))c)      -5→
(+(*~a~a)(*~b~a)c)

그림 2. 논리식을 ACMNF로 변환하는 과정

공리 집합은 참인 변수들의 목록 (V1 V2 ... Vn)으로 주어지며, 목록에 없는 변수는 모두 거짓이다. 공리 집합 A 아래에서 논리식 F의 증명(proof) 이란, F의 ACMNF에 속한 항(term) 중 A 아래에서 참인 것을 말한다. 예를 들어 공리 (bc) 아래에서 (+(*(+~(*ab))(+~a))c)의 증명은 항 (*~a~a)와 c이다.

논리식 F, 공리 집합 A, 정수 k가 주어졌을 때, F의 ACMNF에 나타나는 순서대로 다음 k개의 증명을 출력하는 증명 생성기를 만들어라. 증명을 모두 소진하면 다시 첫 번째 증명부터 이어서 생성한다. 예를 들어 (bc) 아래에서 (+(*(+~(*ab))(+~a))c)의 첫 증명은 (*~a~a)이고, 이어서 세 개를 더 생성하면 c, (*~a~a), c가 된다. ACMNF에 똑같은 항이 여러 번 나타나면, 각 등장은 서로 다른 항으로 취급한다.

입력

입력은 여러 개의 데이터 집합으로 이루어지며 파일 끝(EOF)에서 종료된다. 각 데이터 집합의 형식은 다음과 같다.

F A k1 ... kn 0

여기서 n > 0이고, F는 논리식, A는 공리 집합, k1 ... kn은 0이 아닌 long 정수들이다. 값 0은 데이터 집합의 끝을 나타낸다. 토큰 사이에는 공백이 자유롭게 올 수 있다. 논리식은 최대 500자이고, 모든 ACMNF 항은 공백을 제외하고 최대 80자이다. 모든 입력은 형식에 맞다고 보장된다.

출력

각 데이터 집합마다 F의 증명들을 가리키는 하나의 커서를 유지하면서 ki를 순서대로 처리한다. 각 ki(i = 1 ... n)에 대해 다음 |ki|개의 증명을 생성하며 커서를 순환적으로 진행시킨다. ki > 0이면 그 |ki|개의 증명을 출력하고, ki < 0이면 아무것도 출력하지 않고 커서만 진행시킨다. 출력되는 각 증명은 한 줄의 맨 앞에서 시작하며, 문자들 사이에 공백이 없다.