二分決定グラフによる制約充足問題の解法 Solving Constraint Satisfaction Problems by Binary Decision Diagram

この論文にアクセスする

この論文をさがす

著者

抄録

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

BDD (Binary Decision Diagram) is a compact representation of boolean functions. We have applied BDD to represent all solutions of combinatorial problems or to extend capabilities of multiple-context truth maintenance systems such as ATMS. The process of building BDDs from a set of problem specifications or constraints is considered as soliving Constraint Satisfaction Problems (CSPs). In this paper, we focus on two types of BDD ; a normal BDD representing arithmetic logical formula, and ZBDD (Zero-Suppressed BDD) representing sets. We present encoding methods of data and constraints and new operations for ZBDD. We evaluate these methods by solving N-Queens and Magic Square problems. Then, we discuss the relationship of these methods to constraint propagation methods and ATMS. In BDD, the monotonic consistency maintenance that constraints applied so far hold for ever. In ZBDD, when a constraint is applied to a set, its elements unrelated to the set are removed from it. However, this property allows incremental computation in ZBDD.

収録刊行物

  • 情報処理学会論文誌

    情報処理学会論文誌 36(8), 1789-1799, 1995-08-15

    情報処理学会

参考文献:  19件中 1-19件 を表示

被引用文献:  2件中 1-2件 を表示

各種コード

  • NII論文ID(NAID)
    110002722011
  • NII書誌ID(NCID)
    AN00116647
  • 本文言語コード
    JPN
  • 資料種別
    Journal Article
  • ISSN
    1882-7764
  • データ提供元
    CJP書誌  CJP引用  NII-ELS  IR  IPSJ 
ページトップへ