MaxSATソルバのダイエット

 ■SATソルバが使えない問題

に対して、構造を見直しメモリダイエットを行いました。およそ1/4程度にはなりました。

結果、instance23については、AL1でコンパイル出来るようになりました。このとき、25GB位の消費です。

しかし、instance24については、AL1コンパイルが出来ませんでした。およそ57GB位で、ストップします。TIME制約関係の消費が大きいようで、恐らくは、SATソルバの最大節数を超えているのだと思われます。（デバッグ用の開発環境が32GBなのでデバッグが出来ません）

SATソルバが使えないと、やはり痛いです。LPソルバから整数化を行うのにLPソルバだけで整数化しようとすると途方もない時間がかかります。現実的な時間内に解を得るには、なんとかして使えるような検討を行う必要があります。