Efficient Computation of Graph Overlaps for Rule Composition: Theory and Z3 Prototyping


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. We define the composition of conditional SqPO rules and develop two strategies for its implementation, each theoretically and via the Python API of the SMT solver Z3. They include a straightforward generate-and-test strategy based on forbidden graph patterns 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 two strategies, establishing the superiority of the modular one.

In: arXiv preprint (accepted for GCM 2020)