MiniSat という優秀な SAT ソルバがありますが、Opteron や Itanium2 といった 64bit CPU で正しい結果を返してくれないようなので、改造してみました。 MiniSat は C++ 版と C 版がありますが、C 版を対象にしています。
MiniSat 1.14.1 ではきちんと動くようになったみたいです。
テスト環境は
です。EM64T な Intel CPU でも問題ないとは思います。
MiniSat では各 Clause の Literal を int 型で管理し、int 型のポインタを用いて参照しています。 int 型のポインタを用いる場合 32bit CPU と 64bit CPU ではバイトオーダがずれるため、これが原因であると考え、 int の替わりに long を用いることにしました。
| → |
|
結果の妥当性は SAT-Race 2006 の Sample Benchmark Instances を用いてテストしています。
MiniSat 1.14 用のパッチを置いておきます。 このパッチを用いたことによる事故・不利益などにおきまして稲垣は責任を負いかねますので、自己責任の上で御利用下さい。 このパッチの件で MiniSat の作者に問い合わせるのは御遠慮願います。 結果の妥当性についてテストは行っていますが、パッチを当てたことによって結果が変化してしまう場合は御連絡いただければ幸いです。
MiniSat を展開したディレクトリで
$ patch -p0 < MiniSat-C_v1.14_64bit.patch
てな感じでパッチを適用してください。
>