文献

J-GLOBAL ID：201402250938123096   整理番号：14A0408506

パッキング配列問題の制約モデリングとSAT符号化

Constraint Modeling and SAT Encoding of the Packing Array Problem

著者 (5件)： 則武治樹 (神戸大学大学院システム情報学研究科) ,  番原睦則 (神戸大学情報基盤センター) ,  宋剛秀 (神戸大学情報基盤センター) ,  田村直之 (神戸大学情報基盤センター) ,  井上克巳 (国立情報学研究所情報学プリンシプル研究系)
資料名： コンピュータソフトウェア  (Computer Software)
巻： 31  号： 1  ページ： 1.116-1.130 (J-STAGE)  発行年： 2014年 
JST資料番号： Y0628A  ISSN： 0289-6540  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 制約モデリングは与えられた問題を効率よく解く上で重要な役割を果たすことが知られている.近年,大規模な命題論理の充足可能性判定(SAT)問題を高速に解くことが可能なSATソルバーが実現され,制約充足問題(CSP; Constraint Satisfaction Problem)をSAT問題に符号化して,高速なSATソルバーを用いて求解するアプローチが成功を収めている.本論文では,組合せデザイン分野の一問題であるパッキング配列(PA)問題を例にとり,SATに基づく制約モデリングについて考察する.PAは別名で相互直交的な部分ラテン方陣系とも呼ばれる困難な組合せ問題であり,データベースのディスク最適配置などへの応用が知られている.まず最初に,PA問題を異なる観点から捉えた4つの制約モデル(CSP表現)を提案する.次に,これらの制約モデルを順序符号化法を用いてSAT問題に符号化する方法を示す.なかでも,基本・相違モデルは,与えられたPAのパッキング制約について,その符号化後の節数を小さく抑えられる点が特長である.最後に,組合せデザイン・ハンドブックにあるPA問題を用いて,提案する制約モデルの比較・評価を行った.実験の結果,最適値が未知であった2問について既知の上限が最適値であることを示し,5問について新しい下限を得ることに成功した.(著者抄録)

シソーラス用語： *符号化 ,  *ビンパッキング問題 ,  モデリング ,  *制約充足問題
準シソーラス用語： *SAT符号化 ,  制約モデリング

分類 (2件)： 符号理論  (ND02030R) ,  ネットワーク法  (KA03040X)

タイトルに関連する用語 (4件)： 問題 ,  制約 ,  モデリング ,  SAT符号化