用于规则合成的高效图重叠计算：理论与Z3原型
Efficient Computation of Graph Overlaps for Rule Composition: Theory and Z3 Prototyping
摘要：
图变换理论依赖于规则的组合来表达规则序列的效果。在实践中，图经常受到约束，排除了许多组合规则的候选者。专注于倍半推出（SqPO）语义的情况下，我们开发了一些替代策略计算组合物，每一个理论和实现通过Python API的Z3定理证明。该策略包括一个简单的生成和测试策略的基础上禁止的图形模式，一个更隐式的逻辑编码的负约束的变体，和一个模块化的策略，其中的模式被分解为禁止的关系模式。对于有机化学中聚合物形成的玩具模型，我们比较了三种策略在执行时间和内存消耗方面的性能。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
