- 著者
-
奥乃 博
湊 真一
- 出版者
- 情報処理学会
- 雑誌
- 情報処理学会論文誌 (ISSN:18827764)
- 巻号頁・発行日
- vol.36, no.8, pp.1789-1799, 1995-08-15
- 被引用文献数
-
2
1
BDD(二分決定グラフ)はブール関数のコンパクトな表現方法である。我々は、BDDを使用して組合せ問題の複数の解を同時に表現したり、ATMSといった多重文脈型真偽維特システムの機能拡張をする方法を検討してきた。与えられた問題記述あるいは制約条件からBDDを構築する過程は制約充足問題の解法とみなすことができる。本稿では、2種類のBDD、算術諭理式が使用できる通常のBDDと組合せ集合が使用できるZBDD(Zero?Suppressed BDD)を取り上げ、それらを用いた割約充足問題の解法を検討する。制約充足問題のデータと制約条件のコーディング方法を提案し、N?Queens問題や魔方陣の問題などの具体的な問題を取り上げ、2種類のBDDによる解法を評価する。さらに、BDDによる解法を、制約充足問題での一貫性アルゴリズムやATMSと比較し、評価を行う。BDDでは、一旦適用された制約条件が以降ずっと成立するという単調一貫性維持が成立する、一方、ZBDDでは、組合せ集合演算の性質から、制約条件が適周する対象によって制限される。しかし、この結果ZDDDでは段階的解法が容易となる。