SATソルバーの最新動向と利用技術  [in Japanese] Recent Advances in SAT Solvers and their Utilization Technologies.  [in Japanese]

Access this Article

Search this Article

Author(s)

Abstract

<p>命題論理式の充足可能性判定(SAT)問題を解くプログラムであるSATソルバーは,2000年以降その性能面において飛躍的に進化した.それに伴い,解きたい問題をSAT符号化によりSAT問題へと変換し,SATソルバーを用いて解くSAT型システムが,プランニング,ソフトウェア・ハードウェア検証,スケジューリング問題など様々な分野で成功を収めるようになった.本稿では,まずSATソルバーの最新動向として,性能面と機能面における進化をその要因の1つであるSATソルバーの国際競技会の視点から説明を行う.次に SAT ソルバーの利用技術の視点から,SAT ソルバーの機能面の進化と符号化技術を組み合わせることで,複雑な問題を解くことが可能になることの説明を行う.そのような例として多目的最適化問題のパレート解をSATソルバーを利用して求める方法を説明する.</p>

<p>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.</p>

Journal

  • Computer Software

    Computer Software 35(4), 72-92, 2018

    Japan Society for Software Science and Technology

Codes

  • NII Article ID (NAID)
    130007552525
  • NII NACSIS-CAT ID (NCID)
    AN10075819
  • Text Lang
    JPN
  • Article Type
    journal article
  • ISSN
    0289-6540
  • NDL Article ID
    029343321
  • NDL Call No.
    Z14-1033
  • Data Source
    NDL  IR  J-STAGE 
Page Top