SATソルバーを用いた制約プログラミングシステムとその応用

• Item type: Symposium_02(1)
• 公開日: 2016-01-08
• タイトル: SATソルバーを用いた制約プログラミングシステムとその応用
• タイトル / 言語: en
• タイトル: SAT-based Constraint Programming Systems and its Applications
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: SATソルバー，制約プログラミング，ドメイン特化言語
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_5794
• 資源タイプ: conference paper
• 著者所属: 神戸大学情報基盤センター
• 著者所属(英): en
• 著者所属(英): Information Science and Technology Center, Kobe University
• 著者名: 宋, 剛秀
• 著者名(英): Takehide, Soh
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 近年SATソルバーの求解性能は飛躍的に向上しており，様々な分野で応用が進んでいる．しかし，SATソルバーは連言標準形の命題論理式を入力としており，算術制約を含むような問題を直接記述して解くことには向いていない．このため，より表現力のある入力形式に対応できるようにSATソルバーを利用・拡張したシステムが研究されている．本稿で説明するSAT型制約プログラミングシステム Scarab は，制約充足問題 (CSP) を簡潔に表現できる高い記述性，CSPをSATに符号化した後，密に連携したSATソルバーを実行することによる高い求解性をもっている．本稿ではScarabの設計方針と制約記述のためのドメイン特化言語を説明した後，いくつかのプログラム例を通してScarabを用いたアプリケーション開発の利点を明らかにする．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: In recent years, the performance of SAT solvers have been enormously improved and its applications are enlarged in various research domains. However, SAT solvers are not adequate to directly solve problems such as the one including arithmetic constraints 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. Our proposed SAT-based constraint programming system Scarab provides a rich constraint programming language and the high solving performance of SAT solvers by encoding CSP into SAT. In this paper, we explain the design policy and the domain-specific language of Scarab and demonstrate its advantage for the development of applications throughout some program examples.
• 書誌情報: 第57回プログラミング･シンポジウム予稿集; 巻 2016, p. 19-28, 発行日 2016-01-08
• 出版者 / 言語: ja
• 出版者: 情報処理学会