SATソルバーとCASを組み合わせた組合せ予想の検証（2016年）
本論文では、SATソルバーと数式処理システム（CAS）を組み合わせて、組合せ論における未解決予想を検証する手法を提案している。具体的には、RAMBOと呼ばれる手法を用いて、問題を満足可能性問題に変換し、SATソルバーで解を探索するとともに、CASを活用して対称性の除去や補題の生成を行うことで、大規模な組合せ問題の自動検証を実現する。応用例として、ラムゼー理論やスターリング数の組合せ恒等式などの検証が示されている。
背景メモ
「SATソルバーと数式処理システム（CAS）を連携させて組合せ論の予想を検証する」という2016年の論文。SATソルバーは命題論理式の充足可能性を判定するプログラムで、近年ハードウェア検証や数论などで実績を積んでいる。一方CAS（MathematicaやMapleなど）は記号計算を得意とする。両者を組み合わせることで、大規模な有限探索が必要な組合せ論の未解決問題（例：van der Waerden数、Schur数）を効率的に証明できたと報告している。著者らはアーカンソー大学とケンブリッジ大学に所属する数学・情報科学の研究者で、この手法は「SAT+CAS」方式と呼ばれ、その後も素数のパターンやラムゼー理論などに応用が拡大している。背景として、2010年代にSATソルバーの性能が飛躍的に向上し、数学証明の自動化への関心が高まっていた時期にあたる。