池上先生のインスタンスは、非常に特殊でして、数理的に、まともにコンパイルしようとすると「はまります」 どういうことかというと、ハード制約がないのです。これがどういう背景かは、御著書の20ページに書いてあります。
これに対して、他の全てのナーススケジューリングベンチマークには、ソフト制約とハード制約が分離して記述されます。
＜ハード制約がないと..＞
なにが起きるかというと探索空間が全く縮小されないのです。シフト数・日数・スタッフ数で決まるだけの組合せ空間が全く縮小されないことになってしまいます。例えば、シフト数7・日数31としましょう。ありえる組合せは、7**31=1.5e26 が一人のナースについてのありえる空間です。ハード制約があれば、探索空間は、小さくなります。勿論、ウェイトをつけて、ほとんど起こりそうにないことを記述することは出来ます。が、それにしても探索空間からそれを除外することは出来ません。絶対に起こらないという保証がある場合とない場合とでは、全く意味が異なります。ウェイトがついた場合には、探索空間の縮小は起こりません。ソフト制約では、探索空間が縮小されることはないのです。
そういう訳で、現実的な意味で、ハード制約がないナーススケジューリング問題を解くのは、技術的に非常に困難です。その問題が、エラーがない、もしくは、少ないエラー数で済むと分かっているのなら、やり方はあります。が、もし、INRC2や、SchedulingBenchmarkSuite並みのエラー数となる問題があるとしたら、厳密解は、現状の技術では、難しいと言わざるをえません。（ なので、ベンチマーク集では、必ずハード制約とソフト制約がある訳です。）
＜ハード制約が多すぎると＞
なにかの条件で、解がない事態となる確率が増えます。この事態が起きないように適度なソフト制約を付加する必要があります。
＜ソフト制約が多すぎると＞
上のような事情で、探索時間が増えます。
新しいソルバでは、リニアウェイトのモードを作りました。遅くなる場合もありますが、エラーが多い場合には、体感的にそちらの方がフィットするかもしれません。また、エラーが多いときに、時間がかかっても厳密解を目指したい場合（or for competition)、数理的ソルバもあります。
単体指定指定すること、あるいは、おまかせでソルバを選ぶモード等、複数のOptionをつけようかと思っています。いずれにしても、一つのソルバで済む世界ではないというのが結論です。別件の仕事が入ったので、リリース日程は、後述。
2019年3月4日月曜日
SATはAI?
という問いに対する一つの回答です。
https://www.google.co.jp/url?sa=t&rct=j&q=&esrc=s&source=web&cd=7&ved=2ahUKEwjvhPWPgOfgAhVIa7wKHWiJAFcQFjAGegQIBxAC&url=https%3A%2F%2Fipsj.ixsq.nii.ac.jp%2Fej%2F%3Faction%3Drepository_uri%26item_id%3D169445%26file_id%3D1%26file_no%3D1&usg=AOvVaw3f8dpBKVok_9n49folMpTr
時代は、機械学習・DeepLearningに学術的な興味が移っているようです。しかしSATはAIであるとの見方は新鮮で面白いと思いました。 (α碁や、SAT父・Booleanの話も面白い）
ところで、MaxSAT用のソルバですが、IntelのNadelさんのソルバがよい雰囲気です。2018SAT CompetitionのWinnerですし、何よりソースが短いです。Paperはこちら。
https://www.researchgate.net/publication/325968980_Chronological_Backtracking
これによれば、2017優勝ソルバMaple LCM Distに時系列バックトラッキング機能を盛り込んだもののようです。(恐らくその前は、MapleSATがベースになっているのだろうと思います。)段々名前が長くなっていきます。名前で何を受け継いできたか分かるのがまた面白いSAT Communityの文化なのだと思います。
今のところ、時間はないのですが、余裕が出たら試してみたいと思います。
https://www.google.co.jp/url?sa=t&rct=j&q=&esrc=s&source=web&cd=7&ved=2ahUKEwjvhPWPgOfgAhVIa7wKHWiJAFcQFjAGegQIBxAC&url=https%3A%2F%2Fipsj.ixsq.nii.ac.jp%2Fej%2F%3Faction%3Drepository_uri%26item_id%3D169445%26file_id%3D1%26file_no%3D1&usg=AOvVaw3f8dpBKVok_9n49folMpTr
時代は、機械学習・DeepLearningに学術的な興味が移っているようです。しかしSATはAIであるとの見方は新鮮で面白いと思いました。 (α碁や、SAT父・Booleanの話も面白い）
ところで、MaxSAT用のソルバですが、IntelのNadelさんのソルバがよい雰囲気です。2018SAT CompetitionのWinnerですし、何よりソースが短いです。Paperはこちら。
https://www.researchgate.net/publication/325968980_Chronological_Backtracking
これによれば、2017優勝ソルバMaple LCM Distに時系列バックトラッキング機能を盛り込んだもののようです。(恐らくその前は、MapleSATがベースになっているのだろうと思います。)段々名前が長くなっていきます。名前で何を受け継いできたか分かるのがまた面白いSAT Communityの文化なのだと思います。
今のところ、時間はないのですが、余裕が出たら試してみたいと思います。
2019年2月27日水曜日
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
によるとパラレル部門で好結果が出ています。
で初めて知ったのですが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
によるとパラレル部門で好結果が出ています。
2019年2月25日月曜日
MaxSAT2019
https://maxsat-evaluations.github.io/2019/
です。去年は、参加を見送ったのですが、今年は、どうしようかと思っています。今年は、ポルトガル、リスボンです。行ってみるのもいいかも。
それはともかく、ベンチマークも募集しているので、ナーススケジューリング問題をMAXSAT形式にして、送るのもありです。興味のある方は是非ご参加を。
私の方は、新しいMaxSATの実装を完成させるのが第一優先です。これは、新しいソルバの一部になります。その後、関連特許出願して、実装評価する余裕があれば、ということになるので、時間的にまにあうかどうかはまだ分かりません。なお新たに設計したMaxSAT部のみ、現在のリリースに追加して、リリース予定です。
です。去年は、参加を見送ったのですが、今年は、どうしようかと思っています。今年は、ポルトガル、リスボンです。行ってみるのもいいかも。
それはともかく、ベンチマークも募集しているので、ナーススケジューリング問題をMAXSAT形式にして、送るのもありです。興味のある方は是非ご参加を。
私の方は、新しいMaxSATの実装を完成させるのが第一優先です。これは、新しいソルバの一部になります。その後、関連特許出願して、実装評価する余裕があれば、ということになるので、時間的にまにあうかどうかはまだ分かりません。なお新たに設計したMaxSAT部のみ、現在のリリースに追加して、リリース予定です。
2019年2月23日土曜日
組合せ最適化の近似解法の設計方針
http://research.nii.ac.jp/~uno/approx.htm
宇野先生のページに載っている通りの解法があります。
目指しているのは、厳密解を目標にしつつ、必要なら途中途中で解を得るような方法です。
ナーススケジューリング問題としては、最近シミュレーテッドアニーリングで成果が出ているので、
こちらについても見てみたいのですが、残念ながら上記の要件を満たすことは難しいです。
メタヒューリスティクスでは、高速に近似解を得ることができますが、CPUパワーをそちらに摂られてしまうと、厳密解パワーに廻せなくなってしまいます。極初期に、少しだけ使うのは、意味があると思いますが、厳密解の50%や20%程度の劣化を意識したところでは、かなり難しいと感じています。
現在は、途中途中でMaxSATソルバを動かしていますが、このままですと、かなり性能が悪く、近似解でも良い解が中々出てきません。具体的には、厳密解近くまで来ないと中々良い解になりません。INRC2の8WEEKSが厳密解近くの解を出すまでには、丸一日程度かかるのですが、それらしい近似解の出力にもあまり変わらない時間であり、今のままだと全く実用的ではありません。
（実は、問題領域をどこにするかで、得意なソルバの種類は違ってきます。今問題にしているのは、INRC2の8WEEKS程度でのお話です。この辺の話も後で。かなり色々な事が分かってきました。）
そこで、上記主旨を踏まえて、MAXSATソルバを新たに設計することにしました。新しい挑戦です。
宇野先生のページに載っている通りの解法があります。
目指しているのは、厳密解を目標にしつつ、必要なら途中途中で解を得るような方法です。
ナーススケジューリング問題としては、最近シミュレーテッドアニーリングで成果が出ているので、
こちらについても見てみたいのですが、残念ながら上記の要件を満たすことは難しいです。
メタヒューリスティクスでは、高速に近似解を得ることができますが、CPUパワーをそちらに摂られてしまうと、厳密解パワーに廻せなくなってしまいます。極初期に、少しだけ使うのは、意味があると思いますが、厳密解の50%や20%程度の劣化を意識したところでは、かなり難しいと感じています。
現在は、途中途中でMaxSATソルバを動かしていますが、このままですと、かなり性能が悪く、近似解でも良い解が中々出てきません。具体的には、厳密解近くまで来ないと中々良い解になりません。INRC2の8WEEKSが厳密解近くの解を出すまでには、丸一日程度かかるのですが、それらしい近似解の出力にもあまり変わらない時間であり、今のままだと全く実用的ではありません。
（実は、問題領域をどこにするかで、得意なソルバの種類は違ってきます。今問題にしているのは、INRC2の8WEEKS程度でのお話です。この辺の話も後で。かなり色々な事が分かってきました。）
そこで、上記主旨を踏まえて、MAXSATソルバを新たに設計することにしました。新しい挑戦です。
2019年2月20日水曜日
久々にメンテ
VeritakSVという公開していないverilogシミュレータがあるのですが、Windows10で突然動かなくなったという報告がいくつかあり久々にメンテしました。その際、VisualC++2015に環境を移したのですが、コンパイルが通らなかった記述が数十箇所あり、C++でも、いまだにそういう状態なんだ、
という思いをしました。2012年位まで書いていたのですが、クラスの実装をやり始めたところで、その時点で、C++ソースは20万行を越えていて、その後断念しました。というか、SystemVerilogの検証言語部の実装を検討していたときにSAT技術について学んで、妻の勤務表に使えないかなと思って取り組ん結果が、そちらが本業になってしまいました。
一部のコアユーザにのみ提供していて、未だに使っている人があるようです。
https://bellard.org/tcc/ というTinyCコンパイラをハックしたコード生成を使っているので、とても高速です。(VMコードの10倍速い) 今だったら良いバックエンド(LLVMとか幾つかある）ので、もう少しましな方法を採るでしょう。
という思いをしました。2012年位まで書いていたのですが、クラスの実装をやり始めたところで、その時点で、C++ソースは20万行を越えていて、その後断念しました。というか、SystemVerilogの検証言語部の実装を検討していたときにSAT技術について学んで、妻の勤務表に使えないかなと思って取り組ん結果が、そちらが本業になってしまいました。
一部のコアユーザにのみ提供していて、未だに使っている人があるようです。
https://bellard.org/tcc/ というTinyCコンパイラをハックしたコード生成を使っているので、とても高速です。(VMコードの10倍速い) 今だったら良いバックエンド(LLVMとか幾つかある）ので、もう少しましな方法を採るでしょう。
2019年2月11日月曜日
ナーススケジューリングで厳密解は得られるか？
現在の技術と計算機資源で、どんな問題でも厳密解が得られるようになったか？という問題についてです。
勿論、ナーススケジューリングは、NP困難な問題であるので、規模が大きくなれば自ずと答えは否です。しかしながら、通常遭遇する一般的な問題についての観測と感想です。
現在開発中のソルバは、INRC-IIのほぼ全ての問題について既存のKnownBest記録を塗り替えることができますが、そのうち厳密解が得られたのはほんの僅かでした。（一週間廻しても証明できませんでした。）従って、この結果をもってしても、通常問題で厳密解を得ることは難しそうだということが言えます。 特に、INRC-IIの問題は、行制約のほとんどがソフト制約であり、ソルバ的には、難しい問題です。一方、SchedulingBenchmarkサイト問題は、行制約のソフト制約はありません。その結果、長大規模な問題を除いて、厳密解が得られています。
以上の、観測から、ナーススケジューリングの現状の技術では、世界最高性能のソルバをもってしても「厳密解が得られない問題もある」、ということをご理解頂きたいと思います。一方で、大きな規模でも厳密解が得られる場面もあります。この差についての考察は、後日に。
これまでは、厳密解を得ることに挑んできましたが、実用的には、近似解でも早く結果が欲しい訳で、その部分の改善が残っています。こちらは、根底から設計する必要はありません。厳密解を得るソルバに手を加えていけばよいです。しかしながら、未だアイデア段階であり、これからFeasibilityStudy・設計・実装となります。
勿論、ナーススケジューリングは、NP困難な問題であるので、規模が大きくなれば自ずと答えは否です。しかしながら、通常遭遇する一般的な問題についての観測と感想です。
現在開発中のソルバは、INRC-IIのほぼ全ての問題について既存のKnownBest記録を塗り替えることができますが、そのうち厳密解が得られたのはほんの僅かでした。（一週間廻しても証明できませんでした。）従って、この結果をもってしても、通常問題で厳密解を得ることは難しそうだということが言えます。 特に、INRC-IIの問題は、行制約のほとんどがソフト制約であり、ソルバ的には、難しい問題です。一方、SchedulingBenchmarkサイト問題は、行制約のソフト制約はありません。その結果、長大規模な問題を除いて、厳密解が得られています。
以上の、観測から、ナーススケジューリングの現状の技術では、世界最高性能のソルバをもってしても「厳密解が得られない問題もある」、ということをご理解頂きたいと思います。一方で、大きな規模でも厳密解が得られる場面もあります。この差についての考察は、後日に。
これまでは、厳密解を得ることに挑んできましたが、実用的には、近似解でも早く結果が欲しい訳で、その部分の改善が残っています。こちらは、根底から設計する必要はありません。厳密解を得るソルバに手を加えていけばよいです。しかしながら、未だアイデア段階であり、これからFeasibilityStudy・設計・実装となります。
登録:
投稿 (Atom)