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
によるとパラレル部門で好結果が出ています。