拡張融合法を用いた高速SATソルバの研究開発

• 研究課題/領域番号: 17K12742
• 研究種目: 若手研究(B)
• 配分区分: 基金
• 研究分野: 知能情報学
• 研究機関: 国立情報学研究所
• 研究代表者: 薗部 知大 国立情報学研究所, ビッグデータ数理国際研究センター, 特任研究員 (50747269)
• 研究期間 (年度): 2017-04-01 – 2023-03-31
• 研究課題ステータス: 完了 (2022年度)
• 配分額: 2,470千円 (直接経費: 1,900千円、間接経費: 570千円); 2019年度: 910千円 (直接経費: 700千円、間接経費: 210千円); 2018年度: 910千円 (直接経費: 700千円、間接経費: 210千円); 2017年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
• キーワード: 充足可能性問題 / SATソルバ / 探索

研究成果の概要

充足可能性問題(SAT問題)は計算機科学の重要な問題として知られていて、この問題を解くためのプログラムであるSATソルバは、実世界の問題を解くために使用されているため、高速化の意義は高い。本研究では、従来のSATソルバで使用されている融合法をより強力にした拡張融合法を用いて、鳩の巣原理問題に対して効果的な手法の提案を行った。

研究成果の学術的意義や社会的意義

充足可能性問題(SAT問題)を解くSATソルバは、回路検証、コンピュータプログラムのバグ発見、数学的問題の解決、暗号解析等、現実世界の様々な問題の解を高速に求められる水準に達し、更なる発展が期待されている。本研究では、SATソルバに対して、より理論的に強力であると考えられている拡張融合法を組み込むことを目的として、鳩の巣原理問題に対して、従来のSATソルバの高速化を達成した。

研究成果

• [雑誌論文] An Experimental Survey of Extended Resolution Effects for SAT Solvers on the Pigeonhole Principle (2022)
  • 著者名/発表者名: Sonobe Tomohiro
  • 雑誌名: Algorithms 巻: 15 号: 12 ページ: 479-479
  • DOI: 10.3390/a15120479
  • 査読あり / オープンアクセス
• [雑誌論文] Variable Selection with PageRank for SAT Solvers (2019)
  • 著者名/発表者名: Sonobe Tomohiro
  • 雑誌名: Journal of Computer Science 巻: 15 号: 8 ページ: 1074-1084
  • DOI: 10.3844/jcssp.2019.1074.1084
  • 査読あり / オープンアクセス
• [学会発表] SATソルバを参考にした行列のフルランク性の判定手法 (2018)
  • 著者名/発表者名: 町出智也,薗部知大
  • 学会等名: 人工知能学会全国大会