文献

J-GLOBAL ID：201102203404431747   整理番号：11A0128919

SAT変換に基づく制約ソルバーとその性能評価

A SAT-based Constraint Solver and its Performance Evaluation

著者 (3件)： 田村直之 (神戸大学情報基盤センター) ,  丹生智也 (神戸大学大学院工学研究科) ,  番原睦則 (神戸大学情報基盤センター)
資料名： コンピュータソフトウェア  (Computer Software)
巻： 27  号： 4  ページ： 4.183-4.196 (J-STAGE)  発行年： 2010年 
JST資料番号： Y0628A  ISSN： 0289-6540  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 本論文では,SAT変換に基づく制約ソルバーであるSugarの概要とその性能評価結果について述べる.Sugarは,制約充足問題(CSP),制約最適化問題(COP)および最大制約充足問題(Max-CSP)を,命題論理の充足可能性判定問題(SAT問題) に変換し,MiniSat等の高速なSATソルバーを用いて求解を行うシステムである.SAT変換には,order encodingと名付けた新しい方法を用いており,従来広く用いられているdirect encodingやsupport encodingよりも,多くの問題に対して高速な求解が可能である.本論文では,order encodingの説明を含めたSugarの概要について述べた後,2008年に開催された第3回国際CSPソルバー競技会およびMax-CSPソルバー競技会での結果を基にSugarの性能評価結果を報告する.なお,Sugarは同競技会の10部門のうち4部門で第1位となった.(著者抄録)

シソーラス用語： *応用プログラム ,  *問題解決 ,  性能評価 ,  命題論理 ,  *充足可能性問題 ,  制約充足問題 ,  制約付最適化問題 ,  決定問題 ,  人工知能 ,  ジョブショップスケジューリング ,  符号化 ,  形式記述
準シソーラス用語： ソルバ

分類 (2件)： 数値計算  (JE02000J) ,  その他のオペレーションズリサーチの手法  (KA03070E)

タイトルに関連する用語 (4件)： SAT ,  制約 ,  ソルバー ,  性能評価