トップ «前の日記(2010-07-31) 最新 次の日記(2010-08-14)» 月表示 編集

日々の流転


2010-08-10 [長年日記]

λ. ICFPC2010のゲートの関数を他のソルバで求める

今年の The ICFP Programming Contest 2010 に参加したとき には、ゲートの関数を求めるのに Alloy Analyzer を使った。 Alloy を使った本質的な理由はあまりなくて、たまたま使い慣れていていたことで、解を列挙する機能があったことが大きい。 なので、正直どのソルバーを使っても似たようなものだろうと思っていた。

そこで、どうせなので他のソルバーでも試してみることに。 まず、SMTソルバーのYices(1.0.28)とCVC3(2010-07-11)に以下をそれぞれ食わせてみたところ……結果はいずれもunknownだった。 関係・関数も量化も有限領域上に対してしか使っていないので、最悪でも全部を基礎化(grounding)して、bit blasting すれば解けるはずなのに……これはかなりガッカリ。

(追加するかも)