ソフト制約の意味

池上先生のインスタンスは、非常に特殊でして、数理的に、まともにコンパイルしようとすると「はまります」　どういうことかというと、ハード制約がないのです。これがどういう背景かは、御著書の20ページに書いてあります。　

これに対して、他の全てのナーススケジューリングベンチマークには、ソフト制約とハード制約が分離して記述されます。

　＜ハード制約がないと..＞
なにが起きるかというと探索空間が全く縮小されないのです。シフト数・日数・スタッフ数で決まるだけの組合せ空間が全く縮小されないことになってしまいます。例えば、シフト数7・日数31としましょう。ありえる組合せは、7**31=1.5e26　が一人のナースについてのありえる空間です。ハード制約があれば、探索空間は、小さくなります。勿論、ウェイトをつけて、ほとんど起こりそうにないことを記述することは出来ます。が、それにしても探索空間からそれを除外することは出来ません。絶対に起こらないという保証がある場合とない場合とでは、全く意味が異なります。ウェイトがついた場合には、探索空間の縮小は起こりません。ソフト制約では、探索空間が縮小されることはないのです。

そういう訳で、現実的な意味で、ハード制約がないナーススケジューリング問題を解くのは、技術的に非常に困難です。その問題が、エラーがない、もしくは、少ないエラー数で済むと分かっているのなら、やり方はあります。が、もし、INRC2や、SchedulingBenchmarkSuite並みのエラー数となる問題があるとしたら、厳密解は、現状の技術では、難しいと言わざるをえません。（　なので、ベンチマーク集では、必ずハード制約とソフト制約がある訳です。）

　＜ハード制約が多すぎると＞
なにかの条件で、解がない事態となる確率が増えます。この事態が起きないように適度なソフト制約を付加する必要があります。

＜ソフト制約が多すぎると＞
上のような事情で、探索時間が増えます。

新しいソルバでは、リニアウェイトのモードを作りました。遅くなる場合もありますが、エラーが多い場合には、体感的にそちらの方がフィットするかもしれません。また、エラーが多いときに、時間がかかっても厳密解を目指したい場合（or for competition)、数理的ソルバもあります。
単体指定指定すること、あるいは、おまかせでソルバを選ぶモード等、複数のOptionをつけようかと思っています。いずれにしても、一つのソルバで済む世界ではないというのが結論です。別件の仕事が入ったので、リリース日程は、後述。

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の文化なのだと思います。

今のところ、時間はないのですが、余裕が出たら試してみたいと思います。