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: B. Hoffmann and M. Minas: Proceedings of the Eleventh International Workshop on Graph Computation Models (GCM 2020), Online-Workshop, 24th June 2020, Electronic Proceedings in Theoretical Computer Science 330, pp. 126–144.