혼 절(Horn Clause)

불리언 변수들의 집합과 그 변수들로 이루어진 불리언 식을 생각하자. 각 변수를 배정된 값으로 치환했을 때 식 전체가 참이 되면, 그 값 배정을 충족(satisfying) 배정이라고 한다. 충족 배정이 하나도 존재하지 않는 식을 충족 불가능(unsatisfiable) 하다고 한다.

일반적인 불리언 식의 충족 가능성을 다항 시간에 판정하는 알고리즘은 알려져 있지 않다(그러한 알고리즘이 존재하지 않는다는 것도 아직 증명되지 않았다). 충족 불가능 여부의 판정도 마찬가지다. 그럼에도 불구하고, 특정한 형태로 제한된 식들에 대해서는 이 질문들을 다항 시간에 답할 수 있다. 이 문제는 그러한 부류 중 하나를 다룬다.

리터럴(literal) 은 변수 $x$ 그 자체(양의 리터럴) 또는 그 부정 $\neg x$(음의 리터럴) 를 말한다. 절(clause) 은 하나 이상의 리터럴을 논리합(OR)으로 연결한 것이다. 혼 절(Horn clause) 은 양의 리터럴을 최대 한 개 포함하는 절이다.

임의의 혼 절 $\neg n_1 \lor \neg n_2 \lor \ldots \lor \neg n_k \lor p$ 는 함의(implication)로 다시 쓸 수 있다: $(n_1 \land n_2 \land \ldots \land n_k) \Rightarrow p$. 화살표의 왼쪽을 전건(antecedent), 오른쪽을 후건(succedent) 이라고 한다. 후건이 비어 있으면 상수 false 로, 전건이 비어 있으면 상수 true 로 간주한다.

이 문제에서 식은 하나 이상의 혼 절을 논리곱(AND)으로 연결한 것이다. 이러한 식의 충족 가능성은 다항 시간에 판정할 수 있다. 이를 판정하는 프로그램을 작성하라.

입력은 하나 이상의 식으로 이루어지며, 각 식은 한 줄에 하나씩 아래 문법에 따라 주어진다. 문법에서 [ X ] 는 X 가 생략될 수 있음을, { X } 는 X 가 0번 이상 나타날 수 있음을 뜻한다. 따옴표 안의 문자는 그 문자 자체를 나타낸다.

       <char> → 'A' | 'B' | ... | 'Z'
   <variable> → <char> {<char>}
<horn-clause> → '(' [<variable> {'&'<variable>}] '=>'<variable>')'
              | '(' <variable> {'&'<variable>} '=>' [<variable>] ')'
    <formula> → <horn-clause> {'&'<horn-clause>}

각 변수 이름은 대문자 A–Z 로 이루어진 비어 있지 않은 문자열이다. 각 식은 한 줄을 차지한다. 입력 전체의 길이는 $20,000$ 자를 넘지 않는다.

각 식에 대해 정확히 한 줄을 출력한다.

식이 충족 가능하면, 그 식의 최소 충족 배정(least satisfying assignment) 을 출력한다. 이는 모든 변수를 false 로 두고, 어떤 절이 요구할 때에만 해당 변수를 true 로 강제하여 얻는 유일한 배정이다. 충족 가능한 모든 혼 식은 이러한 최소 배정을 정확히 하나 가진다. 식에 등장하는 모든 변수를 각각 한 번씩, 변수 이름의 사전순 오름차순 으로 나열하되, 각 변수를 이름=true 또는 이름=false 형태로 쓰고 쉼표로 구분하며 공백은 넣지 않는다(예: A=true,B=false,C=false).

식이 충족 불가능하면 unsatisfiable 이라는 한 단어를 출력한다.