约束函数逻辑程序设计协作求解器的建议

理论计算机科学电子笔记188（2007）37-51www.elsevier.com/locate/entcs约束函数逻辑程序设计S. 这是一个1A的地方。J. Fern′andezb，2T. 霍尔塔尔-贡扎勒扎，1 米。Rodr'ıguez-Artalejoa，1F. S'aenz-P'ereza，1R. delVado-V'ırsedaa，1aDepartamenodeSistemasInform'ticosyProgramacio'nUniversidad Complutense deMadrid西班牙马德里bDepartametodeLenguajesyCienciasdelaComputacio′nUniversidadeMa′laaM'alaga，Spain摘要本文提出了一种约束函数逻辑程序设计中求解器协作的建议。约束函数逻辑程序设计是一种将函数、逻辑和约束程序设计结合起来的具有很强表达力的程序设计范式，它使用约束惰性窄化作为目标求解机制。 不同约束域的求解器的合作可以提高实现的效率，因为求解器可以利用其他求解器的推理。 我们限制我们的注意力的三个求解器的合作，处理语法平等和不等式约束，真正的算术约束，有限域（FD）的约束，分别。作为合作机制，我们考虑传播到真正的求解器的约束已提交给FD求解器（反之亦然），施加特殊的通信约束，以确保两个求解器将允许相同的整数值的所有变量参与合作。关键词：协作求解器，约束，函数逻辑编程，惰性缩小，实现。1介绍在过去的几年里，约束编程（简称CP）的不同求解器的合作已经得到了广泛的研究[4]，旨在解决单个求解器无法处理的混合问题，并提高效率。另一方面，函数式和逻辑式编程风格（分别为FP和LP）支持简洁的声明性语义，1名作者，由项目TIN 2005 -09207-C 03 -03和S-0505/TIC 04072作者由项目TIN 2004 -7943-C 04 -01和TIN 2005 -08818-C 04 -01部分资助1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.05.03738S. Estévez-Martín等人/理论计算机科学电子笔记188（2007）37项目建设设施。用于约束逻辑编程的CLP方案由Ja Zarar和Lassez的开创性论文开始，提供了CP和LP的组合，这已被证明对于CP应用非常实用[7]。 添加 FP维CLP导致了各种建议的CFLP计划约束功能逻辑编程，自1991年以来开发，旨在一个非常有表现力的组合CP，高阶懒惰FP和LP。CLP和CFLP都是可以通过不同的约束域和求解器来实例化的方案。本文提出了CFLP中求解器协作的一个建议，更确切地说，是以文[9，2，8]中提出的CFLP方案为例，用TOY语言和系统[1]实现。支持协作的求解器是：支持语法等式和不等式约束的Herbrand域H的求解器;支持整数集合Z上的有限域约束的域FD的求解器;以及支持实数集合R上的算术约束的域R的求解器。之所以选择这种特定的组合，是因为H约束对于处理结构化数据的有用性以及混合FD和R约束在许多实际CP应用中的重要作用[4]。T OY已在SICStus Prolog [15]之上实现，使用SICStus提供的FD和R求解器以及H求解器的Prolog代码。CFLP目标求解通过惰性收缩来评估对程序定义函数的调用，并通过引入新的局部变量来分解混合约束最终，纯FD和R约束出现，必须提交给相应的求解器。我们的建议求解器的合作是基于FD和R求解器之间的通信通过特殊的通信约束称为桥梁。桥u #== v约束u：：int和v：：real取相同的整数值。我们的系统将桥梁保存在一个特殊的存储库中，它们有两个目的，即绑定和传播。绑定只是在桥的一端初始化一个变量，每当桥的另一端变成一个数值时，这个变量就会出现在桥的一端。传播是一个更复杂的操作，只要将纯约束提交给FD或R求解器，就会发生传播此时，依赖于可用桥的传播规则用于构建提交给配合求解器的配合约束（将R视为FD和反之亦然）。传播使两个求解器都能够利用另一个人的计算为了最大化传播的机会，CFLP目标求解程序已经通过操作进行了增强，以便根据某些规则尽可能地创建桥梁。显然，求解器的独立计算仍然是可能的。本文的其余部分组织如下。第二节回顾了CFLP编程的要点，并给出了一个CFLP程序，它解决了一个通用的问题，说明H+FD+R合作。第3节提出了一个正式的描述，共同-通过约束惰性缩小的方式进行操作目标求解，并通过用于创建桥和传播配对约束的规则进行增强第4节介绍了我们目前在T OY系统中实现合作目标求解的一些细节，以及基于第2节程序的性能结果，表明S. Estévez-Martín等人/理论计算机科学电子笔记188（2007）3739通过桥接器传播配合约束会导致扩展时间的显著加速。第5节包括结论摘要、有关工作的简要讨论和对计划的未来工作的一些提示2CFLP编程在本节中，我们回顾了用于惰性约束函数式逻辑编程的CFLP方案[9，2，8]的要点，该方案作为我们提出的求解器合作的逻辑和语义2.1约束域H、 FD和 R我们假设一个通用签名<$=<$DC，FS<$，其中DC=n∈N DCn和FS=n∈NFSn是可数的有限个互不相交的构造函数符号和功能符号，按字母索引函数进一步分类对于每个n ∈ N，分解为区域相关的原函数PF n<$FS n和用户定义函数DF n=FSn\PF n。我们考虑一个特殊的符号，旨在表示一个未定义的值，我们假设布尔常数true，false∈DC0。我们还考虑变量的可数无限集合Var和本原元素的集合U（例如整数的集合Z或实数的集合R表达式e∈Exp的语法为e：：= u|X|H|（e e1. 其中u∈ U，X∈Var且h∈DC_（？）e m）。下面的表达式分类是有用的：（X em），当X∈V ar且m≥0时，被称为可伸缩表达式，而u∈ U和（h em），当h∈DC可伸缩FS时，被称为刚性表达式。此外，刚性表达式（h em）称为活动的i ∈h∈FSn和m≥n，否则为被动。表达式的另一个重要子类是模式集t∈Pat，其语法定义为t：：= u|X|（c t m）|（ftm），其中u ∈ U，X∈Var，c∈DCn，m≤n，f∈FSn，e2= defe1ileq e2→！虚假e1#>= e2= defe2ileq e1→！真#+，#−，#，#/：：int→int→int，domain ： ： [int]→int→bool ，belongs：：int→[int] →bool，标签：：[labelType]→[int]→boolRrleq：：real→real→boole1e2=defe1rleq e2→！假e1>= e2= defe2rleq e1→！真正+，−，，/：：实数→实数→实数Mequiv：：int→real→boole1#==e2=defequiv e1e2→！真正表1约束域H、FD、R和M2.2程序规则的结构程序是形式为ft n= r<$C的约束程序规则的集合，其中f∈DF n，t n是模式的线性序列，r是表达式，C是有限合取δ1，.。，δ m的原子约束δ i，对于每个1≤i≤m，可能包括定义的函数符号的出现。谓词可以被建模为返回布尔值的定义函数，而子句p tn：−C++规则p tn= true在实践中，T OY和类似的约束函数逻辑语言要求程序规则在多态类型系统中是良好类型的S. Estévez-Martín等人/理论计算机科学电子笔记188（2007）3741作为一个运行的例子，其余的文件，我们考虑一个通用的程序编写的T OY解决了问题的搜索一个二维点位于一个离散的网格和一个连续的区域的交叉点。网格和区域都表示为布尔函数。它们可以作为参数传递，因为我们的编程框架支持更高阶的编程特性。% 离散点与连续点：type dPoint=（int，int）type cPoint=（real， real）% 集合和成员资格：类型setOfA =A-> boolisIn：：setOfA->A-> boolisInSet Element = Set Element%网格和区域作为点集type grid = setOf dPoints type region = setOf cPoints用于计算区域和网格的交集的%谓词：bothIn：：region -> grid ->dPoint -> boolbothIn区域网格（X，Y）：-X #== RX，Y #== RY，isIn区域（RX，RY），isIn网格（X，Y），标记[][X，Y]我们将对各种参数给定大小的正方形网格和三角形区域尝试bothIn谓词% 方形网格：square：：int -> gridsquareN（X，Y）：-domain [X，Y] 0N%三角形区域：triangle：： cPoint -> real ->region triangle（RX0，RY0）H（RX，RY）：-r3r2（RX0，RY0）ˆHvR1RY>= RY0- H，RY- RX = RY0- RX 0，RY + RX = RY0 + RX 0我们从一个给定的上顶点（RX0，RY0）和一个给定的高度H建立一个等腰三角 形 。 三 个 顶 点 是 （ RX0 ， RY0 ） ， （ RX0−H ， RY0−H ） ， （ RX0+H ，RY0−H），三角形内的区域由直线r1：RY=RY0−H，r2：RY−RX=RY0−RX0和r3 ： RY+RX=RY0+RX0 包 围 ， 并 由 三 个 线 性 不 等 式 的 结 合 来 表 征 ： C1 ：RY≥RY0−H，C2：RY−RX≤RY0−RX0和C3：RY+RX≤RY0+RX0。这解释了三角形谓词中的实数算术约束。作为这个程序的目标求解的一个例子，我们固定两个整数值d和n，使得（d，d）是网格（正方形n）的中点，其中（n+ 1）2是42S. Estévez-Martín等人/理论计算机科学电子笔记188（2007）37（d，d）正方形网格内离散点的总数。例如，我们可以选择n= 4和d= 2。我们考虑三个目标，计算这个固定的正方形网格与三个不同的三角形区域的交集：• 目标1：bothIn（三角形（d+1/2，d+1）1/2）（正方形n）（X，Y）。 这个目标失败了。• 目标2：bothIn（三角形（d，d+1/2）1）（正方形n）（X，Y）。该目标计算（X，Y）的一个解，对应于点（d，d）。• 目标3：bothIn（三角形（d，d+1/2）2）（正方形n）（X，Y）。该目标计算（X，Y）的四个解，对应于点（d，d）、（d−1，d− 1）、（d，d−1）和（d+1，d− 1）。（0，n）（n，n）（0，n）（n，n）（0，n）（n，n）1/2ˆˆ1v2v（0，0）（n，0）（0，0）（n，0）（0，0）（n，0）目标1目标2目标33合作目标求解扩展[9，2]中给出的惰性约束函数逻辑编程的操作语义，我们在本节中设计了一个基于约束惰性收缩和求解器协作机制的目标求解演算。3.1目标的结构我们考虑一般形式G U的目标。P Q C Q M Q H Q F Q R，以便表示H、FD和R上的求解器协作的计算的一般状态。符号Q被解释为合取。• U是计算中局部变量的有限集合。• P是所谓的形式为e1 → t1的产生式的合取，.，en→tn，其中ei ∈Exp，ti∈Pat，对所有的1 ≤i≤n. G的产生变量集定义为在t1.. t n.• C是待解约束的有限合取，可能包括定义函数符号的出现。• M是FD和R之间的所谓通信存储，具有仅涉及变量和整数或实值的原语• H是所谓的Herbrand存储，具有严格的相等/不等原始约束和具有变量绑定的答案替换。（d，d）（d，d）S. Estévez-Martín等人/理论计算机科学电子笔记188（2007）3743• F是所谓的有限域存储，具有有限域原语约束和带有整数变量绑定的答案替换。• R是所谓的实算术存储，具有原始的实算术约束和带有实变量绑定的答案替换。我们研究满足[9]中给出的目标不变量的容许目标G，并且使得在M中没有变量具有多于一个桥。我们也写□来表示一个不一致的目标。 此外，我们说变量X是目标G中的所需变量i，X出现在G的任何约束存储中（即，M，H，F或R），并且μ（X）/=μ对于对应约束存储的每个解μ都成立。例如，X是有限域约束X#>=3的要求变量，但不是严格不等约束s（X）/=0的要求变量，其中s和0是构造器符号。在续集中，我们使用以下符号，以便通过应用替代σ和添加来指示目标的转换σ到相应的商店：• （PQCQMQHQFQR）@Hσ=def（PσQCσQMσQH<$σQFσQRσ）• （PQCQMQHQFQR）@Fσ=def（PσQCσQMσQHσQF<$σQRσ）• （PQCQMQHQFQR）@Rσ=def（PσQCσQMσQHσQFσQR<$σ）其中（<$Qθ）Tσ=def<$Qθσ，（<$Qθ）代表H、F或R。3.2基于约束惰性缩窄的合作目标求解[9]中提出了约束惰性缩窄演算CLNC（D），作为在单个约束域D（例如H、FD或R）上求解CFLP（D）的目标和在域D上求解单个约束求解器的合适计算机制。现在，为了给我们关于约束域H、FD和R上的求解器合作的建议提供一个正式的基础，同时保持CFLP（D）框架中获得的良好性质，我们必须重新制定微积分CLNC（D）的目标转换规则，以处理上面定义的目标类。 我们有 区分两种规则：通过产生式共享的约束惰性窄化规则（这些规则很容易从[9]改编;见表2），新的规则的合作约束求解的约束存储。3.3合作目标求解规则以下三个规则描述了通过新的产生式从C中的约束中惰性地移除非原始参数的过程，创建存储在M中的新的桥约束以实现传播，以及通过桥的配对约束的实际传播（召回引入），与向FD和R存储器提交原始约束同时发生。FC展平约束你好。P Q p e n→！T，CQM QH QF QR阿维尼翁足球俱乐部M、U. a m→ V m，P Q p t n→！t，CQM QH QF QR如果有任何i∈/P at，则在没有pat的情况下，Vm是新的，44S. Estévez-Martín等人/理论计算机科学电子笔记188（2007）37DC分解你好 。 hem→htm， PQCQMQHQFQRDCU。em→tm， PQCQMQHQFQRCFCo nictFail ureU. e→t，PQCQMQHQFQRCF□如果e是rigid且经过ive，则t∈/Var，e且具有连通根。SP简单生产你好 。 s→t，PQCQMQHQFQ R RRRSPRUJ。（PQCQMQHQFQR）@Hσ若s<$X∈Var，t∈/Var，σ={X <$→t}或s∈Pat，t<$X∈Var，σ={X <$→s};UJ<$U\{X}.IM模拟美国加利福尼亚州 hem→X，PQCQMQHQFQRIMXm，U. （em→Xm， PQCQMQHQFQR）σ若hem∈/Pat是passi ve，则X是dem且dvarial e且dσ={X <$→hXm}。EL消除法e→X，PQCQMQHQFQR RU。PQCQMQHQF QR如果X不会发生在目标的其余部分。DF定义函数你好 。fenak→t，PQCQMQHQFQRDFX，Y，U e n→ t n，r → X，X ak→ t，PQCJ，CQMQHQFQ R若f∈DFn（k>0），t∈/Var或t是可分解的，R：ftn→r∈CJ是P中规则的一个自由的变元，其中Y = var（R），X是新变元。PC放置约束你好 。 pen→t，PQCQMQHQFQ R RRRP PPU。 PQpen→！t，CQMQHQFQR若p∈PF n （k>0），则t∈/V或t是一个dedemandedvaraliablee.表2受约束的惰性缩小p tn是从p en通过用Vi替换每个不是模式的ei而获得的。SB Set Bridges你好。PQ p t n→！t，CQM QH QF QRR乌普萨拉州PQ p t n→！ t，CQMJ，M QH QF QR如果π = p t n→！t是原始约束，并且(i) π是FD约束，并且MJ=桥FD→R（π，M）否则(ii) π是一个R常数，且MJ=bridgesR→FD（π，M）/=π。在这两种情况下，V=var（MJ）\var（M）是出现在由表3、4中描述的桥接操作创建SC提交约束你好。P Q p t n→！t，C Q M Q H Q F Q RR SS。P Q C Q MJQ HJQ FJQ RJ如果SB不能用于设置新网桥，并且以下情况之一适用：(i) 如果p t n→！t是桥u#==uJ则MJ=（u#==uJ，M），HJ=H，FJ=F，RJ=R。S. Estévez-Martín等人/理论计算机科学电子笔记188（2007）3745(ii) 如果p t n→！t是原始Herbrand约束seq t1t2→！t则MJ=M，HJ=（seq t1t2→！t，H），FJ=F且RJ=R。(iii) 如果p t n→！t是原始FD约束π，则MJ=M，HJ=H，FJ=（π，F）并且RJ=（RJJ，R），其中RJJ=传播FD→R（π，M）。(iv) 如果p t n→！t是本原R约束π，则MJ= M，HJ= H，FJ=（FJ，F），且RJ=（π，R），其中FJ=p算子sR→Fd（π，M）.其中表3和表4中给出的传播操作负责通过M中的桥来构造配合约束，以便在FD和R悬挂物之间传播。|表3从FD到R的桥接约束和转换3.4约束求解最后四条规则通过在相应悬挂物（M、H、F或R）上应用约束解算器来描述约束解算过程。我们注意到，为了尊重目标的容许条件并执行足够的惰性评估，我们必须保护存储中出现的所有生成变量χ=pvar（P）免受求解器导致的最终绑定（更多细节请参见[9]我们使用以下符号：• H=H，χ=Y。H Jidicateneonedede• H_i=H_i= H_i ，Hisunsatisfiable）.类似的符号用于指示FD和R解算器的行为M解算器的简单行为被明确地显示。MSM-解算器• 你好。 PQCQX#==uJ，MQHQFQRM S1UJ. （PQCQMQHQFQR）@Fσπ桥FD→R（π，M）传播FD→R（π，M）domain [X1，.，X n] ab{Xi#==没有桥RX I|1≤i≤n，X i在M中有，RX i新}{a≤RXi，RXi（Xi#==RXi）∈M}≤B |1≤i≤n属于X [a1，.，a n]{X #== RX|X在M中没有桥接，RX新}{min（a1，. a n）≤RX，RX≤max（a1，. a n）1≤i≤n（X#== RX）∈M}t1#，#=>，#=）{X i #== RX i|1≤i≤2，t i是变量X i，在M中没有桥，RXinew}{tRt2t1>=t2不发生在表4中被视为t2t1resp。的实现。(1) #>（L，R，Out，Cin，Cout）：-(2) hnf（L，HL，Cin，Cout1），hnf（R，HR，Cout1，Cout），(3) searchVarsR（HL，Cout2，Cout 3，HLR），searchVarsR（HR，Cout3，Cout，HRR），(4) （（Out=true，HL#>HR，{N>HRR}）;（Out=false，HL#<=HR，{N<=HRR}））。这里，第（2）行实现FC和PC目标转换规则;第（3）行通过向混合H+M存储添加新的所需桥来实现规则SB;第（4）行实现传播（规则SC的情况（iii）），将FD约束及其在R中的配对发送到相应的求解器。注意，因为我们特别是对于关系约束，互补情况（真和假结果）对应于互补约束。S. Estévez-Martín等人/理论计算机科学电子笔记188（2007）37494.2性能结果表5比较了运行示例（见第2小节）中执行第2节目标的时间结果。2）的情况。第一列表示目标，第二列和第三列表示参数d和n，分别确定正方形网格的中点和大小。接下来的列以（tB/tBP）的形式显示运行时间（毫秒），其中tB代表仅使用桥进行绑定的系统，tBP代表使用桥进行传播的系统。这些列中的值在 这 个 简 单 的 例 子中 ， 我 们 看 到 ，有限域搜索空间被从R到R的传播极大地削减了。FD。有限域求解器不足以像单纯形法那样有效地切割搜索空间。目标Dn1234512000020000004000040000001828/0179000/0--------22000020000004000040000001125/0111201/02172/0215156/0------32000020000004000040000001125/0111329/01485/0147406/00/00/01500/0147453/02203/0216156/0表5性能结果5结论我们已经提出了一个建议的合作的求解器的三个领域H，FD和R的约束功能逻辑编程，基于传播的FD和R求解器之间的配合约束。我们的演讲包括合作目标求解的形式化描述，作为现有目标求解演算的丰富[9，2]，以及作为扩展的有效实现的讨论一个现有的约束函数逻辑系统，它已经被证明有一个合理的性能[3]。我们已经获得了令人鼓舞的性能结果，目标求解的例子表明，交配约束的传播大大减少了搜索空间，从而导致执行时间的显着除了在顺序环境中提高效率的好处外，求解器的合作甚至开辟了利用新兴技术的可能性，例如并行架构和网格计算，用于在不同的处理元件（平台，处理器或核心）上并行执行不同的求解器正如在引言中提到的，约束求解器的合作在过去几年中得到了广泛的研究[4]。让我们在这一点50S. Estévez-Martín等人/理论计算机科学电子笔记188（2007）37只是有限的相关工作。在他的博士论文[12]中，Eric Monfroy提出了BALI（用于求解器集成的绑定架构，另见[13，14]），提供了许多合作原语，可用于根据不同的策略组合各种求解器。Monfroy的方法假设所有的求解器都在一个共同的存储器上工作，而我们目前的建议需要不同存储器之间的通信。Mircea Marin [10]开发了一种CFLP方案，该方案将Monfroy与我们的建议相反，Marin的方法允许更高阶的统一，这导致更大的表达性和更低的实现效率。此外，Marin等人[11]实现的CFLP实例与我们的工作非常不同，因为它涉及代数符号计算的约束域上的四个求解器的组合。最近，Petra Hofstedt [6，5]提出了一种将各种约束系统和声明性语言组合成一个合作求解器的集成系统的通用方法。 在Hofstedt的建议中属于某个域D到D另一个领域的限制。传播，在本文中使用的，更类似于霍夫斯泰特Hofstedt这些和其他相关的工作鼓励我们继续我们的研究，旨在发现和实现更详细的通信手段之间的求解器，以及尝试他们的性能实验。 未来计划的工作还包括对协作的声明 性 语 义 进 行 建 模 。 本 文 中 描 述 的 实 现 将 很 快 可 用 （ 见http://toy.sourceforge.net）。引用[1] Are nas，P.， A. Fern'andez，A. Gil，F. L'opez-Fraguas，M. Rodr'englishue z-Artal ejoandF. 萨恩斯-佩雷兹，托伊 。AMul t iparadigmDecl ariveLanguage. Verrsio n 2. 二、2（2006），R.CaballleroandJ.S'anchez（Eds. ），可在www.example.com上获得http://toy.sourceforge.net。[2] d e lV ado-V'ırseda，R.， DecarativeConstrantPrgrammingwithithDef i nitio nlTres，in：Proc. 从CoS' 05开始（2005），pp. 184-199。[3] Fern'andez ， A.J. 、 T.霍 塔 拉 - 冈 萨 雷 斯 ， F 。是 的 ， 是 的 。delVado-V'ırseda ，ConstraintFunnctionalLogic Programming over Finite Domains ， Theory and Practice of LogicProgramming（2007），in Press.[4] 格朗维利耶湖E. Monfroy和F. Benhamou，约束编程中的协作求解器：简介，在：约束编程中的协作求解器研讨会，2001年。[5] Hofstedt，P.，“约束求解器的合作与协调”，博士 作者：Shaker Verlag Aachen（2001年）。S. Estévez-Martín等人/理论计算机科学电子笔记188（2007）3751[6] Hofstedt，P.和P. Pepper，声明式和约束式编程的集成，逻辑编程的理论与实践，2007年出版。[7] Ja Zahar，J.和M. Maher，约束逻辑程序设计：综述，逻辑程序设计杂志19 20（1994），pp. 503-581[8] Lo'pez-Fraguas， F.，