https://plus.google.com/100215187201873478127/posts/MCnPteDpMax で書いたのは、scip-maxsatがあるインスタンスで間違った答えを返すという問題で、二転三転したが、とりあえず解決したかなぁ。

たまたま手元にあったscip-2.1.1で解いたら正しい(と思われる)答えが出たので、これは自分のコードの問題かと思って色々調べまわる。

が、scip-maxsatにリンクしてあるscip-3.3.1を単体で実行しても同じ間違った答えが得られることが判明。

ただ、問題が結構極端な問題ではあるので数値計算上の問題かもしれないと思って、これは直しようがないかもなぁ……

とりあえず、SCIPのメーリングリストで聞いてみたら、presolverにバグがありそうで gate extractor というpresolverを向こうにすると正しい答えが得られるという情報が。

最終的には gate extractor 自体のバグではなく、それによって得られた制約を扱う制約ハンドラ(cons_and)の方に問題があったらしく、それを修正してもらえた。

Max-SAT Evaluation 2013 のサイトから修正版を再投稿しようと思ったら、投稿できなくなってた。 とりあえずオーガナイザにメールで送っておいたけれど、これまでも2回バグを知らせてもらって再投稿させてもらっていたし、流石にもう時間切れということだろうなぁ。 差し替えて再実行してくれなくてもまあ仕方ない。 ← 今ここ