Instance24 AL1が動かない

AL1単独で、コンパイルを試みましたが、128GBPCでも出来ませんでした。

リソースモニタを見ると60GB程度まで消費していました。つまり最大の128GBは、消費していないので、SATソルバの限界と見ます。SATソルバの内部は、32ビットのアドレシングであり、その他のビットも割り当てられるために、有効なアドレシングは、30ビット程度です。2^30=1000万Clauses程度までです。恐らくそれを超えてしまったものと推察されます。

ちなみに、Instance23までは、コンパイル出来30GB程度でした。

Instance24は、超長大規模問題ということです。

＜AL1が使えないと＞

AL3中、AL1は、整数化機構として動作します。LPソルバの推定値を現実の整数世界に変換する機構として動作しています。これが使えないということは、LPソルバが整数値を出力するまで、延々とBranch＆Boundを繰り返す必要があります。要するに膨大な時間を要する、ということです。