MaxSATソルバーのSATソルバーを何にするか

http://www.lab2.kuis.kyoto-u.ac.jp/minato/ToDA2018/ToDA2018-5.pdf

で初めて知ったのですがKnuth大先生がSATCompetitionに出ておられてたのですね。当時75歳だそうです。
現在のSATソルバーは、その起源をほぼ2005年のMiniSATに持っています。でその後Glucoseが出て、しばらく停滞したのですが、近年機械学習のPrincipleをSATソルバーに適用したMapleSATでさらに性能が向上しました。現在の最新ソルバーは、MapleSATの手法を使っていると思います。

通常、SATソルバーというと系統的ソルバーを指しますが、確率的ソルバーというのもあります。実は、系統的ソルバーは、機械的に生成したRANDOM　CNF対しては、無力です。強いのは、Industrial問題です。系統的ソルバは、広大な探索空間を全てスキャンしたのと同じ結果になります。単純に考えても分かるのですが、僅か32変数でも4G空間です。RANDOMだと、分布に癖がないということがネックになります。逆に分布に癖があるのがIndustrial問題です。通常ナーススケジューリング問題をCNFに落とすと、RANDOMになることはなく、系統的ソルバで問題になることはありません。しかしながら、前のMaxSAT　Competitionでは、人工的に生成したRANDOM問題が含まれていて、これがほとんど全滅でした。なので、RANDOM問題に強い確率ソルバーを前段に持ってきて対処した経緯があります。が、その後RANDOM問題は、MaxSATCompetitionで排除されるようになったので、現在は不要のはずです。（役にたっていません。）

　で、ここ1年は、SATソルバーの進歩を見ていなかったのですが、ちょっとSurveryしてみました。
興味深いソルバーがありました。
https://github.com/togatoga/togasat
MiniSATの実装をさらに現代的なC++で書き換えたようなソルバーで、オリジナルMiniSATより多分速いのではないでしょうか？

　実装にあたっては、ライセンスも重要で、例えば、最新VersionのGlucoseでは、Parallelの使用に制限があり商用での使用は難しそうです。CryptominisatのようにずっとMITを維持した実装もあります。
Condaの開発者が、好結果を表明しています。
https://github.com/msoos/cryptominisat/issues/513

2018年のCompetition結果
http://sat2018.forsyte.tuwien.ac.at/downloads/satcomp18slides.pdf
によるとパラレル部門で好結果が出ています。

MaxSAT2019

https://maxsat-evaluations.github.io/2019/

です。去年は、参加を見送ったのですが、今年は、どうしようかと思っています。今年は、ポルトガル、リスボンです。行ってみるのもいいかも。
それはともかく、ベンチマークも募集しているので、ナーススケジューリング問題をMAXSAT形式にして、送るのもありです。興味のある方は是非ご参加を。
　私の方は、新しいMaxSATの実装を完成させるのが第一優先です。これは、新しいソルバの一部になります。その後、関連特許出願して、実装評価する余裕があれば、ということになるので、時間的にまにあうかどうかはまだ分かりません。なお新たに設計したMaxSAT部のみ、現在のリリースに追加して、リリース予定です。

　

組合せ最適化の近似解法の設計方針

http://research.nii.ac.jp/~uno/approx.htm

宇野先生のページに載っている通りの解法があります。
目指しているのは、厳密解を目標にしつつ、必要なら途中途中で解を得るような方法です。
　

ナーススケジューリング問題としては、最近シミュレーテッドアニーリングで成果が出ているので、
こちらについても見てみたいのですが、残念ながら上記の要件を満たすことは難しいです。
メタヒューリスティクスでは、高速に近似解を得ることができますが、CPUパワーをそちらに摂られてしまうと、厳密解パワーに廻せなくなってしまいます。極初期に、少しだけ使うのは、意味があると思いますが、厳密解の50%や20%程度の劣化を意識したところでは、かなり難しいと感じています。

　現在は、途中途中でMaxSATソルバを動かしていますが、このままですと、かなり性能が悪く、近似解でも良い解が中々出てきません。具体的には、厳密解近くまで来ないと中々良い解になりません。INRC2の8WEEKSが厳密解近くの解を出すまでには、丸一日程度かかるのですが、それらしい近似解の出力にもあまり変わらない時間であり、今のままだと全く実用的ではありません。
（実は、問題領域をどこにするかで、得意なソルバの種類は違ってきます。今問題にしているのは、INRC2の8WEEKS程度でのお話です。この辺の話も後で。かなり色々な事が分かってきました。）

そこで、上記主旨を踏まえて、MAXSATソルバを新たに設計することにしました。新しい挑戦です。

久々にメンテ

VeritakSVという公開していないverilogシミュレータがあるのですが、Windows10で突然動かなくなったという報告がいくつかあり久々にメンテしました。その際、VisualC++2015に環境を移したのですが、コンパイルが通らなかった記述が数十箇所あり、C++でも、いまだにそういう状態なんだ、
という思いをしました。2012年位まで書いていたのですが、クラスの実装をやり始めたところで、その時点で、C++ソースは20万行を越えていて、その後断念しました。というか、SystemVerilogの検証言語部の実装を検討していたときにSAT技術について学んで、妻の勤務表に使えないかなと思って取り組ん結果が、そちらが本業になってしまいました。
一部のコアユーザにのみ提供していて、未だに使っている人があるようです。

https://bellard.org/tcc/　というTinyCコンパイラをハックしたコード生成を使っているので、とても高速です。(VMコードの10倍速い) 今だったら良いバックエンド(LLVMとか幾つかある）ので、もう少しましな方法を採るでしょう。

ナーススケジューリングで厳密解は得られるか？

現在の技術と計算機資源で、どんな問題でも厳密解が得られるようになったか？という問題についてです。

勿論、ナーススケジューリングは、NP困難な問題であるので、規模が大きくなれば自ずと答えは否です。しかしながら、通常遭遇する一般的な問題についての観測と感想です。
　現在開発中のソルバは、INRC-IIのほぼ全ての問題について既存のKnownBest記録を塗り替えることができますが、そのうち厳密解が得られたのはほんの僅かでした。（一週間廻しても証明できませんでした。）従って、この結果をもってしても、通常問題で厳密解を得ることは難しそうだということが言えます。 特に、INRC-IIの問題は、行制約のほとんどがソフト制約であり、ソルバ的には、難しい問題です。一方、SchedulingBenchmarkサイト問題は、行制約のソフト制約はありません。その結果、長大規模な問題を除いて、厳密解が得られています。
以上の、観測から、ナーススケジューリングの現状の技術では、世界最高性能のソルバをもってしても「厳密解が得られない問題もある」、ということをご理解頂きたいと思います。一方で、大きな規模でも厳密解が得られる場面もあります。この差についての考察は、後日に。

これまでは、厳密解を得ることに挑んできましたが、実用的には、近似解でも早く結果が欲しい訳で、その部分の改善が残っています。こちらは、根底から設計する必要はありません。厳密解を得るソルバに手を加えていけばよいです。しかしながら、未だアイデア段階であり、これからFeasibilityStudy・設計・実装となります。

導入について

導入を検討されているお客様向けに資料を作成しました。

きっかけは、障碍者施設・児童擁護施設向けのご相談があったからです。

児童養護施設の勤務実態は複雑多岐にわかれており、厚労省の指導では大舎制の否定、小規模グループホーム化を推奨しており、その分職員の勤務が多岐に分かれて、手作業による勤務表の作成は困難を極めています。

とのことで、大変にご苦労されているようです。最近の児童虐待のニュースを耳にするにつけ、これら施設の重要性が高まってきていると思います。働く現場の方々に少しでもお役に立てたらと思います。

スケジュールナースでは、勤務表作成・組合せ最適化に関するコンサルティングも行っております。お気軽にお問い合わせください。