SAT型制約プログラミングシステムと周辺技術  [in Japanese] SAT-based Constraint Programming Systems and Related Technologies  [in Japanese]

Access this Article

Author(s)

Abstract

近年SATソルバーの求解性能が飛躍的に向上しており,様々な分野で応用が進んでいる.しかし,SATソルバーは連言標準形の命題論理式を入力としており,実用的な応用が多くある算術制約を含むような問題を直接記述して解くことには向いていない.このため,より表現力のある入力形式に対応できるようにSATソルバーを利用・拡張したシステムが研究されている.本解説では,そのような利用・拡張の1つとしてSATソルバーの求解性能と制約プログラミングシステムの表現力を融合させたSAT型制約プログラミングシステム(SAT型CPシステム)について説明し,その周辺技術についても概説する.

In recent years, the performance of SAT solvers have been enormously improved and its applications are enlarged in various domains. However, SAT solvers are not adequate to directly solve problems such as the one including arithmetic constraints which has many realistic applications since the input of SAT solvers is propositional formulae of conjunction normal form. Therefore, there have been researches for systems extending and/or utilizing SAT solvers so that these can adopt more rich expressions. In this paper, we explain one of such systems—SAT-based constraint programming systems which are the integration of the performance of SAT solvers and the rich expressions of constraint programming systems. We also briefly explain related technologies of SAT-based constraint programming systems.

Journal

  • Computer Software

    Computer Software 34(1), 1_67-1_80, 2017

    Japan Society for Software Science and Technology

Codes

  • NII Article ID (NAID)
    130006855237
  • Text Lang
    JPN
  • ISSN
    0289-6540
  • Data Source
    J-STAGE 
Page Top