A Graph Transformation-Based Engine for the Automated Exploration of Constraint Models

In this demonstration, we present an engine leveraging graph transformations for the automated reformulation of constraint specifications of combinatorial search problems. These arise in many settings, such as planning, scheduling, routing and design. The engine is situated in the Constraint Modelling Pipeline that, starting from an initial high-level specification, can apply type-specific refinements while targeting solvers from multiple paradigms: SAT, SMT, Mixed Integer Programming, and Constraint Programming. The problem specification is crucial in producing an effective input for the target solver, motivating our work to explore the space of reformulations of an initial specification.

Our system transforms a constraint specification in the Essence language into an Abstract Syntax Tree (AST). These ASTs, considered as directed labelled graphs, serve as inputs to the graph transformation language GP2 (Graph Programs 2) for subsequent reformulation. Our engine currently employs a curated set of handcrafted rewrite rules applied sequentially to the ASTs by the GP2 framework. It is designed to learn the efficacy of various rewrites, prioritising those that yield superior performance outcomes. At this stage, our primary emphasis is ensuring the rewritten specifications’ soundness and semantic invariance.

Central to our methodology is constructing a search graph, where nodes represent model specifications and solutions, while edges represent graph transformations and solver performance. Through this search graph our system enables the exploration of constraint specification variants and the evaluation of their effects on lower-level refinement strategies and solvers. Finally, we present a visualisation tool that allows the interactive inspection of the search graph and its content.