论文标题
规则组成的图形重叠的有效计算：理论和Z3原型制作
Efficient Computation of Graph Overlaps for Rule Composition: Theory and Z3 Prototyping
论文作者
论文摘要
图转换理论依赖于规则的组成来表达规则序列的影响。在实践中，图表通常受到限制，排除许多候选人的构成规则。为了关注Sesqui-Pushout（SQPO）语义的情况，我们开发了许多用于计算组合物的替代策略，每个理论上，并通过Z3定理perver的Python API实现。这些策略包括基于禁止图形模式的直接生成测试策略，具有更隐含的负面约束逻辑编码的变体，以及一种模块化策略，其中模式被分解为禁止关系模式。对于有机化学中聚合物形成的玩具模型，我们比较了执行时间和记忆消耗的三种策略的性能。
Graph transformation theory relies upon the composition of rules to express the effects of sequences of rules. In practice, graphs are often subject to constraints, ruling out many candidates for composed rules. Focusing on the case of sesqui-pushout (SqPO) semantics, we develop a number of alternative strategies for computing compositions, each theoretically and with an implementation via the Python API of the Z3 theorem prover. The strategies comprise a straightforward generate-and-test strategy based on forbidden graph patterns, a variant with a more implicit logical encoding of the negative constraints, and a modular strategy, where the patterns are decomposed as forbidden relation patterns. For a toy model of polymer formation in organic chemistry, we compare the performance of the three strategies in terms of execution times and memory consumption.
