工作流可满足性的约简增量模式回溯法

在大量云/服务化资源造成的性能压力下，增量模式回溯法(Incremental Pattern Backtracking, IPB)及其k指派技术是工作流可满足性求解的首选途径，但对“欠约束”实例，其模式枚举性能显著下降，不利于大量可行解的优化选择。针对该问题提出新颖的简指派图概念，证明其可取代k指派图用于模式授权匹配验证，且尽管其块邻域大小耦合了图的整体信息，但仍可以增量方式计算。进而，分析了增量化简指派的实施条件和效果，及其主要影响因素。由此建立了约简增量模式回溯法(Reduced Incremental Pattern Backtracking, RIPB)。在资源配比为2～100的两个仿真实例集上测试，实验结果表明：在其基本子集上，RIPB较IPB有0.96～1.24倍时间性能优势；当资源比例升高或约束密度降低时，RIPB的优势有不同程度扩大；特别地，对资源配比为10而授权比例在1/2左右的两个子集，RIPB的平均优势分别可达1.29和1.61倍。     

形式化方法与应用专题前言

<正>形式化方法是采用数学方法,对复杂计算机系统建立严格语法与语义规范的系统设计与验证方法,常用于复杂动态系统的需求规约、模型设计和属性验证,在计算机硬件设计、软件系统构造、控制系统模型设计与分析、通信系统协议验证和程序代码合成等方面得到了成功的应用.近年来,在深度学习、区块链、量子计算、物理信息融合系统等新兴领域,形式化方法也逐步应用和适配,对提升系统的安全性和可靠性起到了极大的促进作用.