ローカルソルバ検討

 Instance24用対策として、ローカルソルバのSurveyを行い、一通り最新の状況を確認しました。特に目立った進展はないようです。

それとは、別に何かSATで打てる手はないかと思案を重ねてきました。新たな発想として、ソルバのメモリ食いが問題なので、メモリを食わないようにしようという発想に行きつきました。

現状メモリを食っている箇所は、3種類あり、

１）ExactlyOne Encoding　

２）TIME　Cardinals Encoding

３）Cover　Cardinals  Encoding

まずは、 Exactly Oneの実装です。ExactlyOneは、1≧Ｘ≧1　で、回路屋さんの言葉では、One Hot Code　とも呼ばれています。　スケジュールナースの殆ど唯一と言ってよい根幹の内部制約です。

1以上1以下を実装するのに、通常2となる組み合わせを全て禁止、かつ1以上、で実装することが多いです。1以上(X≧１）は、CNF節そのものなので、簡単です。問題は、Instance24のように32シフトもあると、休みのシフト１を加えて33C2=33*32/2=528節も必要になります。OR項と併せて529節が365日X150人=2898000節も必要になります。この負担は、大きいです。

問題は、1以下(AtMostOne制約と呼ばれています）を如何に削減するかです。

CommderとかProductとかBinaryの方法は知られており実際現在の実装もそうなっています。

ただ、この手の方法では、根源的な削減にはならず、別な方法を検討することにしました。