2024年4月27日土曜日

新しいAlgorithm1のアーキテクチャ

 従来のAlgorithm1のアーキテクチャは、パラレルSATソルバです。ポートフォリオと呼ばれる形態を取っています。これは、同一の問題を異なるパラメータで解く方式です。この方式の問題は、

■決定的にならないこと

■大して高速化しない。良い場合もあるが、シングルスレッドの方が良い場合もある


内部のソルバ間は、学習節を交換しながら進みます。マルチスレッドであっても、基本的にアルゴリズムは、一つです。つまり多様性に乏しく、実使用時の様々な問題に対して常に最適なアルゴリズムであるとは言い切れない、という問題がありました。

そこで新しいアーキテクチャは、次のようにします。複数のアルゴリズムを並列に走らせます。問題の形態によっては、得意なアルゴリズムは変わってきます。複数のアルゴリズムを一機に走らせます。アルゴリズムを選びません。どの問題に対して、どいうアルゴリズムが親和性があるか?判定するのも時間がかかってしまうからです。アルゴリズム間では、情報を交換しません。先に着いた者勝ちという、単純な構想です。

懸念としては、駆動インスタンス分のメモリがどうしても必要になります。キャッシュヒット率が下がり、シングルスレッドよりも遅くなることが考えられます。この傾向は、規模が大きければ大きい程顕著になります。


これによる効果としては、
■安定度が高い。プロジェクトが決定的になる確率が高い
■求解速度向上


デメリットとして
■解は、一つのみ
■原因解析機構は、後回し
■リニア解の最適値には、必ずしも合致しない(準最適解)
■環境によっては、遅くなる懸念(メモリキャッシュ問題)

なので、Algorithm5として実験的に実装する予定です。Algorithm1は、そのままとします。
目標は、
1)解を決定的にする
2)ICU70人問題の求解時間6分を2分以下にする
3)SchedulingBenchmarksの記録更新
4)INRC2の記録更新
にありますが、これにより1)2)について、ほぼ達成見込みとなりました。
実使用時の改善となります。しかし、本題の3)4)の改善には、全く寄与しません。
学術問題のベンチマークと実使用時の問題とでは、問題の性質が全く異なるからです。言い換えるならば、Algorithm1/5は、実使用時の問題用、ということです。

学術問題には、学術問題用のアプローチが必要であり、Algorithm5では歯が立ちません。
しかしながら、そこも含めて改善しておかないと、記録更新に到底届くものではありません。今回の改善もそのために必要なステップです。


2024年4月26日金曜日

SATヒューリスティクスの歴史

 長い間、VSIDSというスコアリングが主流でした。その後MapleSATでLRB、その実用形態としてCHBが提案されました。KISSATではCHBは実装されず、またCryptiminisatでも廃止に至ってまたVSIDSに回帰しています。しかし、その後、MABとして、ダイナミックに切り替える方法が提案されて現在に至ります。

ConstraintSolving[2]SATSolvingBasisAndCDCLpdf (ios.ac.cn)

アルゴリズム1系も見直すにあたり、ヒューリスティクス系も見直すことにしました。

SAT Solverを牽引してきたのは、フライブルク大学のArmin Biere教授です。

paper6.pdf (ceur-ws.org)

MiniSAT以来、色々提案はされていますが、Kissat以降目立った向上はありません。

2024年4月25日木曜日

最近気になった論文

 CadiCaLというSATソルバの実装を見ていて、面白いインタフェースを備えていることに気づきました。案の定、SMTソルバcvc5の実装で使われているようです。

IPASIR-UP: User Propagators for CDCL - YouTube

これは、従来のスタンドアロン的な使い方に留まらず、可能性が広がることを意味しています。安直に思いつくのは、B&B(Branch and Bound) と併用することです。その他にも可能性があり、今後の一研究領域になると確信します。

2番目の論文は、既出ですが、改めて見てみました。5%の改善ならば、最近のSAT Competitionでも優勝候補になると思います。

[2110.14053] NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks (arxiv.org)

最近、NPU搭載のCPUが出始めており、例えば、そのプロジェクトに特化した学習をオフラインで行うことが将来可能になる、というです。個別プロジェクト毎に性能向上の可能性があるということです。

しかし、上記手段を用いても速度向上は、数%のオーダでしょう。速度向上を体感できるには、2倍以上が必要と考えます。その意味で、重要なのはアルゴリズムです。新しいアーキテクチャでは、速度向上が体感できると思います。

2024年4月24日水曜日

Q.勤務表作成サービスを利用したいのですが..

 Q.契約とか無くて大丈夫なのでしょうか?

Ans.

プロジェクト作成サービスは、無料で始められます。

仕様を上手く文章で表現できなくとも、ZOOMで会話しながら、始めることが可能です。

スケジュールナースが出した答えをExcelで確認して頂きながら、ステップアップしていきます。ある程度、基本的なところが出来たことが確認できたのならば、発注して頂きます。それまでは、一切料金はかかりません。

発注後は、プロジェクトファイルが届くので、細かな仕様の実装を行います。細かな点についてお聞きしながら進めていきます。

<進め方>

1)ルール.txt の改定(菅原システムズ、お客さま)

2)プロジェクトファイル作成のためのExcelFormatシートの書き出し(お客さま、詳細は、そのときに説明します。)

3)1)2)に基づいたプロジェクトファイル作成(菅原システムズ) Excel解提出(x月解)

4)Excel解検証、1)2)追加・修正(お客さま)


1)~4)を基本的に使えそう、となるまで繰り返します。通常数回程度ループします。この段階では、一切料金は発生しません。

OKとなったら発注ください。


プロジェクトファイル作成サービスは、2種類あり、

A)3カ月サポート(税込み3万3千円、ソフトは別途サブスクをマイクロソフトストアで購入する必要があります)

B)1年サポート(税込み11万円、買い切りソフト込み)

https://www.nurse-scheduling-software.com/japanese/service2/onetime_purchase/

があります。現時点で決定する必要はありません。しかし、サブスクは、クレジットカード購入の一択しかありませんので、国公立病院の場合、2)となってしまうと思います。

5)発注後、プロジェクトファイルを送付します。使い方等、ZOOMでお教えします。また、サポート期間内で、細かな仕様追加・修正等を承ります。

6)サポート期間終了後は、一般ユーザと同様となります。(ご質問に対する回答をメールで行います)


2024年4月17日水曜日

チュートリアル後に、注意するべきこと

スケジュールナースビギナが注意するべきことを、まとめました。

1)ファイル→ダブルクリックでプロジェクトファイルを開かない

2)制約の変更・集合定義の変更は、ブランク予定で行う。ブランク予定以上にUBが良くなることは決してありません。ブランク予定時は、UB=0をできるだけ維持するように心がけてください。

3)設定・制約の変更をしたら、即求解、動作確認を一つづつ行う。一つ変更一つ求解確認が原則です。高速ソルバたる必要と所以がここにあります。

4)解がないときに、解を見ても意味はありません。解がない原因は、ハード制約間の矛盾です。エラーメッセージを冷静に見て、今起きている矛盾を取り除いてください。今、起きていることを冷静に分析・推理することが重要です。エラーメッセージがヒントの全てです。

5)制約の確認は、マウスホイールボタン、Day集合・スタッフ集合により行う

6)スタッフプロパティシートは制約ではありません。集合の定義です。一方スタッフ毎のシフトは、制約です。しかも前月を含む全体に対するハード制約になります。



2024年4月16日火曜日

Q.介護スタッフ専用の「A勤務」(まれに看護が入ることもある)が看護職に連続で入ったりする..

 Ans.

スタッフ定義のスタッフプロパティシートは、集合の定義です。制約ではありません。


制約ではないので、書いたとしても何の作用も引き起こしません。そこで、グループ集合で

否定集合を作り、


否定した集合に対して制約して、初めて意味を持ちます。


一方、スタッフ毎のシフトは、全期間に作用するハード制約です。


ハード制約なので、チェックされてない人のシフトは、絶対に割り当てられることはないです。スタッフ毎のシフトは、将来も変わることのない勤務に使い、月々で変わる勤務には、スタッフプロパティシートによる記述をお勧めしています。このハード制約は、全区間に作用します。チェックを変更すると、それ故先月部にハードエラーを引き起こします。そのために、先月部に矛盾があったときは、先月部をソフト制約にして逃げるオプションにチェックを入れておきましょう。こうしておくと、先月部でハードエラーとなることはありません。レベル1のソフトエラーとなります。

この違いを理解して適切に制約してください。



2024年4月15日月曜日

Q.同じプロジェクトファイルに対して複数のスケジュールナース...

 が出ています。どうしたらよいでしょう?


Ans.

いいえにしてください。名前を付けて保存をして、名前のバージョンを例えば、ver9→ver10という風に、別名にて保存することをお勧めします。

恐らく.nurse3の拡張子の同じファイルをダブルクリックして起動しているのだと思います。スケジュールナースのアイコンをクリックすると、次のように複数起動していることが分かります。これが原因です。



「ファイル」→「プロジェクトファイルを開く」でプロジェクトファイルを開いた方が間違いなく操作できると思います。

2024年4月14日日曜日

Q.「その人とは誰からもペアになりたくない」はどう記述すればよいでしょう?

 Ans.

誰もその人とはペアになりたくない、という方はいらっしゃるかもしれません。大体どの病棟・施設でも、そういう方はいらっしゃいます。しかし、だからと言って誰ともペアを組ませないと、夜勤の人数は、常にその方、一人となってしまい、列制約を満足できなくなってしまいます。題意は、恐らく、そのようなスタッフと組む回数を平等にする、ということなので、その人とのペア回数を平準化することです。

例えば、その方とのペア回数を全員1回以下とする、可能ならば。ということではないかと思います。

残念ながら、この制約は、Pythonでしか記述できません。この職場の場合、男同士の夜勤は禁止、なおかつ看護師と介護各々1名ということなので、その方が介護・男である場合、あり得る組み合わせ対象は、女性・看護師に限定されることに注意します。そうなると、意外に組み合わせ範囲は、限定され、例えば、夜勤を6回、女性看護師が4人しかいない場合、

6回=1回2人 2回2人

6回=2回 3人

6回= 3回 2人

6回=3回1人 1回1人 2回1人

つまり、ペア1回の人が2人、ペア2回の人が2人という解しか、全員が負担する、という解は存在しないことになります。他の全てのでケースにおいて、負担0の方が存在し不平等がありえます。「私2回だ、不平等だ」は、4人のうちの50%、2人に発生するのは必然となることは理解しておいた方が良いと思います。別な見方をするなら、3回ペア夜勤を禁止することで、2回以下となる解が得られるようになる、ということです。また、ペア1回以下をハード制約とすると解は存在しない、ということになります。

この辺が組み合わせ最適化の難しいところです。単純なリニア制約では表現できないところが、人間的であるところだと思います。

次の求解パラーメータ、許容エラー1に注目してください。

一番下で、オーバライドにチェックが入っています。


これは、次のPythonソースで、最大ペア回数を1回に制限している部分に作用します。

Pythonソース上は、許容エラー数が3(sc3.SeqError(min,max,許容エラー数)になっていますが、上記のようにオーバライドのチェックされているので、1が適用されて、実際は、

0±1≦ペア回数≦1 ±1

のように許容エラー部±1として作用します。たとえば、

6回=3回1人 1回1人 2回1人

のように一人の人にエラーが集中しても、目的関数値が小さければそちらが最適値になります。しかし、題意は、一人の人に負担を集中させないことにあるので、±1で2回まではOKだが、3回は絶対ダメよ、とハード制約にしている訳です。この辺の設定をPythonソースを弄ることがなく出来るようなオプションがオーバライド設定になります。

ちなみに、許容0とすれば、ハード制約となり、解が存在しない、もしくは、強制的に夜勤4回以下となるでしょう。→やってみました。解がありません。つまり、全員を1回以下にする解は物理的に存在しません、ということです。



Pythonソースは、以下です。上で説明した内容そのものですので、理解し易いと思います。下から見ていくと良いと思います。今回は、かなり高度な設定の仕方でした。


import sc3


def ペア回数制限Sub(person1,person2):
    list=[]
    for day in 今月:
        v1=sc3.GetShiftVar(person1,day,'入り')
        v2=sc3.GetShiftVar(person2,day,'入り')
        list.append(v1&v2)
    s=staffdef[person1]+"と"+staffdef[person2]+"の組み合わせ回数"
    print(s)
    sc3.AddSoft(sc3.SeqError(0,1,3,list),s,5)#min max allowable errors 最大1回に制限


def ペア回数制限(person1):
    if person1 in 男:
        if person1 in 看護師 or person in 准看護師:
            #ペア対象 女性 かつ 看護師または准看護師 ではない
                for person2 in 入り:
                    if person2 in 女 and person2 not in 看護師 and person2 not in 准看護師:
                        ペア回数制限Sub(person1,person2)
        else:
            #ペア対象 女性 かつ 看護師または准看護師 
                for person2 in 入り:
                    if person2 in 女 and (person2 in 看護師 or person2 in 准看護師):
                        ペア回数制限Sub(person1,person2)
    else:
        if person1 in 看護師 or person in 准看護師:
            #ペア対象 看護師または准看護師 ではない
                for person2 in 入り:
                    if person2 not in 看護師 and person2 not in 准看護師:
                        ペア回数制限Sub(person1,person2)
        else:
            #ペア対象 看護師または准看護師 
                for person2 in 入り:
                    if person2 in 看護師 or person2 in 准看護師:
                        ペア回数制限Sub(person1,person2)

for person in 特別ペア回数制限:
    ペア回数制限(person)
        
   
    

2024年4月13日土曜日

Q.次の記述のどこがいけないのでしょうか?

 Ans.

男同士の夜勤禁止が、間違っています。「かつ」は、「全員」という意味です。この制約を言葉にしてみると、

男全員が男全員と入りをすることは禁止

という意味になります。そもそも男全員が夜勤に入ること自体があり得ないので、それを禁止にしても意味はありません。

問題は、二つあり

■同じ集合である「男」と「男」を禁止にしていること、

■全員の意味である「かつ」を使用している


ことにあります。ペア制約で、意図通りにするには、上図のように、「男」集合を分割し、「看護師男」と「介護男」とします。演算子は、「または」を使用します。「または」は、少なくとも一人以上という意味になります。この制約を言葉にしてみると、

看護師男の少なくとも一人以上が、介護男の少なくとも一人以上と夜勤をすることを禁止。

と、制約意図と合致していることが分かります。



ペア制約での記述でも間違いではありませんが、Betterな記述は、次のように列制約で記述します。
このとき、スタッフプロパティは、以下のようにします。

この記述スタイルの利点は、以下です。

ペア制約で個人名を使わずに記述可能。スタッフプロパティシートは毎月変更するので、スタッフの退職・入職等の変更等のメンテナンスはこのシートを弄ることになります。制約は時が経つと忘れてしまいますが、このシートは、全項目をメンテする、とだけ覚えておけばよい。
ペア集合1、2、3の変更はスタッフプロパティシート上で自由である。また複数人数のペア禁止も可能、使わなければブランクでもOK。列制約で制約したことは忘れてよい。メンテナンス性が良い。より汎用的であり、将来の変更のし易さが違います。
■ペア制約では、「看護師男」、「介護男」と集合を分けて記述する必要がありますが、このスタイルでは、「男」だけで記述でき、新たに集合を合成する必要がない

2024年4月12日金曜日

Q.入明入明休休を好むスタッフは、どう記述したらよいでしょう?

 Ans. 

スタッフプロパティシートに、連続夜勤回数の最大と最小を記述します。連続夜勤を行うスタッフには、このプロジェクトの場合、漏れなく2連休が付いてきます。(ハード制約で記述)

そのために、稼ぐ意味も含めて連続夜勤を好む方は、最小連続夜勤回数を設定します。反対に、連続夜勤を好まない方もいるでしょう。そういう方は、最大連続夜勤回数を0にします。


連続夜勤のカウントは、明入パターンで行えばよいでしょう。




2024年4月11日木曜日

Q 「入明入明の後は連休」が動かない

 Ans.

パターンが間違っています。下のパターンでで囲んだところは、各々

「明けの後週休以外」の禁止 →明けの後週休を強制

「明けの後、入り」

で「明けの後」が共通しています。

パターンは全体に対して作用する。同じパターンがあったときは、短いパターンで制約される、という原理を想いだしてください。長いパターンの方は、6日のスパンに対して、禁止です。一方短い方は、2日のスパンに対して禁止です。よって、「明けの後週休を強制」制約が作用し、行制約No4は、決してヒットすることはありません。


このままでは、2回連続の夜勤ができないので、「明けの後週休を強制」を「明けの後週休または入りまたは有給」に変更します。施設によっては、有給を許さないところもあるので、注意してください。(可能であれば、有給や、年休も付けた方が、解空間の減少を抑える効果が期待できるので付けた方がBetterです。)



最終的に、上記シフト集合を用いて修正したのが次です。短いパターンに規制され「週休または入りまたは有給」しかありえないので、長いパターンの方はブランクでもOKです。勿論、「入休」または「休集」でもOKです。解空間は減少しますが、「週休」でもOKです。

2024年4月10日水曜日

連続勤務制約で注意するべきこと

 次の2点です。

1)連続勤務6日禁止の定義の明確化が必要

必ず週休が5日内に1回以上含まれるなのか?休日集合が5日内に含まれるか? 施設によって違います。週休でなければならない施設もあるし


週休でなくても、例えば年休や有休が5日内であればOKという施設もあります。その場合は、それらを含んだ休日集合で制約します。


2)先月からの連続性に注意

2交代の場合、入り明けは、連続しています。入りが、今月最終日が連続勤務5日目だったとしたら、来月1日目は、6日目明けが強制され矛盾となってしまいます。従い、予めそのようなパターンは、禁止しておく必要があります。例えば、次の記述青部になります。入明入明まで考慮すると、恐らくリソース的に月末は困難になってしまうでしょう。なので強制的に先月からの夜勤の場合は入明休となるこのパターンで良いと思います。

なお、防止パターンの曜日集合は、月末しか見ないので、「今月」でもよいのですが、セオリー、「パターンを弄ったら今月自動」で記述しています。

以上は、2交代パターンですが、変則2交代(長入明)の場合は、さらにもう一日拘束長が増えるので、さらに防止パターンが必要となります。



2024年4月9日火曜日

Q入りの後が明けや 入明入明の後は連休といった絶対に満たさないといけない制約ができていないのですが?

 Ans.曜日集合の指定が間違っていました。「制約開始日一日前」と「制約開始日一日前から」

は、違います。

マウス中ボタン(ホイールボタン)を押すとDay集合が表示されるので確認してみてください。スケジュールナースは、この曜日集合を一日づつずらしながら全体をスイープして制約しています。なので、「制約開始日一日前から」は、先月の最後の日+今月(28日)分の集合である必要があります。他も同様です。




間違いのないやりかたは、

パターンをいじったら、曜日タイプを「今月自動」にして求解し、ファイルを保存するようにします。

こうすると次回プロジェクトを読み込んだときに、適切に設定されているのが分かります。


2024年4月8日月曜日

Q.Macの対応予定はありませんか?

 Ans. 申し訳ありませんが、ありません。将来的にも、ほぼ可能性はないと考えてください。

理由は、こちら側の内部の事情によるものです。申し訳ございません。

■技術的には、エンジン系が、インテル系のCPUに限られるという事情があります。極限まで、最適化エンジンを「最適化」しているためです。X86/X64というインテル系のCPUをターゲットにしています。互換CPUとしてAMDがあり将来的にも王道と考えています。

■技術外の理由は、サブスク・買い切り版の形態の対応です。Appleの形態では、現状の買い切り版のような菅原システムズに支払う形態は認められていません。公的機関に納入している菅原システムズにとってこれは痛いです。

Appleに対して「App Storeでの30%というマージンは法外なぼったくり」「ユーザーの選択を狭める」と批判が集中 - GIGAZINE

また、マイクロソフトのマージンは、15%です。ただし、マイクロソフトの場合は、米国からの支払いとなるので、米国の税金が取られるようです。アップルは分かりません。なので、どちらに利があるかは、一概に比較できません。余談ですが、Appleは、審査もマイクロソフトに比べて厳しいので、GUIを大分見直す必要があります。

■Excelとの親和性

ソフトの性質上、デスクトップアプリであり、Excelとの連携・親和性が必須です。


2024年4月5日金曜日

Q.無償版を今まで騙し騙し使っていました。買い切り版を導入したのですが、旧プロジェクトで求解できません。

 Ans.

買い切り版をお買い上げ頂きありがとうございます。

ソフトウェアは、常にバージョンアップしています。無償版での旧プロジェクトを含めて、下位互換を実現しています。適正な記述であれば、新しいバージョンでもそのまま読み込み、実行が可能です。

しかしながら、新しいバージョンでは、より不正な制約記述に対してエラーチェックを厳しくしており、無償版ではエラーが出なかったものが、新しい版ではエラーが発生することは考えられます。求解ページに何等かのエラーメッセージが赤字である筈ですので、エラーメッセージに従ってエラーを潰してください。

もし、何も表示されない場合は、恐れ入りますが当該プロジェクトをサポートまで送って頂くようお願いします。記述修正をして返送します。

→**その後、連絡があり自力で記述修正をして動いているとのことです。


2024年4月4日木曜日

 Q.10台まで接続可能というのは、インストール後にアンインストール をすれば接続可能台数のカウントが元に戻るということでしょうか?

 Ans.いいえ、アンインストールしてもアカウントとマシンは紐づけされたままです。紐づけは、ソフトではなくマシンで行われているためです。

ですので、自宅のPC等、不要となったマシンの紐づけを解除するには、以下のようなマイクソフトアカウント上で操作します。(アンインストール済とします。)


ストアにサインインします。

ご自分のアイコンが表示されていると思いますので、クリックすると次のような画面が出ます。アカウントとデバイスの管理をクリックします。

ご自分のマイクロソフトアカウントページが開きます。下の方にデバイスの表示があります。「全てのデバイスの表示」をクリックします。
私の場合、下記5台が紐づいています。今NOTE-PCのマシンの紐づけを解除したいとします。
Note-PCをクリックします。


「詳細を見る」をクリックします。

「このデバイスを削除」で紐づけを解除します。
以上です。


2024年4月3日水曜日

課題整理

課題メモです。


 1)icu 70人問題

夜勤10人という制約で、長日勤10人、入り10人、明け10人という規模の問題に対して現状6分位時間がかかっています。これを32threads cpuで実行したときに2分以下となるようにしたい。Algorithm1の再設計。

2)SchedulingBenchmark記録更新問題

大容量3次キャッシュを積んだCPUで、記録更新を狙いたい。Alrogirhm1の再設計とAlgorithm3/4の整数化機構再設計 Coptの採用検討(評価ライセンスを長期にもらえないか交渉)

3) INCR2 記録更新問題

Algorithm3/4 LowerBoundに課題。StrongBranchのDeepLearning化、再設計。2)と共通

4)ペア制約 Algorithm3/4問題

ペア制約があると、途端にAlgorithm3/4の優位性が失われる問題。ブランチングと、整数化機構の再設計

5)論文執筆

国内特許ばかりで国際的な認知がない。WEB結果では認知されない。上記新記録を結果を持って投稿。Native共著者要。

6)英語本

英語Kindle本化。英語講義・トレーニングプロジェクト作成

7)AIモデル化

LLMのファインチューニングでJSONを出力させる。プロジェクトの自動作成支援


課題が多すぎですが、サポートもしっかり行いつつ、一歩一歩進めていきます。

1)に関しては、5月中の性能評価を目指しています。2)ー6)に関しては、今年前半に目途を付けたいと思っています。7)に関しては面白いテーマだと思います。私の方は、ソルバの高性能化で手が回りませんが、面白い研究ネタだと思います。




2024年4月1日月曜日

Intel SAT Solver Windows port

 プロジェクトファイルは附属していますが、そのままでは動きません。Windowsにポートしたときのメモ


1)namespace Topor 追加@TopiWL.cc

 Topor::CTopi<TLit, TUInd, Compress>::TULit* CTopi<TLit, TUInd, Compress>::WLPrepareArena(TULit l, bool allowNewBinaryWatch, bool allowNewLongWatch)

2) NOMINMAX define 追加::max()がマクロで置き換えられる問題回避

4) SKIP_ZLIB define 追加 ZLIB使用しない

5)popen/pclose をfopen/flcoseに代替え UNIX用を置き換え

6)ソース追加 

TopBitcompression.cc  TopiInprocess.cc