SAT-based Constraint Programming Systems and Related Technologies
SAT-based Constraint Programming Systems and Related Technologies
复制标题
基于SAT的约束规划系统及相关技术
DOI：
10.11309/jssst.34.1_67
复制
发表时间：
2017
影响因子：
--
通讯作者：
田村直之
中科院分区：
文献类型：
--
作者：
宋剛秀;番原睦則;田村直之
近年 SAT ソルバーの求解性能が飛躍的に向上しており, 様々な分野で応用が進んでいる. しかし, SAT ソルバーは連言標準形の命題論理式を入力としており, 実用的な応用が多くある算術制約を含むような問題を直接記述して解くことには向いていない. このため, より表現力のある入力形式に対応できるように SAT ソルバーを利用・拡張したシステムが研究されている. 本解説では, そのような利用・拡張の 1 つとして SAT ソルバーの求解性能と制約プログラミングシステムの表現力を融合させた SAT 型制約プログラミングシステム (SAT 型 CP システム) について説明し, その周辺技術についても概説する.