开发全幺模线性规划用于最优一致性检查：何时及为何它补充A*

# 为最优符合性检查开发全幺模线性规划：何时及为何它能与A∗互补
来源：https://arxiv.org/html/2605.26938

###### 摘要
基于对齐的符合性检查是比较观测流程执行与规范流程模型的先进方法。标准精确求解依赖于基于A∗的启发式搜索，在处理长迹或大量偏差时可能表现出指数级运行时间。本文引入了一种将基于对齐的符合性检查重新表述为定义在同步乘积可达图上的全幺模线性规划（LP）的方法。通过利用潜在的网络流结构，所提出的公式保证了通过LP松弛存在整数最优极值点解，从而避免了与整数变量和分支定界搜索相关的组合开销。我们对来自真实世界和合成基准数据集的超过210万个符合性检查实例进行了广泛的实证评估。结果表明，A∗和LP方法表现出互补的性能特征：前者在短且符合良好的迹上表现最佳，而LP公式在具有偏差的较长迹上提供了显著的加速，这正是符合性检查最具信息量的场景。基于这些发现，我们推导出简单的算法选择指南，结合了两种方法，相比始终使用A∗，平均运行时间节省38.6%，选择准确率达到96%。

###### 关键词：流程挖掘，基于对齐的符合性检查，线性规划，全幺模性

\affiliation [biu] organization=巴伊兰大学工程学院，城市=拉马特甘，国家=以色列

作者接受稿件。已接受发表于 *Expert Systems with Applications*。本版本根据CC BY-NC-ND 4.0许可提供。请引用已发表的文章。

## 1. 引言

符合性检查是流程挖掘中的一项基本任务，用于量化观测流程执行与规范流程模型的一致性程度。在可用技术中，基于对齐的符合性检查因其语义严谨性和诊断能力而成为标准，它能够计算观测迹与流程模型之间的最优对应关系。然而，计算此类最优对齐在计算上要求很高，实际解决方案通常依赖于启发式搜索算法（如A∗）或混合整数线性规划（MILP）公式。该领域的一个核心问题是：精确的符合性检查是否必然需要专门的搜索算法和定制实现，或者能否将其表达为标准的、现成的优化范式，从而受益于运筹学领域数十年的进展。虽然像A∗这样的方法在有利情况下可能非常有效，但它们需要仔细的启发式设计、定制实现，并且在处理长迹或高度偏差的迹时可能表现出指数行为。相比之下，那些能够在既定优化框架内建模的问题可以利用成熟的求解器技术，允许直接使用现成求解器而无需定制实现，前提是其底层结构支持高效的精确求解方法。

本文表明，基于对齐的符合性检查确实允许这样的公式。我们提出将该问题重新表述为定义在同步乘积可达图上的线性规划，其约束矩阵是全幺模的。我们将此公式称为符合性检查的全幺模重述（URC2）。关键的理论洞见是，由此产生的问题对应于一个具有整数右侧的最小成本网络流，这保证了LP可行域的每个极值点都是整数。换句话说，只要存在最优解，LP就允许一个整数最优解。因此，可以使用标准LP求解器计算最优对齐，而无需整数变量或分支定界搜索。重要的是，这一结果并未消除符合性检查固有的状态空间复杂性：在最坏情况下，同步乘积的可达图仍可能呈指数级增长。相反，URC2通过用单一线性优化问题替代启发式搜索或整数搜索，消除了探索状态空间内部的组合优化。在这个意义上，URC2将计算负担从搜索控制转移到对显式构造的状态空间部分进行线性优化，同时依赖求解器效率而非启发式探索。

在实践中，当前的URC2实现通过广度优先探索，在达到实际深度限制之前，构造同步乘积可达图的明确有界子图。该界限用于控制图构造成本，并避免在处理循环或并发时出现无界扩展。然后，在构造的子图上精确求解LP。URC2并非作为现有方法的通用替代品，而是作为A∗的补充。通过一项包含五个真实世界和合成基准数据集、超过210万个符合性检查实例的广泛实证研究，我们表明没有一种方法占主导地位。A∗在短且符合良好的迹上表现最佳，因为启发式指导使探索的状态空间保持较小。相比之下，URC2在具有偏差的较长迹上提供了显著的性能提升，这正是启发式搜索往往性能下降的场景。这种区别具有实际意义，因为符合性检查在预期存在偏差的场景中最具信息量，而完全符合的执行几乎无需分析。基于这些观察，我们识别了每种方法更优的条件，并推导出一个简单的算法选择规则，结合了两种方法。与单独持续应用A∗相比，这种混合策略在保持最优性的同时，实现了38.6%的运行时间节省。

本文的主要贡献包括：
1. **全幺模LP公式**。我们将基于对齐的符合性检查重新表述为同步乘积可达图上的最小成本网络流问题，并证明其约束矩阵是全幺模的。这保证了通过线性规划存在整数最优极值点解，从而无需整数变量即可实现精确对齐计算。
2. **大规模实证评估**。我们进行了一项广泛的实验研究，比较了URC2和A∗在超过210万个来自真实世界和合成数据集的实例上的表现，分析了不同迹长度、模型特征和偏差水平下的性能。
3. **实用算法选择指南**。我们识别了决定A∗和URC2相对性能的关键因素，并提供了一个简单、可操作的选择规则，实现了96%的选择准确率。结果表明两种方法具有互补性：URC2在长且不规范的迹上实现显著加速，而A∗在短且符合良好的迹上仍然更可取。

本文其余部分的结构如下：第2节回顾相关工作。第3节介绍所需概念和符号。第4节提出URC2公式并建立其全幺模性，随后第5节给出一个说明性示例。第6节描述实验设计，第7节报告实证结果。基于这些发现，第8节提供了在A∗和URC2之间进行选择的实用指南。第9节讨论局限性和未来研究方向，第10节总结全文。

## 2. 相关工作

自形式化以来，符合性检查已通过精确、近似、基于分解和符号方法进行了研究。本节回顾最相关的研究流，并将所提出的全幺模LP公式置于这些工作之中。

### 2.1 精确的基于对齐的符合性检查

对齐的概念由Adriansyah等人（2011，参考文献[1]）引入，随后在Adriansyah（2014，参考文献[2]）中形式化，其中通过使用A∗搜索同步乘积来计算迹与Petri网模型之间的最优对齐。这一公式已成为精确符合性检查的标准方法，并得到流程挖掘框架（如ProM和PM4Py）中成熟实现的支持。该方法依赖于从底层Petri网的标识方程推导出的启发式函数。后续van Dongen（2018，参考文献[36]）的工作引入了具有更紧界限的扩展标识方程，减少了搜索过程中求解的线性规划数量，特别是对于存在活动交换的迹。Li和van Zelst（2022，参考文献[19]）通过为基于分割点的对齐计算引入缓存策略，进一步提高了整体搜索效率。最近，Casas-Ramos等人（2024，参考文献[12]）提出了REACH，通过强制移动和部分可达图缓存来减少探索的状态数量以及每个状态的处理时间。尽管有这些改进，基于A∗的方法保留了最佳优先搜索的基本架构，可能在分支因子和对齐长度上表现出指数级复杂性，这使得它们对于具有许多偏差的迹或高并发性的模型可能不实用。

与此同时，数学规划方法已被探索用于符合性检查。De Leoni和Van Der Aalst（2013，参考文献[15]）提出了一种基于混合整数线性规划（MILP）的多视角方法，以整合控制流、数据、资源和时间。最近，Schwanen等人（2024，参考文献[24]）将块结构流程树的对齐问题公式化为MILP，表明对于这种受限模型类，问题属于NP。他们的公式需要整数变量来编码并行性，并且仅在不存在并行算子时才简化为多项式时间的线性规划。我们的方法在范围和工作机制上有所不同。URC2不限制模型类，而是支持通用工作流Petri网，并将对齐计算公式化为定义在同步乘积可达图上的最小成本网络流问题。关键洞见在于，所得约束矩阵是全幺模的，这保证了通过线性规划本身存在整数最优极值点解，而无需引入整数变量，且与并发程度无关。因此，所得公式在可达图规模上承认多项式时间可解性。

### 2.2 近似和启发式方法

近似和启发式技术以准确性换取可扩展性。Schuster等人（2020，参考文献[27]）提出利用流程树的分层结构进行对齐近似。基于采样的方法（Bauer等人，2019，参考文献[4]；Fani Sani等人，2020，参考文献[17]）在聚合符合性度量上提供统计保证，但牺牲了迹级诊断。启发式方法，包括进化算法（Buijs，2014，参考文献[10]；Taymouri和Carmona，2018，参考文献[30]），以损失最优性保证为代价实现了可扩展性。数据结构优化，如基于trie的缓存（Awad等人，2021，参考文献[3]）和串联重复压缩（Reißner等人，2020，参考文献[22]），减少了冗余计算，但依赖于迹相似性或重复模式。

### 2.3 分解策略

基于模型的分解将流程模型划分为独立对齐的片段（Munoz-Gama等人，2014，参考文献[21]；Taymouri和Carmona，2016，参考文献[31]；Cheng等人，2023，参考文献[13]）。基于日志的分解将事件日志水平或垂直分区以进行分布式处理（Valencia-Parra等人，2021，参考文献[34]；Bogdanov等人，2024，参考文献[8]）。这些方法以全局最优性换取可处理性，并可能引入重组开销。

### 2.4 符号编码

符号技术使用决策图（Bloemen等人，2018，参考文献[7]）或SAT/MaxSAT公式（Boltenhagen等人，2021，参考文献[9]）来压缩状态空间。虽然对剪枝有效，但在复杂模型上可能产生高内存消耗。

### 2.5 定位

全幺模LP公式URC2在基于对齐的符合性检查研究中占据了独特地位。与分解或近似方法不同，URC2寻找最优对齐。与基于A∗的方法（在处理不规范迹时可能表现出指数行为）不同，LP公式在构造的可达图规模上具有多项式复杂性。通过利用约束矩阵的结构性质，URC2避免了MILP公式的组合复杂性，并允许直接使用标准现成LP求解器，无需分支定界或切割平面过程。同时，URC2保留了基于对齐的符合性检查的诊断能力，这与基于令牌或采样的方法形成对比。其主要计算开销在于构造LP求解所依据的有界可达图部分。我们的实证结果揭示了互补的性能行为：A∗擅长处理短而符合良好的迹，而URC2在处理具有偏差的较长迹时提供了显著优势。这种互补性具有实际意义，因为恰好在发生偏差时，符合性检查最具信息量，这也激发了利用两种方法优势的算法选择指南。

## 3. 概念与符号

本节介绍开发URC2所需的概念，从定义用于表示预期和观测流程行为的流程模型和迹模型开始。在本节中，我们使用标准的流程挖掘定义和符号（例如参见Van Der Aalst，2016，参考文献[39]），并进行了一些调整。接下来，我们解释如何将流程模型和迹合并为同步乘积，然后定义成本函数和关键对齐概念。

###### 定义1（带标签的标记Petri网）
带标签的标记Petri网是一个元组 \(N=(P,T,F,\lambda,m_i,m_f)\)，其中