SCIP http://scip.zib.de/ に簡単なフロントエンド https://github.com/msakai/scip-maxsat をつけて、Max-SAT Evaluation 2013 http://maxsat.ia.udl.cat/introduction/ に投稿しているのだけれど、主催者からバグの指摘がきて、でも手元のMacでは再現しない…… orz

ms_industrial/sean-safarpour/c5_DD_s3_f1_e1_v1-bug-gate-0.dimacs.seq.filtered.cnf という問題で、最後に出力した目的関数値は92187なのに、実際に出力しているモデルで違反制約の数を数えると88757だという問題。

手元のMacでは、出力される目的関数値は 540802 → 536828 → 536554 → 92187 → 88757 → 8 と遷移して終了していて、出力されるモデルでの実際の違反制約の数も8でちゃんと一致しているんだけれどなぁ。

節Ci: L1 ∨ … ∨ Ln を Ri + L1 + … + Ln ≧ 1 に置き換えて、R1 + … + Rm を最小化する問題としてSCIPに解かせているので、最適解以外では目的関数値が実際の違反制約の数よりも大きな値になり得るというのと、92187も88757も最適化途上で現れている目的関数値ということもあり、ひょっとして最適化がちゃんと終了していないのにSCIPgetStatusがSCIP_STATUS_OPTIMALを返しているのではないかという気がしているが、そんなことってあるのだろうか……