彼女は悩んでいた。成績が良くないのだ。両親に無理を言って全寮制の学校に入学したものの、彼女の才能は一向に開花することはなかった。あるいは才能など元々なかったのかもしれないが、それはできるだけ考えたくない可能性だった。
そこで彼女が頼ったのは、インターネット上で見つけた怪しげな脳力トレーニングの教材だった。SAT-EN-3 (SATisifiability problem for Enhancement of Neuron: version 3) と銘打つその学習メソッドによると、充足可能性問題のようなもののインスタンスをひたすら手で解くことによって、計算力が向上し、引いては論理的思考力・直感力・想像力も豊かになり、部活動でも活躍できて恋愛もうまくいくのだという。さすがに最後の2つは眉唾ものじゃないかな、と彼女は思ったが、ソロバンや百マス計算のような例もあることだ。暗算が得意になったら儲けものかな、ぐらいの気楽さで、彼女はこの教材に取り組んでみることにした。
SAT-EN-3では、加法標準形で表される論理式の各変数に適切に割り当て、論理式の値を真にすることができるかどうか判定しなければならない。ちなみに、1つ以上の変数 (または、その否定) の論理積を 節 (clause) と呼び、いくつかの節の論理和で表される論理式のみが加法標準形に従っている。一般に充足可能性問題といえば論理式は乗法標準形で表されるが、SAT-EN-3では加法標準形であることに注意せよ。
彼女はしばらく SAT-EN-3 の問題集に取り組もうとして、ふと思い直した。問題集にお金を払うぐらいなら、プログラミングが得意な親友にパフェでもご馳走して、 SAT-EN-3 の問題を生成し、解くプログラムを書いてもらおう。そうすれば問題も解答もいくらでも手にはいるじゃないか。
こうして彼女の親友であるあなたは、SAT-EN-3を解くプログラムを書くことになったのである。
入力は複数のケースからなる。 各ケースは以下のフォーマットで与えられる。
expression
入力の終わりは"#"からなる行によって与えられる
expressionは以下のBNFに従う。
ここでは文字列リテラルを""を用いて囲んでいる。
実際の入力に""は含まれない。
また入力には余計な空白は含まれていない。
<expression> ::= "("<clause>")" | "("<clause>")|("<expression>")"
<clause> ::= <literal>"&"<literal>"&"<literal>
<literal> ::= <variable> | "~"<variable>
<variable> ::= [a-z]|[A-z]
expressionの長さは500文字を超えない。
テストケースの数は1100個を超えない。
与えられた式を満たす変数の割り当てが存在するのならばyesを、そうでなければnoを出力せよ。
(B&B&f)|(~d&~i&i)|(~v&i&~V)|(~g&~e&o)|(~f&d&~v)|(d&~i&o)|(g&i&~B)|(~i&f&d)|(e&~i&~V)|(~v&f&~d) (S&X&~X) #
yes no
The University of Aizu Programming Contest 2011 Summer
原案: Tomoya Sakai
問題文: Takashi Tayama