schedunule nurseⅢ one drive版

インストーラは、準備できていません。当面64Bit版のみです。
私のテスト環境をそのままOneDriveに上げています。日々、更新しているので、バージョン管理はありません。(正式リリース版時と互換がない場合があります）
とりあえず、マニュアル（途中）を用意しました。

one driveのフォルダをコピーしてください。
GUI　EXE、schedule_nurse3.exeは、sc3_test/sc3/sim_engine32にあります。
ショートカットを作成して起動してください。

SAT RACE 2019

今年は、SAT　Competitionはなくて、SAT　RACEでした。SAT１９　Conferenceで結果が発表されております。最新のProceedingsが８月までは、フリーアクセスできます。Armin Biereさんと、Fahiem Bacchusさんの論文に注目しています。
来年は、Armin　BiereさんのCaDiCalがトップを取りそうな気配です。

メインソルバ マルチスレッドの評価

簡単に評価してみました。
結論的には、効果のある場合もあるし、ない場合もある、という微妙な結果になりました。

これは、SATとかメタヒューリスティクスの世界では、よくある話です。こちらでもSatisfiable problems are well-known to have unstable solving times. と述べられている通り、解が見つかる・見つからない　というのは、確率的なものです。RandomizerのSeed値を変えただけで、10倍速度が違うということは、往々にしてあります。ですので、ソルバーの真面目な評価は、カクタスプロットという多数のインスタンスを用いて、統計的に評価するのが一般的です。

下が、求解後の画面です。各重みに対するエラー数の表示を追加実装しました。

下は、中規模のインスタンス結果で、NRCⅡn030w4-16291です。このインスタンスの厳密解は、1660-1670内に存在することが分かっています。（数理的ソルバ（アルゴリズム４）で数時間RUNした結果)　

確かに、CPU数（スレッド数）が大きくなると求解時間は、減少傾向が確認できますが、目的関数値は、改善傾向にあるとは言えません。

Xeon　E5-2620　2GHｚ　28GBRAM（6コア12スレッド)

さらに、非常に重いハード制約のインスタンスの結果が次です。
グラフにするまでもなく、マルチスレッドでは、非常にばらつき、なおかつ改善どころか,改悪傾向
にあります。

CPU数	求解時間(sec)	備考
1	189	求解時間は安定(SC2では1688sec)
2	Timeout(2000sec)	求解時間は安定しない
3	1387
4	1444
5	739
6	741

これより、重いインスタンスでは、マルチスレッドにしないほうが良い、と言えます。キャッシュに収まらないという、物理的劣化要因は、確かにありますが、deterministicでないということがあります。
deterministicにするかしないかは、パラレルソルバの設計要件です。しないことによって、共通リソースが多くなり、メモリ減少→キャッシュミス減少→オーバヘッドが少なくなる..パラレル化の効果がより強く発揮する場合もあり一概に駄目だとは言えません。

確率的な要因、determisticでないこと、キャッシュ溢れ、この３要因によって、シングルスレッドに劣るのだと思います。軽いインスタンスでもdetemisticでない影響はあるのですが、目立たないということでしょう。

＜ハードのソフト化＞
SC3では、求解オプションを追加しており、ハード列制約を緩和することが出来ます。
（解がないという事態を避ける目的で入れた新オプションです。Default　Onです。）

ハード列制約のソフト化にチェックを入れると、最大ソフト重みの、およそ10倍の重みでソフト制約化を行います。上の左画面では、重み60までしかありませんが、右の結果画面では、重み1000の行があります。これが、ソフト制約化した擬似ハード制約になります。結果エラーが0ですから、ハード制約は全て満たしているという結果になっています。

このオプションで、走らせて見るとどの程度難しそうかは、求解の進み具合から、推測できるのではないかと思います。ハードインスタンスの場合、GO/NGですから、満たすのか満たさないのか、解が出てくるまで、あるいはタイムアウトまで、分かりませんが、上のようにチェック一つでソフト化
することで、先が読みやすくなるのではないかと思います。
。





　

メインソルバの改善 その２

マルチスレッド化の実装を行いました。

検証は、これからです。
cryptminisatの設計思想をそのまま拝借しました。マルチスレッド特有のLockに時間がかかってしまうことを避けるシンプルな設計思想です。

それから、名前がユニークです。似たような事は、私もやっていたのですが、体系的に少し徹底してやる感じです。メモリ削減に効果が期待できそうです。

さらに、新しい改善アルゴリズムを思いつきました。

以上を実装して、どれだけ効果があるかは分からないのですが、メインソルバについて出来る事は
やり終えたと思います。

メインソルバの改善 マルチスレッド化

アルゴリズム１は、メインソルバですが、実務問題では、やはり殆どの場合、他は使わない(使えない）、となると、やはりマルチスレッド化しておいた方が何かと都合がよいと思いました。

ということで、頑張って、マルチスレッド化と、及びチューニングを行い、なんとか旧来のパフォーマンスは、維持したいと思います。

 搭載ソルバ郡は、以下です。

アルゴリズム０/1は、SATベース、２は、UNSATベース、３は、SimulatedAnnealingの予定ですが、
未実装です。４は、数理的ソルバです。

名称	略称	停止方法	CPU数	内容
0	SC2ソルバ	タイムアウト	設定可	ほぼ旧SC2ソルバです。
1	メインソルバ	タイムアウト	設定可	リニア方式ソルバです
2	特殊ソルバ	厳密解が求まるまで停止しないので、打ち切るには、中止ボタンを押してください	1	実務問題は、殆ど解けません。
				０近傍に解があることが分かっている場合に、有効な場合があります。
3	Reserved
4	数理的ソルバ	厳密解が求まるまで停止しないので、打ち切るには、中止ボタンを押してください	1	Simplex/内点法を使ったソルバです。実務問題では、殆どの場合、メインソルバに歩があります。しかし、学術ベンチマーク問題では、このソルバが優勢です。

SC3のメインソルバ解説

SC3は、複数のソルバを搭載していますが、基本的には、defaultソルバのみ（アルゴリズム１）を使ってください。
アルゴリズム１は、旧来ソルバ（アルゴリズム０）と同じ種類の、改良Versionになっています。

右のペインは、SchedulingBenchmarkサイトのInstance1の問題を解いたところです。
充足解を書き込み中での前の数値が目的関数値となります。

目的関数値は、OR用語で、最適化問題における最適値となります。Status　Optimumが出ているので、厳密解が607　ということが分かります。これは、SchedulingBenchmarkサイトにあるKnown
Best　Valueという値と一致しています。

従来のレベルに関しては、同じ扱いです。そこに重みが紐付けされていることになります。
607ということは、恐らく重み100であるレベル７のエラーが6個、重み１，２，３のエラーが数個足して7という具合になっていると思われます。

各レベルの重みをW(i)、エラー個数をE(i)としたとき、目的関数値は、リニア加算で求められ

ObjectiveValue=ΣW(i)＊E(i）

という具合に表現されます。　これは、あくまでモデリングの話であって、現実の良し悪しは、Logとか２乗とか、非線形にした方が、感覚的に近いということはあるかもしれません。が、そうなると
解くのも難しくなるので、MIP問題では、線形加算で求めるのが一般的です。

それはともかく、目的関数値０が、理想的であることは、依存ないでしょう。そして、目的関数値が小さければ小さいほど、より良い勤務表のアサイン　という風になるように、感覚的な重みを
選ぶことは、ユーザの仕事になります。理想からの偏差をコストとして捉えコスト最小問題として考えるとしっくりするのではないかと思います。

重みを大きくすれば、優先度が高くなります。上の例で、100というのは、ハード制約的な意味合いを持たせているだと思います。ソルバにとって、重み100（レベル7）の1個のエラーは、重み1(レベル1)100個のエラーと同じ重みとなります。

＜従来ソルバとの対比＞
レベルが、１－２種だとさほど感じませんが、レベルが多く時間がかかる複雑な問題では、末端レベルで悲惨な状況になりがちでした。そのような場合は、重みで表現すれば、調整がしやすくなるのではないかと思います。

また、途中で求解を打ち切る場合でもそれなりの解になっていることが
多いのではないかと思います。

トータルの数値として出てくるので、勤務表の良し悪しを目的関数数値で比喩しやすくなる、という事が言えます。また、ソルバの評価にしても、同じ問題なら、少ない目的関数値を出力した方が優秀ということが言えます。

＜アルゴリズム１のソルバとアルゴリズム０（旧来)のソルバでの比較は、どうか？＞
という質問には、やってみてくださいとしか言えません。

インスタンス(問題)毎で違います。
劇的に速くいく場合もあるし、却って時間がかかる場合もあります。一般には、ソフト制約が多い場合は、アルゴリズム１が強く、少ない場合（２種以下）では、アルゴリズム０が良い場合もある、という感じです。

＜CPU数＞
アルゴリズム０は、CPUを複数使えますが、その他のアルゴリズムは、CPUを一つしか使いません。これは、前に述べたUlitimate構想によるものです。（Ulitimate機能の実装は、来年以降でしょう。）

量子アニーリング

とても勉強になるサイトがあります。なるほど、整数計画もSATを介してイジングモデルに変換できるのですね。　組合せ最適化に対する新しいアプローチです。

今までの組合せ最適化のアプローチは、大きく分けて次の３つです。

■MIP
　Simplex・内点法をベースとした線形ソルバをベースにCuttingPlaneで整数化を図る古典的なアプローチです。Cplex/Gurobi等、商用ソルバが圧倒的に強い分野です。

■SAT
　SATソルバーベースのアプローチです。

■Simulated　Annealing
  に代表されるメタヒューリスティクス的アプローチです。

これに量子アニーリングが加わることになるのでしょう。ハードウェアの並列性を生かした解法
と認識しています。

全ての問題を一つのソルバが凌駕するということには、恐らくならないと思います。例えば、ブランク数独は、SATの独壇場で100x100でも難なく解けますが、MIPやメタヒューリスティクスでは、そうではないでしょう。1000人のナーススケジューリングという問題がもしあったとしたら、私ならMIPやSATは使わず、Simulated　Annealingを採るでしょう。（というよりも、まともに解けない規模です。）　ということで、問題分野・規模で、採るべきソルバーは変わってくると思います。


　
　

人工知能学会 正会員登録なりました

今月号の学会誌17ページに、理事会で承認された新規入会の方々で、菅原システムズがしっかいり載っています。年度初めということもあるのか、100人以上います。私の底流は、SAT・グラフ・整数計画といった基本問題にありますが、学会誌をみても流れは、DeepLearningにあることを感じます。今後どのような融合があるのか、興味があります。