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

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