부울 충족 가능성

부울 충족 가능성 문제(SAT)는 컴퓨터 과학에서 아주 어려운 문제로 알려져 있다. 부울 식이 하나 주어졌을 때, 변수에 true 또는 false를 일관되게 대입해서 식이 참이 되게 만들 수 있는지 판정하는 문제다. SAT는 NP-완전이고, 3-CNF 식으로 제한한 3-SAT도 NP-완전이다. 반면 2-CNF 식에 대한 SAT, 즉 2-SAT는 P에 속한다.

#SAT는 SAT를 확장한 문제다. 여기서는 대입이 가능한지 판정할 뿐 아니라 식을 참으로 만드는 대입이 몇 가지인지 센다. 이 문제는 2-CNF 식으로 제한해도 #P-완전이다. 이 문제에서 풀 것은 1-DNF 식에 대한 #SAT, 즉 #1-DNF-SAT다.

1-DNF 형태의 부울 식이 주어진다. 1-DNF 식은 절 하나 이상을 논리합(or)으로 이은 식이고, 각 절은 리터럴 정확히 하나로 이루어지며, 리터럴은 변수이거나 변수의 부정(not)이다.

형식적으로 정의하면 다음과 같다.

 ⟨formula⟩ ::= ⟨clause⟩ | ⟨formula⟩ ∨ ⟨clause⟩
  ⟨clause⟩ ::= ⟨literal⟩
 ⟨literal⟩ ::= ⟨variable⟩ | ¬ ⟨variable⟩
⟨variable⟩ ::= A . . . Z | a . . . z

식에 등장하는 모든 변수에 true와 false를 대입해서 식이 참이 되게 하는 방법이 몇 가지인지 구하라. 같은 변수가 여러 번 나오면 모두 같은 값으로 대입한다. 식에 나오지 않는 문자는 변수로 세지 않는다.

입력의 유일한 줄에 1-DNF 형태의 논리식이 주어진다. 길이는 1000자를 넘지 않는다. 논리 연산은 |(논리합)와 ~(부정)으로 나타낸다. 변수는 A부터 Z까지와 a부터 z까지이고, 대문자와 소문자는 서로 다른 변수다. 식에는 공백도, 위 문법에 없는 다른 문자도 들어 있지 않다.

주어진 식에 대한 #SAT의 답을 정수 하나로 출력한다.