SAT問題と他の制約問題との相互発展 Interplay between SAT and Other Constraint Problems

この論文にアクセスする

著者

    • 酒井 政裕 SAKAI Masahiro
    • 株式会社東芝研究開発センターシステム技術ラボラトリ― System Enginering Laboratory, Corporate Research & Development Center
    • 今井 健男 IMAI Takeo
    • 株式会社東芝研究開発センターシステム技術ラボラトリ― System Enginering Laboratory, Corporate Research & Development Center

抄録

SAT問題は,命題論理式の充足可能性問題,すなわち命題変数を含む論理式に対し,その論理式を真にするような命題変数への値の割り当てが存在するかを決定する問題である.SATは古典的なNP完全問題であり,計算量的には難しい問題であるものの,近年のアルゴリズムの改良とハードウェアの進化によって著しい高性能化が実現された結果として,様々な分野への応用が行われている.本稿ではSATにまつわる研究で現在活発な領域として,関連する問題クラスへの応用やそれにまつわる研究分野との間の交流について,調査し,紹介する.

Boolean SATisfiability problem (hereafter SAT) is the problem of deciding whether there exists an assignment to variables in a given propositional formula that makes the formula true. SAT is a computationally difficult problem as it is a classical NP-complete problem, but development of practically fast algorithms and hardware speed-ups enable SAT solvers to be used in variety of real applications.<BR>In this paper, we survey applications of SAT algorithms into broader problem classes, and technical interplays between SAT research and other research fields around those problem classes.

収録刊行物

  • コンピュータ ソフトウェア

    コンピュータ ソフトウェア 32(1), 1_103-1_119, 2015

    日本ソフトウェア科学会

各種コード

  • NII論文ID(NAID)
    130004892312
  • 本文言語コード
    JPN
  • ISSN
    0289-6540
  • データ提供元
    J-STAGE 
ページトップへ