SATソルバーの最新動向と利用技術

摘要

命題論理式の充足可能性判定(SAT)問題を解くプログラムであるSATソルバーは，2000年以降その性能面において飛躍的に進化した.それに伴い，解きたい問題をSAT符号化によりSAT問題へと変換し，SATソルバーを用いて解くSAT型システムが，プランニング，ソフトウェア•ハードウェア検証，スケジユーリング問題など様々な分野で成功を収めるようになった.本稿では，まずSATソルバーの最新動向として，性能面と機能面における進化をその要因の1つであるSATソルバーの国際競技会の視点から説明を行う.次にSATソルバーの利用技術の視点から，SATソルバーの機能面の進化と符号化技術を組み合わせることで，複雑な問題を解くことが可能になることの説明を行う.そのような例として多目的最適化問題のパレート解をSATソルバーを利用して求める方法を説明する.%Since 2000，SAT solvers that are programs solving SAT instances has enormously progressed in performance. Due to the performance improvement, SAT-based systems that encode problems into SAT instances and solve them by SAT solvers have succeeded in various research fields such as planning, software/hardware verification, scheduling problems, etc. In this paper, as recent advances in SAT solvers, we first explain the progress of their performance and functions from the viewpoint of the international competition of SAT solvers which is a factor of their progress. Then, from the viewpoint of utilization technologies, we explain that we can solve more complex problems by combining progressive functions of SAT solvers with encoding methods. As an example, we explain a solving method for the multiobjective optimization problems by using SAT solvers.