Solving Constraint Satisfaction Problems 
by Binary Decision Diagram

Hiroshi G. Okuno (NTT Basic Research Laboratories)
Shin-ichi Minato (NTT LSI Laboratries)

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
solving 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.


二分決定グラフによる制約充足問題の解法

奥乃 博 (NTT 基礎研究所), 湊 真一 (NTT LSI研究所)

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