理论计算机科学电子笔记176（2007）181-197www.elsevier.com/locate/entcs软约束重写逻辑框架Martin Wirsing马丁·威辛1，2慕尼黑路德维希-马克西米利安大学，信息学院，80538慕尼黑Grit Denker，Carolyn Talcott，Andy Poggio，LindaBriesemeister3SRI International，333 Ravenswood Ave，Menlo Park，California 94025摘要软约束扩展了经典约束，使其能够处理非功能性需求、过约束问题和偏好。Bistarelli、Montanari和Rossi发展了一个非常优雅和抽象的基于半环的软约束理论，其中许多不同种类的软约束可以在所谓的约束半环上以统一的方式表示和组合。本文提出了Bistarelli，Montanari和Rossi等人在重写逻辑中提出的一个原型约束类型的框架.作为一个案例研究，我们提出了软约束的应用软件定义的无线电网络的新领域。我们将软件定义无线电的“最佳”参数分配问题建模保留字：重写逻辑，软约束，软件定义的无线电。1介绍软约束是经典约束的扩展，用于处理非功能性需求、过约束问题和偏好。软约束不是仅确定可接受域元素的子集，而是将等级分配给可以从一组有限或无限多的“偏好”值中选择-应用程序域的每个元素。Bistarelli，Montanari和Rossi [4][1]已经开发了一个非常优雅和抽象的基于半环的软约束理论，其中许多1这项工作部分由SENSORIA项目IST-2005-016004赞助。2wirsing@lmu.de3名.姓@ sri.com1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.06.015182M. Wirsing等人理论计算机科学电子笔记176（2007）181不同种类的软约束可以被表示和组合在统一的 这就是所谓的约束半环。本文给出了Bistarelli，Montanari和Rossi等人在重写逻辑[7]中提出的软约束原型的框架工作据我们所知，这是软约束的首次重写实现其他实现基于约束逻辑编程和并发约束编程：clp（FD，S）[13]和softclp（FD）[17]是clp（FD）通过约束半环的扩展。前者基于一种新的抽象机，具有很好的效率;后者是clp（FD）库的扩展， 可以通过这种方式重用来自nyp are ntcl p（FD）求解器的广泛类别的约束传播算法和搜索方法。 [3]的方法使用Frühleth我们的重写逻辑框架由Maude理论和参数化功能模块组成，这些模块可以通过实例化具有特定设置的参数理论轻松集成到任何其他Maude应用程序中。 应用程序.约束半环的公理化理论被建模为Maude泛函理论;特殊的约束半环如加权和和、模糊自然数被建模为泛函Maude模;该框架的所有其他模块（如约束半环的卡积、隐式和显式软约束以及约束求解算法）通过约束域和半环的选择而被参数化。为了提高约束求解的效率，所有递归规范都以尾递归形式表示，并且各个约束的域元素根据它们在约束半环中的等级进行排序。我们还证明了我们的搜索算法的正确性作为一个案例研究，我们提出了软约束的应用软件定义的无线电网络的新领域（见例如http://www.sdrforum.org）。软件定义的无线电是一种无线电，其中大多数或所有频率控制，调制/解调格式，带宽和其他参数由软件实现，因此可以在无线电操作期间改变。 这为商业和业余无线电提供了巨大的新灵活性，但在不同环境中控制这些无线电需要对其参数设置进行微妙的微调和调整。我们使用约束半环的卡累利阿积将软件定义的无线电的“最优”参数分配问题建模为软约束求解问题，在我们的软约束原型重写逻辑框架中实现解决方案，并将我们的软约束求解器嵌入SRI的策略感知，面向目标的分布式体系结构（PAGODA）中用于无线电网络建模。请注意，尽管其他实现（如[3]和[9]）也可以处理半环的Carnival积，但其他已发表的案例研究都没有利用此功能。测试运行表明，软件定义无线电的最佳参数分配可以在几秒钟内计算出来;只有最困难的约束集需要一分钟以上的时间来构建解决方案。M. Wirsing等人理论计算机科学电子笔记176（2007）181183监测HA雷索基地HDC船首ner被隔离的协调员协调员知识五金制品提取层2示例应用作为在Maude开发约束解决机制的驱动应用程序，我们专注于通信无线设备或无线电，优化资源使用，如带宽和功率相对于给定的目标。 此应用程序设置在基于策略和目标的应用程序的更广泛背景中，其中设备协作努力实现目标，同时满足约束可能解决方案的策略。PAGODA（参见http://pagoda.csl.sri.com）是一种用于设计（部分）自治系统的模块化架构。PAGODA节点通过感知和执行与其设备交互，由要实现的目标驱动并受策略约束。一个PAGODA系统是一个PAGODA节点的集合，这些节点通过合作来实现共同的目标。PAGODA体系结构的灵感来自于对自主空间系统体系结构的研究，特别是MDS体系结构[12]及其前身[15]。Fig. 1. PAGODA节点架构图1显示了PAGODA节点的主要组件：知识库、协调器、推理器、监视器和硬件抽象层。 还有一个与系统操作员（总部）通信的组件，负责与其他PAGODA节点进行分布式协调的组件（分布式协调器）。知识库包含由其余组件共享和更新的知识。这些知识涵盖了广泛的信息，包括(1)节点或系统试图实现的目标，（2）限制节点或系统允许执行的操作或交互的策略，从而减少设置参数的选择数量，以及（3）指定可以设置（旋钮）和读取（传感器）的参数及其关系的设备模型。旋钮设置的效果可以在改善的连接性、更高的带宽和与目标相关的其他可观察结果方面观察到。例如，增加发射功率或选择较低频率会导致无线电之间的连接性更好。这些关系在表中定义，如图2（左）所示。 请注意，某些旋钮设置，如 高频率的传输，可能有矛盾的效果（减少连接，184M. Wirsing等人理论计算机科学电子笔记176（2007）181图二、部分旋钮传感器（左）和部分旋钮传感器（右）工作台但带宽更高）。同样，旋钮设置和可测量的传感器读数之间的依赖关系也被定义。图2（右）显示了定义选择特定旋钮设置对传感器读数的影响的摘录。根据定义，如果列中的权重之和大于50（即 case in the full table），则旋钮设置的组合意味着列中的相应传感器读取“良好”。因此，高发射功率和低发射频率也促进了信号强度读数的增加 作为连接性损失的良好传感器读数，而高传输功率和高传输频率促进吞吐量的更好读数推理器组件确定适当的旋钮设置，以便实现目标或发生期望的效果。推理机使用知识库中的信息作为推理的基础：设备模型，即旋钮、事件和传感器读数之间的关系;目标;策略;以及当前状态。当确定新的参数设置时，推理器还提供诸如使用什么传感器值和/或来自设备模型的什么关系来推断新设置的判断。如果事情没有按预期进行，这可以用于诊断。 推理机还指定了应该被监控的传感器和不满足目标的传感器读数的条件，以便推理机可以采取纠正措施。我们用Maude语言[7]开发了PAGODA架构的正式可执行规范，并使用无线电的抽象设备模型实例化它以测试这些想法。目标被视为对传感器读数子集的软约束。矢量（旋钮）和传感器读数之间以及传感器读数和目标之间的关系被形式化为约束半环，这为求解软约束提供了清晰的数学基础[4，10]。特别是，传感器表（见图2右侧）为旋钮设置分配权重。这些权重的总和表明特定旋钮设置对给定传感器的好处：其权重总和越高越好。我们的目标是计算一系列感兴趣的传感器的估值旋钮，优化这些权重的总和。 我们的模型，这是由模糊自然数的约束半环分级的权重。效应约束指示特定旋钮设置对给定效应的影响。 fect（参见图2左侧）。目标是找到满足最大所需效应或等效地违反最小所需效应的旋钮设置。最好的情况发生在没有违反效果的情况下[2]。我们使用加权和的约束半环模型M. Wirsing等人理论计算机科学电子笔记176（2007）181185∗∗∗≤≤⟨ ∗ ⟩∈⟨ ∗⟩我们使用规范实例化了PAGODA 抽象设备规范，一个具体的无线电，MadRad，模拟实际的无线电硬件/软件，包括随机的，不寻常的和错误的行为。测试场景允许我们探索一些可能的系统行为。3Maude中的C-半环与软约束3.1Maude简介Maude [7]是一种基于重写逻辑的多范式可执行规范语言[14]。Maude的源代码、几个平台的可执行文件、手册、入门、案例研究和论文都可以从Maude的网站http：//maude上获得。 cs.uiuc.edu。我们使用功能理论，功能模块和参数化模块在我们的框架。函数模是用于指定代数数据类型的等式理论，例如特定的约束半环;它们用语法fmod. 结束调频函数模块可以有排序、子排序关系、运算符、变量、成员公理和等式，并且可以导入其他的-ories或模块。 功能理论（Syntax Theories） 端点）类似于功能模块，它们用于声明模块接口，例如约束半环的公理理论;但是与功能模块相反，它们具有松散的解释（与功能模块的初始代数语义相反）并且不需要是可执行的（由属性nonexec表示）。参数化模块（可在Maude 2.2）用于表示我们的通用方法软约束。这样的模块P具有语法fmod P{X1：：T1，.，Xn：：Tn}...其中Xi是形式参数，Ti是表示参数类型的泛函理论（i = 1，.， n）。 视图V（从T到M的写入视图 V是… endv）规定了如何要求一个特定的目标模M满足源理论T。 实例P（V1，...，Vn）需要从每个形式参数Xi的类型Ti到对应的实际参数Mi的视图Vi，使得每个Mi满足Ti模由Vi指定的重命名的公理（即每个Vi是理论态射）。3.2约束半环一个半环S是一个代数G; +; ; 0; 1，其载体集G，两个常数0， 1G和两个二元运算+，具有下列性质：+是交换结合的，0是它的中性元;+，1是其中性元素，0是其吸收元素。一个约束半环S（简称c-半环）是一个半环G;+; ; 0; 1，它具有以下两个附加性质： 是交换的，1是+的吸收元。 然后-正如一个匿名的裁判所观察到的 加法导致G的元素之间的偏序关系，定义为a bia+b=b。这种偏序将用于比较约束的解决方案，并确定最佳解决方案。 如果a≤b，我们也说b比a好。 +和n是单调的w.r.t.≤，0是最小元素，1是最大元素186M. Wirsing等人理论计算机科学电子笔记176（2007）181G;<$G;≤ <$G构成一个完备格，其上界至少为+约束半环具有重要的闭包性质：它们在幂集的形成和卡里积下是闭的。一个ic-半环是一个约束半环，其中k也是幂等的。则+分布在G和G上;≤ G是一个完全分配格，以G为它的最大下界。我们形式化半环，约束半环，和ic半环的莫德理论在一个直截了当的方式。排序被称为分级，因为它的元素将用于分级软约束。 注意，最后一个公理导出了传递性和对称性的等价关系。Prosemiring是PRBOOL。排序等级。操作零：->等级。行动一 ：->等级。op_+_：Grade Grade -> Grade [aslogid：zero prec 33].op_*_：Grade Grade-> Grade [aslogid：one prec 31].op_<=_：Grade Grade -> Bool [prec 37].op _equiv_：Grade Grade -> Bool [prec 37].变量X Y Z：等级。等式X *（Y + Z）=（X * Y）+（X * Z）[nonexec].等式X * 零=零[nonexec]。等式X<=Y为（X+Y）==Y[nonexec]。eq X equiv X = true[nonexec]。ceqX equivZ = trueif XequivY =true/\ZequivY =true [nonexec]. 末端SEMIRING是一种半成品。变量X：等级。等式X + one = one[nonexec]。末端两个c-半环的乘积形成一个c-半环，其运算以明显的分量方式定义。导出序关系=×是一个偏序。我们还介绍了字典排序=与首选组件的应用程序。字典序是一种扩展为=×的全序;它也非常适合无线电应用，其中最佳效应优于最小传感器值的优化 注意，与<= ×相反，乘法一般不是单调的。词典-图形排序<=但对于无线电应用表现良好[18]。该方法以两个约束半环为参数，将产品建模为参数化模块。fmod对{X：： C-SEMIRING，Y：： C-SEMIRING}是保护BOOL对{X，Y}进行排序。操作对：X$Grade Y$Grade -> Pair{X，Y}[ctor]。op zero：-> Pair{X，Y}. eq zero = pair（X$zero，Y$zero）. 操作一：->对{X，Y}。等式1 = pair（X$one，Y$one）。var A A1 A2：X$等级。var B B1 B2：Y$等级。op _+_：Pair{X，Y} Pair{X，Y}-> Pair{X，Y}[prec 33].等式对（A1，B1）+对（A2，B2）=对（A1 + A2，B1 +B2）。op _*_：Pair{X，Y} Pair{X，Y}-> Pair{X，Y}[prec31].op_<=*_：Pair{X，Y} Pair{X，Y}-> Bool [prec37].op_<=_：Pair{X，Y} Pair{X，Y}-> Bool [prec 37].op _equiv_：Pair{X，Y} Pair{X，Y}-> Bool [prec 37].opfst：Pair{X，Y}-> X$Grade.op snd：Pair{X，Y}-> Y$Grade.M. Wirsing等人理论计算机科学电子笔记176（2007）181187∞∞⟨ ∪ {∞} ∞ ⟩∞⟨ ∪ {∞}∞⟩{}. . .endfm3.3布尔、模糊与加权和半环约束半环的示例是布尔代数，并且具体地，布尔=假;真;假;真，除加权和外，所有这些代数都是ic-半环。在布尔代数中，真比假好;对于模糊自然数，0是最小和最大元素，而加权和的排序与通常的排序相反：是最小元素，0最大的元素在Maude中，模糊自然数以如下方式被指定为函数模。我们引入了无穷模糊自然数的NatFN和两个表示元素和“非无穷”自然数的子类IftyFN和NiNatFNFMOD FUZZYNAT是pr NAT。排序NiNatFN IftyFN NatFN。子分类NiNatFN IftyFN NiNatFN[ctor]. op iftyFN：-> IftyFN[ctor].OP _+_：NiNatFN NiNatFN-> NiNatFN [prec 33].op _+_：NatFN NatFN-> NatFN [prec 33].等式fn（M）+fn（N）= fn（max（M，N ） ） 。 等 式 fn （ M ）+iftyFN = iftyFN 。 等 式iftyFN + U = iftyFN。op_<=_：NatFN NatFN-> Bool.op _equiv_：NatFN NatFN -> Bool.操作零：->NiNatFN。等式零=fn（0）。操作一：->IftyFN。等式1 =iftyFN。varsNM：Nat. varU：NatFN.op _*_：NiNatFN NatFN-> NiNatFN [prec 31].OP _*_：NatFN NatFN-> NatFN [prec 31].等式fn（M）* fn（N）=fn（min（M，N））。等式fn（N）*iftyFN = fn（N）。等式fn *fn（N）= fn（N）。等式iftyFN * iftyFN = iftyFN。. . .endfm然后，我们定义了一个从C-半环到FUZZYNAT的观点，并且可以很容易地通过结构归纳证明所有公理都是满足的，即，该视图形成理论态射。查看FuzzyNat从C-SEMIRING到FUZZYNAT是排序等级到NatFN。恩代夫用类似的方法，给出了无穷自然数上的加权和WSUM的约束半环以及从C-SEMIRING到加权和代数的理论态射WSUM在我们的软件定义无线电应用中，我们使用的Carnival产品为自然数上的约束半环。它通过使用视图WSum和FuzzyNat实例化参数化模块PAIR来定义。卡氏积也形成一个c-半环，它由视图WSumFuzzyPair表示。FMOD WSUMMUZZYPAIR是pr PAIR{WSum，FuzzyNat}。endfm188M. Wirsing等人理论计算机科学电子笔记176（2007）181∈∈−→−→›→›→−→−→›→›→ ∈−→›→›→⟨ ⟩ ∈ −→−→查看从C-SEMIRING到WSUMMUZZYPAIR的WSumFuzzyPair是对{WSum，FuzzyNat}排 序 的 等 级 。恩代夫3.4软约束软约束为一组问题变量的不同估值分配等级。设S是一个具有载体集G的约束半环，D是一个有限问题域，V是所有问题变量的集合. A.估值： V arD是一个从V ar到D的局部映射，它有一个有限支集。给定变量的有序列表al V ar，软约束将G中的等级分配给al中变量的每个可能赋值;更正式地，软约束是一对al;cst，其中cst（V ar D）G是从赋值到G的元素的映射，使得cst的域的每个赋值都有有限支持度al。由于所有这些赋值的集合是有限的，因此任何软约束都有一个有限的定义域，因此可以用一个有限的对集合（pairs）来显式表示（二）与（联D）和G或通过特定的构造函数或函数声明以更隐式的方式 就像编程语言一样。在我们的框架中，我们支持这两种可能性;在这里，我们只提出了显式形式和一个特定的隐式形式，我们需要我们在软件定义无线电中的应用为了表示Maude中的赋值，我们在所有变量的集合V ar上定义一个全序。模块VALUATION由变量的有序集X和有序域D的理论参数化（使用Maude序言中提供的理论TAO-SET）;每个赋值=（a1 d1，…，一个kd k）由a表示对，对d1]由有序列表a1=a1，...，a k个变量和列表d1=d1，…，d k的相应元素的集合。 对于固定的al，D）G 同构于Dk因此，任何约束定义cst都可以表示为从Dk到G在Maude中，我们用类似于Maude序言的MAP模块的参数化模块LC-MAP来指定这样的映射，除了范围是约束半环S，并且出于效率的原因，任何映射的域由D的元素列表组成。和MAP一样，我们为映射引入了一个参数化排序LC-Map，并为形式为（dl g）的简单条目引入了一个子排序;出于空间效率的原因，我们从LC-Map项中省略了条目（dl0）。此外，该规范包含了根据定义域的不同字典序的值和根据上定义域的值对映射进行排序的有效操作。 分类列表1 是SORTABLE-LIST（参见Maude 2.2 prelude）的扩展，通过noDupmerge操作合并两个有序列表而不重复元素。fmod VALUATION{X：： TAO-SET，D：： TAO-SET}是prEXT-BOOL。 pr SORTABLE-LIST1{X}. pr SORTABLE-LIST1{D}.排序赋值{X，D}。操作[_|-> _]：List{X} List{D} -> Valuation{X，D}[ctor].操作变量：估值{X，D}->列表{X}。操作值：Valuation{X，D}-> List{D}。操作一致：估值{X，D}估值{X，D}->布尔值。* 检查公共变量的值是否相等* 两个评价。op mergeEntry：Valuation{X，D} Valuation{X，D} -> List{D}.* 合并了两个一致估值的值...endfmfmod LC-MAP{D：： TAO-SET，S：： C-SEMIRING}是M. Wirsing等人理论计算机科学电子笔记176（2007）181189Σ∈›→|∗∗|›→›→⊆|保护可排序列表{D}。排序LC-Entry{D，S}LC映射{D，S}。子排序LC-Entry{D，S}< LC-Map{D，S}。op empty：-> LC-Map{D，S}[ctor].操作符（_|->_）：列表{D} S$等级-> LC-条目{D，S}[ctor]。op：LC-Map{D，S} LC-Map{D，S} -> LC-Map{D，S}[ctor ascurid：空]。...op sortCoDomain：LC-Map{X，Y} -> LC-Map{X，Y}。. . .endfm具体化约束由理论X（变量）、D（问题域）和S（c-半环）参数化。它具有约束和约 束 列 表 的 参 数 化 排 序 ， 以 及 显 式 和 隐 式 约 束 的 子 排 序 EConstraint 和IConstraint，以及具有常数等级0的约束的排序ZeroConstraint和完全没有约束的情况的排序NoConstraint软约束的显式表示形式为[al|（val1<$−→ g1），.， （val m−→ g m）]其中所有等级g1，.，g m与0不同（如在LC-MAP中）。c-半环的运算和LC-MAP的运算被提升到如下的约束。将约束c=[al cst]应用于赋值函数定义为map applica- tion：c[max] =cst[max];zeroConstraint和noConstraint定义具有常数值0和1的约束;约束乘法定义为满足方程c1c2[max] =c1[max]c2[max]，约束加法定义为类似的。然后很容易证明约束集再次形成c-半环[5]。此外，我们定义了投影算子投影和（对于约束传播）部分求值算子peval。对于任何约束c=[al cst]和任何赋值n =[bldl]，其中blal，peval（c，n）将c限制为与n一致的赋值;特别地，对于bl=al，我们有peval（c，n）=[al（dlcst[n]）]。对于约束c和变量xl的有序列表，project（c，al）计算和dl Dkpeval（c，[al dl]）的所有可能的al的部分求值。为了提高效率，所有对约束的操作都以尾递归的方式指定。作为一个例子，我们展示了约束乘法的具体化fmod CONSTRAINT{X：： TAO-SET，D：： TAO-SET，S：： C-SEMIRING}是保护EXT-BOOL。保护NAT。保护SORTABLE-LIST 1 {X}。保护VALUATION{X，D}。保护LC-MAP{D，S}。排序NoConstraint{X，D，S}ZeroConstraint{X，D，S}SimpleConstraint{X，D，S} EConstraint{X，D，S}Constraint{X，D，S}ListConstraint{X，D，S}。subsort NoConstraint{X，D，S} ZeroConstraint{X，D，S} NoConstraint{X，D，S}[ctor].操作zeroConstraint：-> ZeroConstraint{X，D，S}[ctor].操 作 [_|_] ： List{X} LC-Entry {D ， S} -> SimpleConstraint{X ， D ，S}[ctor].操作[_|_]：列表{X} LC映射{D，S}-> EConstraint{X，D，S}[ctor]。op _+_：约束{X，D，S}约束{X，D，S} ->约束{X，D，S}。op_*_： 约 束 {X ， D ， S} 约 束 {X ， D ， S} -> 约 束 {X ， D ， S} 。op_[_]：约束{X，D，S}估价{X，D}-> S$等级。op peval：EConstraint{X，D，S} Valuation{X，D}-> EConstraint{X，D，S}. OP项目：EConstraint{X，D，S}列表{X}-> EConstraint{X，D，S}。...190M. Wirsing等人理论计算机科学电子笔记176（2007）181∈⟨ ⟩ ⟨⟩×{}变量AL BL：列表{X}。 变量VL WL L：列表{D}。变量EN 1 EN 2：LC-条目{D，S}。变量M M1 M2结果：LC图{D，S}。变量P Q：S$等级。varC：约束{X，D，S}。eqnoConstraint*C=C。 eq[AL|M]*noConstraint=[AL|M]。eqzeroConstraint * C = zeroConstraint。eq [AL |M]* zeroConstraint = zeroConstraint。eq [AL|空] * [BL |M] = [noDupMerge（AL，BL）|空的]。eq[AL|（VL|-> P）M1]*[BL |M2]=如果P =/=零then [noDupMerge（AL，BL）]|[AL|（VL|-> P）M1] * 地图[BL |M2]] else [noDupMerge（AL，BL）|[AL |M1] * 地图[BL |M2]] fi.op _*Map_：SimpleConstraint{X，D，S}SimpleConstraint{X，D，S} -> LC-Map{D，S}。eq [AL|（VL|-> P）] * 地图[BL|（WL|-> Q）]=如果（P *Q=/=零），则一致（[AL|->VL]、[BL|->WL]），然后（mergeEntry（[AL|->VL]、[BL|->WL]）|->P*Q）空的fi。op _*Map_：EConstraint{X，D，S} EConstraint{X，D，S} -> LC-Map{D，S}。OP_$*Map_with_is_：EConstraint{X，D，S}EConstraint{X，D，S}LC-Map{D，S} LC-Map{D，S} -> LC-Map{D，S}。eq [AL| M1] * 地图[BL| M2]=[AL |M1] $* 地图[BL |M2是空的。eq [AL| EN1 M1] $* 地图[BL| EN2 M2]，其中M是结果= [AL| EN1 M1] $* 地图[BL| M2]与Mis（结果（[AL| EN1]* 地图[BL| EN2]）。eq [AL| EN1 M1] $* 地图[BL|空]，其中M是结果= [AL |M1]$* 地图[BL |M是结果。eq[AL|$*Map [BL]|M2]，其中M是结果=结果。...endfm3.5硬约束和隐式约束硬 约 束 可 以 被 认 为 是 一 类 特 殊 的 软 约 束 ： 那 些 在 二 值 布 尔 半 环 上 的 约 束Bool=false;true;false;true其中true表示满足硬约束，false表示违反[4]。 硬约束和软约束常常同时出现在同一个问题中。设S是软约束的c-半环.然后有几种编码硬约束的可能性：• 选择S作为c-半环，用1S表示硬约束的满足，用0S表示它的违反。这为满足所有硬约束的软约束和硬约束的一致组合产生非零等级;如果违反了其中一个硬约束，则所得权重为0S。• 用字典序法构造Carnival产品BoolS。然后，硬约束的饱和度由1Bool，g表示，违反由0Bool，g表示对于一些gS。这为我们提供了对硬约束违反的更细粒度的分析：人们不仅可以区分满足所有硬约束的约束组合的等级，还可以区分违反其中一个硬约束的软约束的等级。M. Wirsing等人理论计算机科学电子笔记176（2007）181191≥⟨ ⟩ ⟨⟩|›→›→∗∗Σ≤ ||∗∗对于我们的无线电应用，我们选择了后一种解决方案的一个改进：c-半环是加权和和模糊自然数的字典序Carnival积WSUMFUZZYPAIR（见3.3节）。对于传感器约束，出现形式为n常数的硬约束，其具有“模糊自然数约束”的c-半环中的值。我们表示满足这样的硬约束1WSum，n和违反0WSum，n，从而也给出了有关传感器约束的等级的信息。一般来说，隐式约束由结构递归表达式和特定的应用程序相关构造函数定义。作为操作，我们提供部分求值和转换为显式约束。对于无线电应用，我们使用传感器表作为传感器约束的空间效率表示。 传感器值的简单表示 通过求和导致具有许多变量的约束并因此导致潜在指数数量的条目;例如，对于“信号强度”的显式约束[TP TF Cp.（嗨...50）（Lo Hi Hi.0）. ]相反，我们使用一个隐式约束（使用构造函数sm表示sm（[TP|（Hi → 50）（Lo → 0）] [TF|（Hi → 0）（Lo → 50）]. ）在约束求解过程中，我们总是尽可能地采用部分求值的方法，以减小隐式约束的规模，然后再将其转化为显式约束。4解决软约束软约束列表cl=cl1. CL n由乘法CL1. cl n;结果再次是软约束c，其可以表示为和sc1+.+sc m的简单约束（其中mD|变量（cl）|）. 每个这样的简单约束称为C的可能解。并非所有这些可能的解决方案都是应用程序感兴趣的。 在以下 我们把cl写成cl 1的简写。求cl n和cl的cl1+. +cln在许多情况下，我们搜索所有最佳解的集合maxSol（cl），即，D的所有元素|变量（C）|在解空间中具有最大等级，或者对于具有优于特定阈值的等级的解。也可以更一般地计算投影项目（cl1. cl n，xl）到变量的子集xl，如果只有这些变量是感兴趣的，然后考虑相同类别的解。对于无线电应用，我们需要算法来满足这两个要求：在短时间内找到一个容许解，以及在有足够的计算能力和时间的情况下，找到所有最佳解或所有容许解。但是我们可以简化这项工作，因为所有的变量（旋钮）都是感兴趣的，并且所涉及的半环都是全序的。下面，我们因此这些简化的假设，并提出了一个Maude实现搜索所有最佳的解决方案，并给出了其他搜索算法的实施草图192M. Wirsing等人理论计算机科学电子笔记176（2007）181∗∗||∗∗|›→∗|›→∗|›−→−→|›→|›→该实现由以下三个参数化模块组成：一个模块SOLVECONSTRAINT的两个搜索算法和两个模块的解决方案和CONTINUATION表示的数据类型的解决方案和存储必要的回溯信息。模块SOLUTION提供了关于所有解、它们的等级和它们的数量的明确信息;特别地，solution（scl，g，n）是由表示解的简单约束的列表scl、scl的所有元素的等级g和解的数量n=scl组成的构造器项。 连续由模块CONTINUATION定义;连续ct（cl0，sc）由部分解sc和未解约束的列表cl0组成，其预期性质是sc的组合sc cl0与cl0中的所有约束再次形成原始约束问题cl的一组可能解。模块SOLVECONSTRAINT定义了深度优先搜索算法，用于找到所有最佳解，用于找到优于某个阈值的第一个解，以及用于找到所有此类解（类似方法见[3]）。对于任何列表cl，search（cl）计算所有最佳解的集合maxSol（cl）。为了提高效率，假设所有约束[al（val1g1），. （val m）g m）]，在cl中，所有等级g1，.，g m是降序的。搜索使用辅助尾递归操作$search（cl，sc，n，csol）其中cl表示要求解的约束列表，sc是实际的部分解，n是延拓，csol=solution（scl，b，n）是到目前为止获得的约束解。的 最 有趣情况的的递归定义是CL=[al（vl p）erest]rest和sc=[bl（wl q）]其中vl具有等级p，erest表示由cl的第一约束的剩余赋值组成的映射，并且rest表示约束cl的列表的尾部。（所有其他情况都更简单，erest、rest或cl为空，或sc对应于noConstraint。如果P级新解的q不小于b，且与 如果cl的第一个子约束c0=[al（vl p）]与sc一致，则$search计算新的部分解[al（vl（p）]并将约束的其余部分保存在延续中以供稍后回溯。 否则，如果p q足够大，但c0与sc不一致，则继续搜索erest;最后，如果p q b，我们可以使用每个约束都按等级降序排序的事实，这意味着对于erest条目的所有等级g，我们也有<因此，部分解SC不能被完成为最佳解，并且算法利用延拓进行回溯fmod SOLVECONSTRAINT{X：：TAO-SET，D：：TAO-SET，S：：C-SEMIRING}是pr CONSTRAINT{X，D，S}。pr CONTINUATION{X，D，S}.pr解决方案{X，D，S}。var N：Nat. 变量AL BL：列表{X}。变量VL WL：列表{D}。varERest：LC-Map{D，S}. 变量P Q B：S$等级。var SC：SimpleConstraint{X，D，S}.var EC：EConstraint{X，D，S}。var C：约束{X，D，S}。变量L Rest：ListConstraint{X，D，S}。var Cont：ListContinuation{X，D，S}. var结果：解决方案{X，D，S}。操作搜索：ListConstraint{X，D，S} -> Solution{X，D，S}。eq search（L）= $search（sortElements（L），noConstraint，nil，solution（nil，zero，0））。M. Wirsing等人理论计算机科学电子笔记176（2007）181193j=1Σj=1op $search：ListConstraint{X，D，S} Constraint{X，D，S}ListContinuation{X，D，S} Solution{X，D，S}-> Solution{X，D，S}。...eq $search（[AL|（VL|-> P）ERest] Rest，[BL|（WL|-> Q）]，续，溶液（L，B，N））=如果（B=P*Q）和（zeroP*Q），则如果一致（[AL|-> VL]、[BL|-> WL]），则$search（Rest，[AL|（VL|-> P）]* [BL|（WL|->Q）]，ct（[AL |ERest]静止，[BL|（WL|->Q）]）续，溶液（L，B，N））else $search（[AL |ERest]静止，[BL|（WL|-> Q）]，续，溶液（L，B，N））Fielse $backtrack（Cont，solution（L，B，N））fi.eq$search（C，SC，Cont，Result）=$backtrack（Cont，Result）[owise].op $backtrack：继续{X，D，S}解决方案{X，D，S} ->解决方案{X，D，S}。eq$backtrack（nil，Result）=结果。eq$backtrack（ct（L，C）Cont，Result）=$search（L，C，Cont，Result）....endfm很容易看出搜索算法正在终止。 以下引理是搜索算法正确性证明的基础引理4.1（搜索不变）对于所有列表cl = cl1. CL m的显式约束（其中每个CL i以等级 的 降 序 排 序 ） ， 对 于 所 有 部 分 约 束 SC ， 所 有 形 式 CT （ contl1 ，scontl1），. . .，CT（contlk，ssclk），以及形式为solution（scl，b，n）的所有解Csol，其中scl是具有等级b
我的内容管理
展开
