논리식을 참으로 만드는 할당의 개수

입력으로 하나의 논리식이 주어진다. 논리식은 입력 변수 A부터 L까지, 상수 0과 1, 그리고 동치(⇔), 함의(→), 논리합(∨), 논리곱(∧), 부정(¬) 연산자로 이루어지며 다음 문법을 따른다.

<expression>  ::= { <implication> ⇔ }* <implication>
<implication> ::= <disjunction> | <disjunction> → <implication>
<disjunction> ::= <conjunction> | <disjunction> ∨ <conjunction>
<conjunction> ::= <term> | <conjunction> ∧ <term>
<term>        ::= A ... L | 0 | 1 | ¬ <term> | ( <expression> )

여기서 {X}*는 X를 0번 이상 반복함을 뜻한다. 연산자 우선순위는 낮은 것부터 높은 것 순으로 동치, 함의, 논리합, 논리곱, 부정이며, 함의(→)는 오른쪽 결합(right-associative)이다.

각 연산의 의미는 일반적인 정의를 따르되 동치만 예외이다. 한 식 안에서 나란히 이어진 여러 개의 동치 $a_1 \Leftrightarrow a_2 \Leftrightarrow \cdots \Leftrightarrow a_k$는 모든 인자의 값이 서로 같을 때에만 1이고, 그렇지 않으면 0이다.

12개의 변수 A부터 L까지에 각각 0 또는 1을 대입하는 방법은 모두 $2^{12} = 4096$가지가 있다. 이 4096가지 대입 중에서 논리식의 값이 1이 되는 경우의 수를 구하라.

첫 번째 줄에 논리식이 주어진다. 논리식의 길이는 최대 300,000자이다. 동치는 <=>, 함의는 ->, 논리합은 |, 논리곱은 &, 부정은 ~로 표기한다. 변수 A~L과 상수 0, 1은 그대로 쓴다. 논리식에는 공백이나 문법에 없는 다른 문자가 포함되지 않는다.

12개의 변수 A부터 L까지에 대한 $2^{12} = 4096$가지 대입 중에서, 논리식의 값이 1이 되는 대입의 개수를 정수 하나로 출력한다. 식에 등장하지 않는 변수도 0 또는 1을 자유롭게 가질 수 있으므로 개수에 포함된다.

우선순위 때문에 B&C|E는 (B&C)|E로 해석된다. 또한 F<=>(F)<=>F처럼 같은 값이 동치로 나란히 이어지면 세 인자가 항상 서로 같으므로 값은 언제나 1이다. 함의는 오른쪽 결합이므로 A->B->C는 A->(B->C)와 같다.