Tarik Hadzic,Rune Moller Jensen,Henrik Reif Andersen计算逻辑和算法组，哥本哈根IT大学，denmarktarik@itu.dk,rmj@itu.dk,hra@itu.dkabstract。在这些注释中，我们正式地描述了从表示有效控制的解空间的BDD计算有效域的功能。形式化主要是基于CLab[1]confireguration框架。1引言交互式confireguration问题是约束满足问题(CSP)的特殊应用，其中用户被协助交互式地为变量赋值bya软件工具。这个软件被称为configurator，通过计算和显示每个未赋值变量的可用有效选择来帮助用户，这些选择被称为有效域计算。应用领域包括定制物理产品（如PC和汽车）和服务（如机票和保险）。实现交互式控制的工具需要三个重要功能：它应该是完整的（所有有效控制都应该通过用户交互来实现）、无回溯（用户永远不会因为逻辑推导的不完整性而被迫改变之前的选择）、以及它应该提供实时性能（反馈应该足够快，以允许实时交互）。在保持完备性的同时又能保证回溯自由的要求使得计算有效域的问题变得NP困难。实时性能要求进一步要求运行时计算在多项式时间内是有界的。根据userinterface设计标准，为了让用户感觉到交互是实时的，systemresponse实际上需要在大约250毫秒内[2]。因此，目前满足这三个条件的方法都使用离线预计算来生成表示解空间的运行时数据结构[3,4,5,6]。这种数据结构的挑战是，解空间几乎总是指数级的大，而且很难找到。尽管有糟糕的最坏情况界限，但在实际工业应用中从未发现数据结构通常可以保持较小[7,5,4]。2交互式约束问题的输入模型是一种特殊的约束满足问题(CSP)[8,9]，其中约束用命题公式表示：definition1。模型C是一个三元(X，D，F)，其中X是一组变量{X，..，xn-1}，D=D×。.。×dn-1是它们的参数D,的笛卡尔积。dn-1和F={F,...,fm-1}是一组超原子命题xi=v,其中v∈Di的命题公式，具体地，每个定义域都可以定义为Di={0,...,di-1}。值v，.的赋值。.，vn-1到变量x，..，xn-1表示为赋值ρ={(x，v)，..，(xn-1，vn-1)}。赋值域dom(ρ)是指被赋值的变量集:dom(ρ)={xi[xi]v∈di.(xi，v)∈ρ}，如果dom(ρ)=x，则将ρ称为总赋值。我们说一个总赋值ρ=F是有效的，如果它包含所有表示为ρ=F的规则。一个部分赋值ρ′，dom(ρ′)X是有效的，如果至少有一个总赋值ρρ′是有效的ρ=F，即如果至少有一种方法可以成功地对现有的con guration过程进行赋值。例1。考虑通过选择颜色（黑色、白色、红色或蓝色）、尺寸（小号、中号或大号）和印花（“黑衣人”-MIB或“拯救鲸鱼”-STW）来指定一件T恤。我们必须遵守两个规则：如果我们选择theMIB印花，那么黑色也必须被选择；如果我们选择小尺寸，那么STW印花（包括鲸鱼的大照片）不能被选择，因为大鲸鱼不适合小衬衫。

Tshirt示例的coon guration问题（X,D,F）由变量X={X,X,X}组成，这些变量表示颜色、大小和打印机。变量域是D={black,white,red,blue},D={small,middle,large}和D={MIB,STW}。这两个规则转换为F={F,F}，其中F=(x=MIB)yen(x=black）和F=(x=STW)yen(x6=small）。有DDD=24个可能的分配。这些赋值中有11个是验证，它们形成了图1所示的解空间。1.（黑色，小型，MIB)（黑色，大型，STW)（红色，大型，STW)（黑色，中型，MIB)（白色，中型，STW)（蓝色，中型，STW)（白色，大型，STW)（蓝色，大型，STW)（黑色，大型，MIB)（红色，中型，STW)图1。T恤Example2.1用户交互的解决方案空间Confiregurator帮助用户交互地达到有效的产品指定，即达到总的有效分配。这种交互作用的关键操作是对每个未赋值变量xi∈X\\dom(ρ)计算有效域dρi di。域是有效的，如果它包含那些且只包含那些能够将ρ扩展为一个总的有效赋值的值，即Dρi={v∈Diàρ′:ρ′=Fóρ{(xi，v)}ρ′}。这种要求的意义在于，只要用户从有效域中选择值，它就保证了对变量的无回溯赋值。这减少了交互过程中的认知工作量，并提高了可用性。在交互的每一步，Confiregurator根据用户先前选择的当前部分赋值ρ，向用户报告有效域。然后用户选择一个未赋值的变量xj∈X\\dom(ρ)，并从计算出的有效域vj∈Dρj中选择一个值。3基于BDD的计算量在[5,10]中通过将计算量分为线上和线上两个阶段来实现交互式计算量。首先，在fluine阶段，作者编制了表示所有有效域Sol={ρρ=F}解空间的aBDD,然后在线提供计算有效域（CV D）的功能，并在与用户交互过程中执行相应的算法。这种方法的优点是BDD只需要编译一次，并且可以重用用于多用户会话。用户交互过程如图1所示。2.inco(Sol,ρ)1:当Solρ>12:计算dρ=CVD(Sol,ρ)3:向用户报告dρ4:用户选择(xi，v)表示某些xi6∈dom(ρ)，v∈dρi5:ρρ{(xi，v)}6:返回ρ，图2。基于解的BDD表示的交互式Counguration算法Sol达到了有效的总Counguration作为参数ρ.在线用户交互的一个重要要求是保证用户与Coungurator交互的实时体验。因此，在联机阶段执行的算法在BDD表示的大小上必须是可证明的。这就是我们所说的实时保证。由于CV D函数是NP-hard的，而在线算法生成的BDD是多项式的，因此不可能为最坏情况下的BDD表示提供多项式大小的保证。然而，它发现BDD的大小对于实践中出现的所有con实例来说都足够小[10]。3.1二叉决策图约简有序二叉决策图(BDD)是一个有根有向无环图，表示一组线性有序布尔变量上的布尔函数。它由一个或两个标记为1或0的终端节点和一组可变节点组成。每个变量节点都与一个布尔变量相关联，并且有两个输出边low和high。变量的Givenan赋值，布尔函数的值由apath从根节点开始，如果关联变量为true，则递归地跟随高边，如果关联变量为false，则跟随低边来确定。

如果到达的终端节点的标签为1，则函数值为true；否则就是假的。该图被排序使得所有路径都尊重变量的排序。BDD被减少使得没有一对不同的节点u和v与该AME变量以及低和高后继器相关联（图3A)，并且没有一个变量节点u具有相同的低和高后继器（图3B)。由于这些减少，nodesuvux的数目x x(a)(b)，图3。(a)与相同变量关联的具有相等的低和高继承权的节点将被转换为单个节点。(b)消除对变量进行冗余测试的节点。高边和低边是用实线和虚线绘制的，实际上许多函数的BDD往往比函数的真值赋值数小得多。另一个优点是简化使BDDs成为规范[11]。通过在单个多根图中表示BDDs的集合，其中BDDs的子图是共享的，可以节省大量的空间。由于规范性，两个BDDs是相同的当且仅当它们具有Sameroot。因此，当使用这种表示时，两个OBDDS之间的等价性检查可以在恒定时间内完成。此外，BDDs易于操纵。在两个BDDs上的AnyBoolean操作可以在与它们的大小成比例的时间内进行。BDD的大小在很大程度上取决于变量的顺序。优化排序本身是一个Co-NP-完全问题[11]，但选择排序的一个很好的启发式是将因变量定位在排序中相互靠近。对于BDDs和分支程序的全面介绍，请阅读Bryant的原始论文[11]和其他书籍[12，13]。3.2编译co-figuration模型每个域变量xi与域Di={0,....,di-1}由ki=logdi布尔变量xi,编码。..,XIKI-1。每个j∈Di，对应于abinary编码V。.VKI-1表示为V。.VKI-1=enc(j)。而且，每一个布尔值的组合V。vki-1表示某个整数j≤2ki-1，表示为asj=dec(v.vki-1)。因此，原子命题xi=v被编码为布尔表达式xi=vó..XIKI-1=VKI-1。此外，还添加了域约束来禁止这些赋值给V。.VKI-1不转化为Di中的值，即dec(v..VKI-1)≥Di。设解空间Sol上的有序变量集x<。<xk-1由二元决策图B(V，E，Xb，R，var)表示，其中V是节点u的集合，E是边E的集合，Xb={0，1，.，XB-1}是可变索引的有序集合，用var(u)≤xb-1标记每个非终端节点u，并用索引Xb标记终端节点T、T。通过取布尔编码变量n-1 i=0{xi,...,xiki-1}的并集，并以自然分层的方式排列它们，即xij<xijiff i<iori=i=iandj<j，构造了一组变量索引xbi。每个有向边e=(u,u）都有一个起始顶点u=π(e)和一个结束顶点u=π(e)。R表示BDD的根节点。BDD表示T恤示例的解空间。2如图所示。4.在T恤示例中，有三个变量:x、xandx，它们的域大小分别为4个、3个和2个。每个变量由布尔变量的向量表示。在定义变量xi的布尔向量中，域为Diis(xi,xi,···xli-1i)，其中li=lg di。例如，在文章中，与T恤尺寸相对应的变量x，用布尔向量(x，x)表示。在BDD中，从根节点到终端节点1的任何路径都对应于一个或多个有效的con。例如，从rootnode到终端node 1的路径（所有变量都取低值）表示validcon饱和度(black、small、MIB)。

另一个具有x、x和xtaking低值和xtaking高值的路径表示两个有效的configuration：（black,medium,MIB）和（black,medium,STW）,namely。在这个路径中，变量xs是一个don\'tcare变量，因此可以同时取低值和高值，这导致两个有效的configuration。从根节点到终端节点0的任何路径都对应于无效的configuration。4计算有效域在展示算法之前，让我们先介绍一下适当的符号。如果索引k∈Xb对应于j+1个Boolean变量xijencomain变量xi,则定义var(k)=i和var(k)=j为适当的映射。现在，给定BDD B(V，E，Xb，R，var),Videnotors所有节点SU∈V的集合，这些节点用一个BDD变量标记，该BDD变量编码域变量xi，即VI={u∈V var(u)=i}。我们想到了在BDD中对一层进行过孔修改。我们可以定义为u∈Vilayer外的边可到达的节点集，即INI={u∈Vi[u\'，u)∈E.var(u\')<i}。对于标记为i=var(R)的根节点R，我们定义为ini=vi={R}。我们假设在以前的用户赋值中，一个用户为一个firenitedomain变量x=v,x∈x赋值，将旧的部分赋值ρold扩展到当前的xxxxxxxxxxx（图4）。T恤示例解空间的BDD。变量xjidenote位vjoft域变量xi的布尔编码。赋值ρ=ρold{(x，v)}。对于每一个变量xi∈X，旧的有效域表示为DρOLDI,i=0,。..,n-1。将原来的BDD BρOldis简化为限制的DBDD,Bρ(V，E，Xb，var)。CV D的功能是通过从新的受限BDD Bρ(V,E,Xb,var)中提取值来计算剩余未赋值变量XI6∈dom(ρ)的有效域Dρi.为了简化下面的讨论，我们将分析在给定BDD B(V，E，Xb,var)上ECV D算法的孤立执行。任务是从起始域di计算validdomains V dii。用户-confiregurator交互可以理解为在受限BDDs Bρ，其中验证域为Dρi，起始域为DρOLDI上的这些执行的序列。CV D功能通过执行图5和图5中给出的两个算法来实现。6.fiefrst算法的关键思想是：如果有一条边e=(u,u)越过Vj，即var(u)<j<var(u)，那么我们可以将Dj3的所有这些边包含到一个有效域V djüdj.我们把e称为长度为V a r(u)-var(u)的长边。注意，它跳过了Svar(u)-va r(u)布尔变量，因此紧凑地表示了大小为2var(u)-var(u)的部分asolution空间。对于剩余的变量xi，其有效域没有被CV d-ski pp复制，我们从图中执行CV D(B，xi)。6.在这里，对于域中的每个值j，我们检查它是否可以是域di的一部分。其关键思想是，如果j∈dithen，则必须有u∈Visuch，它使用jCV d-跳过(B)1的二进制编码从u遍历BDD：对于每一个i=0至n-12:L[i]èi+13:TèT opological Sort(B)4:对于每个k=0到t-15:uèT[k]，ièvar(u)6:对于每个u∈nexprect[u]7:L[i]èmax{L[i]，var(u)}8:S"a{}，Sè09:对于i=0到n-210:如果i+1<L[S]11:L[S]èmax{L[S]，L[i+1]}12:else13:如果S+1<L[S]SèS{S}14:Sèi+115:对于每个j∈S16:对于i=j到L[j]17:V dièdifig.5。在第1-7行中，创建L[i]数组来记录源于Vilayer的最长边e=(u,u)，即L[i]=max{var(u\')[u，u\')[e，var(u)=i}。执行时间由T opologicalSort(B)控制，它可以在O(e+V)=O(e)时间内实现深度搜索。在第8-14行中，重叠的长段已经在O(n)个步骤中合并。最后，在第15-17行中，有效的domainshave在O(n)个步骤中被复制。因此，总的运行时间为O(E+n)，CV D(B，xi)1:V Di{}2:对于每个j=0到di-13:对于每个k=0到ini-14:uèIni[k]5:u′ètraveres(u,j)6:如果u′6=t7:V DiV Di{j}8:return图6。

经典CVD算法。enc(j)表示数字j到kivalues v,的二进制编码。..,VKI-1。如果T从图中反(u，j)。7结束于一个与T不同的结点，那么j∈Vdi.将导致一个T以外的结点，因为这样至少有一条满足路径Tallowing xi=j.T rave rse(u,j)1:ièva r(u)2:V,。..,VKI-1èenc(j)3:sèvar(u)4:如果标记为[u]=j返回T5:标记为[u]èj6:而s≤KI-17:如果var(u)>i返回U8:如果vs=0uèlow(u)10:否则uèhigh(u)12:如果标记为[u]=j返回T13:Mar ked[u]èj14:sèvar(u)图7。对于给定的u∈V,i=var(u),T raverse（u,j）迭代Viand返回遍历结束的节点。当用T raverse（u,j）遍历时，我们将已经遍历的节点标记为j,M arked[ut]àj并防止在将来的j-遍历st raverse（u‘,j）中再次处理它们。即：若T raver se(u,j）通过ut到达Tnode，则任何到达ut的其它遍历T raver(u,j）也必须在T中结束。因此，前值j∈Di,每个节点u∈Vii最多遍历一次，导致最差案例时间复杂度O(Vi·Di)。因此，所有变量的总运行时间为O(PN-1I=0VI·Di)。两个OCV D算法的最坏运行时间为O(PN-1I=0VI·Di+E+n)=O(PN-1I=0VI·Di+n)。Jensen,R.M.：Clab：一个用于快速无回溯交互式产品配置的C++库。http://www.itu.dk/people/rmj/clab/(2007)2。Raskin,J.：人性化的界面。艾迪森·韦斯利（2000）3。Amilhastre,J.,Fargier,H.,Marquis,P.：一致性恢复和非动态CSPS的解释-应用于控制。艺术情报1-2(2002)199-234ftp://fpt.irit.fr/pub/irit/rpdmp/configuration/.4.交互约束满足的方法。哥本哈根大学计算机科学系硕士论文（2003）5。Hadzic,T.,Subbarayan,S.,Jensen,R.M.,Andersen,H.R.,Moller,J.,Hulgaard,H.：使用预编译解空间表示法的Fastbacktrack-free乘积Countration。载于：PETO会议，DTU-tryk(2004)131-1386。Moller,J.,Andersen,H.R.,Hulgaard,H.：互联网上的产品配置。资料来源：第六届信息系统和技术会议记录。（2002）7.Configit软件A/S。http://www.configit-software.com（在线）8。曾义：约束满足的基础。学术出版社（1993）9.Dechter,R.：约束处理。摩根·考夫曼（2003）10。Subbarayan,S.,Jensen,R.M.,Hadzic,T.,Andersen,H.R.,Hulgaard,H.,Moller,J.：比较一个完整且无回溯的交互式控制器的两种实现。在:CP\'04 CSPIA研讨会。（2004）97-11111。布尔函数操作的基于图的算法。IEEE Transactionson Computers 8（1986）677-69112。Meinel,C.,Theobald,T.：VLSI设计中的算法和数据结构。Springer(1998)13。分支程序和二元决策图。工业与应用数学学会(SIAM)(2000)