最近気になった論文

 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倍以上が必要と考えます。その意味で、重要なのはアルゴリズムです。新しいアーキテクチャでは、速度向上が体感できると思います。

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

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

Ans.

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

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

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

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

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

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

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

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

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

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

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

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

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

 Ans.

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

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

否定集合を作り、

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

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

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

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

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

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

Ans.

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

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

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

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

 Ans.

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

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

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

６回＝１回２人　２回２人

６回＝２回　３人

６回= 3回　２人

6回=3回１人　１回１人　２回1人

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

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

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

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

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

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

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

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

6回=3回１人　１回１人　２回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)
        
   
    

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

 Ans.

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

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

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

問題は、二つあり

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

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

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

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

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

ペア制約での記述でも間違いではありませんが、Betterな記述は、次のように列制約で記述します。

このとき、スタッフプロパティは、以下のようにします。

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

■ペア制約で個人名を使わずに記述可能。スタッフプロパティシートは毎月変更するので、スタッフの退職・入職等の変更等のメンテナンスはこのシートを弄ることになります。制約は時が経つと忘れてしまいますが、このシートは、全項目をメンテする、とだけ覚えておけばよい。

■ペア集合１、２、３の変更はスタッフプロパティシート上で自由である。また複数人数のペア禁止も可能、使わなければブランクでもOK。列制約で制約したことは忘れてよい。メンテナンス性が良い。より汎用的であり、将来の変更のし易さが違います。

■ペア制約では、「看護師男」、「介護男」と集合を分けて記述する必要がありますが、このスタイルでは、「男」だけで記述でき、新たに集合を合成する必要がない