文献

J-GLOBAL ID：201402250699583446   整理番号：14A0135214

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

著者 (5件)： 則武治樹 (神戸大 大学院システム情報学研究科) ,  番原睦則 (神戸大 情報基盤セ) ,  宋剛秀 (神戸大 情報基盤セ) ,  田村直之 (神戸大 情報基盤セ) ,  井上克巳 (国立情報学研)
資料名： 日本ソフトウェア科学会大会講演論文集(CD-ROM)  (日本ソフトウエア科学会大会講演論文集(CD-ROM))
巻： 30th  ページ： 79-92  発行年： 2013年 
JST資料番号： X0080B  ISSN： 1348-0901  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

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

シソーラス用語： *充足可能性問題 ,  *パッキング問題 ,  命題論理 ,  モデリング ,  制約条件 ,  データベース ,  最適化問題 ,  配置問題 ,  符号化 ,  評価試験 ,  配列 ,  数学的性質 ,  ベンチマーク
準シソーラス用語： ラテン方陣 ,  制約モデリング

分類 (2件)： 論理代数  (JB03000H) ,  その他のオペレーションズリサーチの手法  (KA03070E)

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