CoReS: A tool for computing core graphs via SAT/SMT solvers

摘要

When specifying graph languages via type graphs, cores provide a convenient way to minimize the type graph without changing the corresponding graph language, i.e. the set of graphs that can be mapped homomorphically into the given type graph. However, given a type graph, the problem of finding its core is NP-hard. Using the tool CoReS, we automatically encode all required properties into SAT- and SMT-formulas in order to iteratively compute cores by employing the corresponding solvers. We obtain and discuss runtime results to evaluate and compare the two encodings. Furthermore we consider two application scenarios: invariant checking for graph transformation rules and minimization of conjunctive queries in the context of databases. (C) 2019 Elsevier Inc. All rights reserved.