증명 생성기
시간 제한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가 그 예이다. 더 이상 적용할 규칙이 없으면 변환이 끝난다. 변환은 항상 종료되며, 어떤 순서로 규칙을 적용하든 결과는 유일하다.
~~F → F~(*FS) → (+~F~(*S))~(+FS) → (*~F~(+S))(+F) → F(+s(+S)s') → (+sSs')(*F) → F(*s(*S)s') → (*sSs')(*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이면 아무것도 출력하지 않고 커서만 진행시킨다. 출력되는 각 증명은 한 줄의 맨 앞에서 시작하며, 문자들 사이에 공백이 없다.