文献

J-GLOBAL ID：201402200323843300   整理番号：14A1307276

Scala上で実現されたSAT型制約プログラミングシステムのための開発ツール

著者 (3件)： 宋剛秀 (神戸大 情報基盤セ) ,  番原睦則 (神戸大 情報基盤セ) ,  田村直之 (神戸大 情報基盤セ)
資料名： 日本ソフトウェア科学会大会講演論文集(CD-ROM)  (日本ソフトウエア科学会大会講演論文集(CD-ROM))
巻： 31st  ページ： ROMBUNNO.SOFUTO1-1  発行年： 2014年 
JST資料番号： X0080B  ISSN： 1348-0901  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 命題論理の充足可能性判定(SAT)問題を解くプログラムであるSATソルバーが2000年以降大きく進歩しており,活発に開発と研究が行われている。このような背景から,様々な分野でSATソルバーを利用したSAT型システムが成功をおさめるようになった。通常SAT型システムには,与えられた問題をSAT問題へと符号化する専用のプログラムが必要になるが,この開発コストのために制約モデルや符号化方法など問題を解くうえで重要な役割を担う部分に注力できないという問題があった。本論文ではSAT型システムのための開発ツールであるScarabを提案する。Scarabは制約プログラミングのためのドメイン特化言語,SAT符号化モジュール,SATソルバーへのインターフェースから構成されており,SAT型制約プログラミングシステム開発者を対象に,表現性,変更容易性,効率性を備えたワークベンチを提供することを目的としたツールである。Scarabはオブジェクト指向言語と関数型言語が融合されたScala言語上にコンパクトに実装されている。バックエンドのSATソルバーにJavaで実装されたSat4jを用いることにより,インクリメンタル解法等の高度な解法を容易に実現できる点も特長の一つである。(著者抄録)

シソーラス用語： *制約プログラミング ,  支援プログラム ,  *ソフトウェア開発 ,  *充足可能性問題 ,  符号化 ,  システムインタフェイス ,  モジュール構造 ,  オブジェクト指向言語 ,  関数型言語 ,  実装設計 ,  Java
準シソーラス用語： ソフトウェアツール

分類 (2件)： 計算機システム開発  (JD02010R) ,  論理代数  (JB03000H)

タイトルに関連する用語 (4件)： SAT ,  制約プログラミング ,  開発 ,  ツール