n100w8_1_2-4-7-9-3-9-2-8 solved!

It took us five months to solve this problem.　The challenge lies in proving that it is optimal.

n100w8_1_2-4-7-9-3-9-2-8:  LB=2145 UB=2145

While the upper bound (UB) of 2145 is relatively easy to obtain, demonstrating that there is no better solution is quite difficult. With the standard Branch and Bound method, you could run the algorithm for a million seconds and still not achieve a proof.

The initial gap between the lower bound (LB) and upper bound (UB) is less than 10, which may seem manageable, but it is actually one of the most challenging problems.

Throughout this process, we have learned a lot and gained valuable knowledge. What makes this particular instance unique is the extremely low gap-narrowing gain (a term we coined). We believe this is due to structural symmetry. To address this, we would need to implement symmetry breaking, but we will discuss that another time.

 There are now only two remaining unresolved instances for INRC2 8weeks on our side! 

n080w814-4-9-9-3-6-0-5

n080w820-4-0-9-1-9-6-2

Optimization Night 9

CDCLによるMILP解法が興味深いです。日本でも、このような方がいらしたのですね。NTT DATA出身の方らしいのですが、この会社は、OR業界の重鎮が在籍され、東大・京大出身の方が多い、印象です。（⇒RAMP講演の懇談会で名刺交換させていただいたことがありました。そのときは、NTT DATAに所属されていました。当時、私もSATの限界を感じ分岐限定法の勉強を始めたばかりでMILPのヒュリスティクスについて質問させていただいたのですが、丁寧に教えて頂いたことがあります。）

 Optimization Night #9

INTSATについては、その後、RoundingSATやExact系に引き継がれていると思いますが、Benders　Decompositionを用いるというのは、聞いたことがありません。CDCLでBenders Cutを用いるのは新しいと思います。研究の最前線だと思いますので今後も要注目です。

CDCL による厳密解法を採用した MILP ソルバー - Speaker Deck

Q 日勤リーダを２－３日間ずつ、A/Bチーム各１名とするには？

 Ans.

休日も含めて、全日リーダを各１名配置した解です。

シフト「リーダ」を追加します。

列制約で、A/Bチームから各１名を設定します。なお、若手二人がリーダとならないようにしています。

リーダ回数を指定するために、グループ定義を設定します。

スタッププロパティシートで、各スタッフのリーダ回数を設定します。禁止の人は最大０、

制約なし（何回でもOK）の人はブランクにします。

行制約です。１日単リーダを禁止、４日連続を禁止とすれば、残りは、２－３日間連続のリーダとなります。また、日勤リーダの間隔が短くなりすぎないようにしています。

以上で、全日リーダ、２－３日間A/Bチーム各１名の実装が完了しました。

日勤者数管理は、リーダを含めて日勤者数とするか、リーダを含めない日勤者数とするかは、列制約による実装となります。ここでは示しませんが考えてみてください。

＜平日日勤リーダのみの場合＞

平日のみ日勤リーダにしたい場合は、以下を変更します。このようにすると、全てのパターンは、平日ついて作用することに注意してください。

先月部を含めるとハード制約では、矛盾が生じる可能性があるので、全てソフト制約とします。

列制約で、「今月平日」、「今月休日」を追加変更します。今月休日では、日勤リーダを不可とします。

以上の変更で、平日のみ２－３日間、日勤リーダの実装が完了しました。

下の解を見ると、休日を跨いで、２－３日間、日勤リーダが実現出来ていることが分かります。

先月休日は、リーダが割り当てられています。これは、先月予定部がフィルインされていないことと、先月休日に対しては、なんの制約もしていないためです。先月予定部がフィルインされていれば、解消するので上の制約で問題ありません。

sloppy24

Solving Linear Optimization Problems for Pseudo-Booleans and Yonder 

の略らしいです。ワークショップです。

Jakob Nordström: SLOPPY '24

確かに、SATを一般のMIP問題に適用しようとすると、CNF表現では、無理があると思います。これを疑似ブーリアンと抽象化することで、IP問題と親和性が生まれます。で、そこにCutting Proofを入れるという発想は自然なものとなります。

ただし、一般にLPの速度は、CDCLのバックトラックに比べ、二けた以上遅いので毎回行う訳には行きません。LPソルバを導入した場合、この辺をどうバランスを取っていくかというのが実装上の問題かと思います。

Yinyu Ye教授の講演集

内点法の大御所の講演集です。 

web.stanford.edu/~yyye/talks.html

特に、

Rescale

は、最近のLPの動向について詳しく大変参考になります。

COPTに関して妙に詳しいので、もしかしたら、COPTの創業者達は、教授の門下生？かもしれません。

Q 次のソフト制約で、許容範囲を超えています。のエラー解析の仕方

 Ans 

次のようなエラーとなっています。

この上部を見ると、SoftConstraintColumn5という赤エラーが表示が出ています。これは、ソフト列制約レベル５の許容範囲が超えていることを示しています。

範囲が超えているというエラーなので、極端に範囲を大きくすれば、解が出ます。許容範囲を2→１０に変更しました。

これで、解が出ました。列制約レベル５に対応する重み５のエラーが多数出ています。実際に解の状況を確認します。休日の制約であるはずなのに、平日にもエラーが表示されていることが分かります。

Day集合を確認してみると、次のように上図解の通りの集合となっています。

Day集合の指定が間違っていることが分かりました。

正しい、集合に修正します。

修正後の解です。平日日勤と排他的になっていることが分かります。

まとめ

１）一つ制約を書いたら、直ぐに求解して動作を確認しましょう。

２）制約におけるDay集合、グループ集合を確認しましょう。

３）許容範囲を超えています。⇒当該許容範囲を極端に大きくしてみて、解が出し原因を突きとめます。

pseudo boolean competition2024

Pseudo Boolean Competition 2024

 ８年ぶりにcompetitionが再開されました。この理由として、２０１６年の参加者が殆どいなかったこと、Jakob Nordstr¨ omさんが、強固に開催を主張したこと、が挙げられています。

参加者としては、CAI教授系中国チーム、RoundingSAT系、Exact系、SCIP系、そして、名古屋大酒井先生です。2016年来の進歩としては、RoundingSAT系のcutting proofがあるのですが、それなしのNAPSと比べると、それほど差がついているようには見えないというのが意外でした。

PB24 Pseudo-Boolean Competition 2024

いずれにせよ、今後の方向性としては、RoundingSATをベースとしたものになると思います。私も、この発想を取り入れようかと思っています。

chat gptの構造化出力

待ち望んでいた機能が実装されたようです。 

https://note.com/mz700/n/n1ff5b41abb8b

Azure版でも可能になっています。

Azure OpenAI Service で構造化出力を使用する方法 - Azure OpenAI | Microsoft Learn

これで、何が嬉しいかというと、出力が完全なjsonで出てくるということです。しかも、ユーザの定義するJson形式で出てくるというです。スケジュールナースの制約指示は、私が定義したJsonスキーマに基づいて、GUIが作成を担当しています。つまり、

制約作成者⇒GUI⇒JSON⇒ソルバ

という現在の流れになっています。これを、AIに学習させれば、

制約作成者⇒AI⇒JSON⇒｛ソルバ　GUI｝

という、最も熟練度を要する部分をある程度、置き換えることが出来る可能性が出てきた、ということです。既にGitlab-copilotのように、AIは、pythonコードも出力することが出来るようになってきました。スケジュールナースのJsonは、実はPythonコードも含む仕様です。なので、モデリングの全てを任せられる可能性まで視野に入れることも出来ます。信頼性については問題があるのが現状ですが、AIの日進月歩に期待しましょう。テキストもしくは音声で、「ああして、こうして」と言うだけで勝手にモデリングしてくれたらなんて幸せでしょう？

かって、看護師長時の妻は、私の傍らにいて、「ああして、こうして。」と言うだけでした。結局、私という存在がいるので、最後までスケジュールナースの制約を覚えることはありませんでした。それでも、私という制約作成者がいたおかげで勤務表づくりは何の問題もありませんでした。

私の代わりをAIに担わせることは出来ないでしょうか？

幸いにして、スケジュールナースは、オープンソースのモデリング集があります。日本、否、世界中の看護師勤務に関する知見もあります。このブログも実は、モデリング学習資源の一つです。10年に渡る膨大なスケジュールナースのモデリング資源があり学習資源については事欠きません。

そのスケジュールナースJsonスキーマは、公開していませんが、出力されるJson形式をみれば、大体想像がつくと思います。

また、JsonからGUIにコンバートするプログラムの開発も必要となります。AIが出力したJsonを人間が視覚的に理解するには、GUIでの視覚表現に戻す必要があるからです。

今後の予定として、

世界記録を更新し、

公開されているナーススケジューリング問題を全て解き、

ソルバの再構築の後に

取り組んでみようと思います。ソルバ再構築は、未だ構想段階です。今回のINRC2を全て解こうという取り組みの際、得られた知見を持って再度ソルバ全体を見直す必要が感じました。一言で言うとSAT表現とリニアソルバの融合になります。具体構想については、別の機会に。

来春以降、主要テーマとしたいと思います。