约束满足问题求解的符号OBDD桶消元算法  

OBDD-based Bucket Elimination Algorithm for Constraint Satisfaction Problem

作　　者：徐周波[1,2] 古天龙[2] 常亮[2] 李凤英[1,2] 

机构地区：[1]西安电子科技大学电子工程学院,西安710071 [2]桂林电子科技大学计算机科学与工程学院,桂林541004

出　　处：《计算机科学》2011年第7期200-202,219,共4页Computer Science

基　　金：国家自然科学基金(60963010;60903079;61063002);广西自然科学基金重点项目(0832006Z)资助

摘　　要：桶消元算法是求解约束满足问题的一种典型推理方法。针对桶消元算法面临的状态空间爆炸问题,将有序二叉决策图(OBDD)技术与该算法结合起来,给出了约束满足问题的一种求解算法。通过对约束满足问题中变量和域值的编码,将CSP问题转化为命题可满足性问题,给出了约束满足问题的OBDD表示方法;基于桶消元的算法思想,在约束满足问题的OBDD表示的基础上,利用OBDD的"与"操作和"量化"操作等,避免了传统算法中状态的显式枚举,隐式地实现了对CSP的求解。对大量随机生成的测试用例进行了实验分析,结果表明提出的符号算法明显优于桶消元法和符号直接求解法。Bucket-elimination algorithm is a typical reasoning method for the constraint satisfaction problem（CSP）.Aiming at the state explosion problem of bucket-elimination algorithm,ordered binary decision diagram（OBDD） technique was combined with bucket-elimination algorithm,and a symbolic OBDD-based algorithm for CSP was proposed.By encoding each variable and each value in the domain as binary variables,CSP was encoded as a propositional satisfiability（SAT） problem,and then CSP was formulated symbolically by OBDD.Based on the ideas of bucket-elimination algorithm and the symbolic OBDD representation of CSP,the CSP was solved implicitly by the AND operator and the EXIST operator of OBDD,so that the explicit enumeration of states in traditional algorithms was avoided.The simulation results show that the symbolic algorithm is more efficient than both the bucket-elimination algorithm and the direct algorithm based on OBDD.

关 键 词：约束满足问题 符号算法 桶消元 有序二叉决策图(OBDD) 

分 类 号：TP301.6[自动化与计算机技术—计算机系统结构]