Enumerating Query Plans via Conditional Tableau Interpolation

Abstract

Database query optimization studies the problem of finding equivalent and efficient query execution plans for user queries under schema constraints. Logic-based approaches to query optimization leverage automated theorem proving and Craig interpolation to enumerate query plans that are correct and performance-optimal. In this thesis, we investigate and improve one of the state-of-the-art logic-based query optimizers – the Interpolation Test Bed (ITB).

We begin by formally capturing the physical data independence framework and query optimization problem with first-order logic. Then, we give a gentle introduction to the classical results from logic that form the basis of logic-based query optimizers. We re-establish the correctness of ITB’s conditional tableau interpolation mechanism by reduction to free-variable tableau interpolation. To facilitate the reduction proof, we introduce interpolation rules for the free-variable tableau and prove the correctness of interpolation. Then we show the correctness of conditional tableau interpolation by reduction.

We investigate a limitation of ITB’s forward chaining design, which causes missing optimal plans. To address this limitation, we propose a rewriting procedure inspired by Magic Set Transformation (MST), to extend the plan space for the current ITB system. We show that the propose rewriting procedure effectively generates the missing query plans, which are otherwise not found, while accommodating the existing forward chaining design.