GPU(RT5000)を使っても、MittlemanBenchmarkで、IPMを上回るとのことです。
しかし、精度とロバスト性の問題は、依然として課題ということは変わりがないようです。
次のリリース(v.1.11)でユーザの評価に委ねる、ということのようです。
Highs開発チームに新たに3人加わったようですので、MIP系/PDLP系の開発が加速されることが期待されます。
2025年5月14日水曜日
2025年5月13日火曜日
離散解は、リニア解の近傍にある
前回、SATソルバで最適化しようとしても限界があることを示しました。SATソルバの解は離散解です。有体に言えば、(0,1)のどちらかです。これをどのようにシフトを表現するか？という話は、こちらでしました。
ところで、MIPソルバでは、リニアソルバの解⇒離散解にしています。SimplexやIPMでリニア解を得て、Branch＆Bound または、CUTTING PLANEの手法で、離散解を得ています。
この手法の根底にあるのは、リニア解（0.0～１.0）の近くに離散解があることです。そんな保証はどこにもないのですが、何故か実務問題は、そういう事象が多い、ということです。
同じような例は、SATソルバでも観測されています。ランダム系列をSATソルバに食わせても、全くと言ってよいほど解けません。しかし、実務問題をエンコードして食わせてみると、思いの他、良く解ける、ということはあります。
（つまり、私達の生命活動はエントロピーに反する側、何がしら秩序だっている、ということではないでしょうか？）
そこで、リニア解から、離散解への変換ヒュリスティクスを考えます。最も単純には、四捨五入です。
話は飛びますが、ビタビアルゴリズムは、最尤復号方法と言って、A/D変換したアナログ値を確率的に最もあり得るデジタルビットに変換するアルゴリズムです。これは、ダイクストラ法の一変形であることが、ビタビ氏自身も認めていることです。
そこで、単純な四捨五入ではなく、最もありえそうなビットへ復号する変換を考えても良いと思います。で、その候補が、前回の手段となります。
2025年5月12日月曜日
DPS kissat incremental評価
DPS kissat2021baseの評価がまとまりました。
Instanceとしては、スケジューリングベンチマークと実務インスタンスから取ってきています。青色は、Optimumが判明している部分、赤は、最良の目的関数値を示している部分です。
パラメータとしては、現行CryptminisatベースとDPS kissat2021で、スレッド数を変化させています。環境は、Ryzen5950 128GBです。
＜CMSAT-KISSAT比較 単スレッド比較＞
KISSATの優位性は見出せません。同じか、僅かにCryptminisatの方が優位です。
＜CMSAT-DPS＞
Optimumが求まっているインスタンスについては、CMSAT単スレッドが最も高速です。スレッド数が増えていくに従い、低速化する傾向がインスタンスによらず見られます。
Optimumが求まっていないインスタンスについては、大まかに言って、スレッド数が増えれば増えるほど、目的関数値(OFV)の改善傾向が見られます。
＜考察＞
DPSのマルチスレッド化により、高速化が期待されましたが、Optimuｍが判明している比較的エラーが少ないインスタンスについては、逆に遅くなる傾向にあります。キャッシュ特性の方が支配的な領域ではないかと思います。
一方、エラーが多数のインスタンスについては、目的関数値の改善傾向が見られます。キャッシュ特性劣化を上回る探索能力の向上によるものと推察されます。
シングルスレッドで駆動している部分もあり、未だ改善の余地はありますが、DPS KISSATという最新のソルバを駆使しても、現行Cryptminisatベースのシステムに対して目立った効果は期待できない、ということになります。
＜今後の進め方＞
本結果を基に数理ソルバとの融合を進めます。要改善部分（シングルスレッド駆動部、部分的Timeout）については、別途検討
2025年5月11日日曜日
Qスケジュールナースの勤務表作成サービスの契約について
Q.スケジュールナースの勤務表作成サービスの契約について教えてください。
添付のPDF拝見したところ、1病棟に就き1ライセンス契約（110.000円）となると、2病棟では220.000円のサポート料金が必要となりますか？
Ans.
はい、そうなります。もしも病棟間で、殆ど同じ仕様ということであれば、１病棟だけの契約にして1年間メンテナンスの仕方を学んで頂ければ、1年後、独力で展開することも可能と思います。その場合は、サポート料金はなしで、病棟数ｘ買い取り版のライセンス料金で展開が可能です。
しかし、病棟仕様が例えば、1病棟が2交代、2病棟目が3交代というように、仕様が大幅に異なるのであれば、2ライセンス分のサポート付を購入して頂くのが安心だと思います。
2025年5月10日土曜日
IntelのNadelさんがNVIDIAへ
SAT/Maxsat solverで多くの貢献をしてきたNadelさんがNVIDIAに移ったようです。
にしてもNVIDIAとは。SAT solverをGPU化する試みはあるのですが、未だ成功したという例はありません。アークテクチャを根本的に変えないと無理があると思いますが、もしかしたらその面での研究をされるのかもしれません。
にしても、CuOPTと言い、今回の移籍と言い、NVIDIAは全方位に裾野を広げていますね。共通するKey WORDは、最適化です。
2025年5月6日火曜日
2025年5月5日月曜日
Q.夜勤の禁止ペアを追加したい
Q.以下の組み合わせの夜勤ペアを禁止したい
水越智哉 と 新人
水越智哉 と 徳重駿介
水越智哉 と 杉村青空
水越智哉 と 水野真吾
徳重駿介 と 杉村青空
Ans.
禁止したいペアの集合を作って、最大スタッフ数≦１ とすればよいです。
ただし、水越智哉さん 徳重駿介さん 杉村青空さんの3人については、どの二人を選んでも禁止であることに注意して記述します。（夜勤禁止ペアCで記述）
また、水越さんは、その他に新人や、水野さんともペア禁止であるので、属性を増やして記述する必要があります。
１）グループ定義で、青部記述を追加します。
新たに、弱めの重みの４で制約しましたが、今回禁止したペアでのエラーはありません。
今回は、使っていない禁止ペア集合もあります。新たに禁止ペアを追加したくなった場合にご活用ください。
このように、スタッフ個人名ではなく、スタッフプロパティシートで抽象化して実装すると、メンテナンス上好ましいです。（退職したり、新たに追加したりするときは、スタッフプロパティシートをメンテするだけでよい。）
一般に、禁止ペアは、解空間を狭める割合が小さく、多くのペアを禁止しても障害にはならないようです。
登録:
投稿 (Atom)