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

Abstract

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