文章基本信息

标题：SAT型制約プログラミングシステムと周辺技術
本地全文：下载
作者：宋剛秀 ; 番原睦則 ; 田村直之等
期刊名称：コンピュータソフトウェア
印刷版ISSN：0289-6540
出版年度：2017
卷号：34
期号：1
页码：1_67-1_80
DOI：10.11309/jssst.34.1_67
出版社：Japan Society for Software Science and Technology
摘要：近年SATソルバーの求解性能が飛躍的に向上しており，様々な分野で応用が進んでいる．しかし，SATソルバーは連言標準形の命題論理式を入力としており，実用的な応用が多くある算術制約を含むような問題を直接記述して解くことには向いていない．このため，より表現力のある入力形式に対応できるようにSATソルバーを利用・拡張したシステムが研究されている．本解説では，そのような利用・拡張の1つとしてSATソルバーの求解性能と制約プログラミングシステムの表現力を融合させたSAT型制約プログラミングシステム(SAT型CPシステム)について説明し，その周辺技術についても概説する．