Graphiti: Bridging Graph and Relational Database Queries
Yang He, Ruijie Fang, Isil Dillig, Yuepeng Wang
TL;DR
Graphiti introduces a formal framework for proving or refuting equivalence between graph queries in Cypher and relational queries in SQL by leveraging database transformers that map graph instances to induced relational schemas. A correct-by-construction transpilation translates Cypher queries to SQL on the induced schema, and a residual database transformer reduces the original problem to SQL equivalence checking with existing tools. The approach is implemented and evaluated on 410 benchmarks, demonstrating its effectiveness for both verification and counterexample generation, and exposing subtle bugs in real-world Cypher translations. The work highlights the practical impact for correctness in graph-relational interoperability and lays groundwork for broader transformer-based reasoning and tooling. It also shows that automated transpilation can be fast and, in many cases, produces competitive or better-performing SQL queries. The framework paves the way for safer migrations and more reliable cross-model query reasoning in real systems.
Abstract
This paper presents an automated reasoning technique for checking equivalence between graph database queries written in Cypher and relational queries in SQL. To formalize a suitable notion of equivalence in this setting, we introduce the concept of database transformers, which transform database instances between graph and relational models. We then propose a novel verification methodology that checks equivalence modulo a given transformer by reducing the original problem to verifying equivalence between a pair of SQL queries. This reduction is achieved by embedding a subset of Cypher into SQL through syntax-directed translation, allowing us to leverage existing research on automated reasoning for SQL while obviating the need for reasoning simultaneously over two different data models. We have implemented our approach in a tool called Graphiti and used it to check equivalence between graph and relational queries. Our experiments demonstrate that Graphiti is useful both for verification and refutation and that it can uncover subtle bugs, including those found in Cypher tutorials and academic papers.