Master’s Thesis Presentation • Data Systems • Enumerating Query Plans via Conditional Tableau Interpolation

Please note: This master’s thesis presentation will take place in DC 3317 and virtually over Zoom.

Eva Feng, Master’s candidate
David R. Cheriton School of Computer Science

Supervisor: Professor David Toman

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 plan 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 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 the 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 for the existing forward chaining design.

To attend this master’s thesis presentation in person, please go to DC 3317. You can also attend virtually using Zoom at https://uwaterloo.zoom.us/j/96218532566.