Savioptimizavimas reliacinėse duomenų bazių valdymo sistemose

Most query planners are implemented as a set of specialized algorithms combined by hand written heuristics. Creating such planner requires an enormous amount of time and expertise, not to mention that due to a rather small exploration of search space planners can return suboptimal results. In this project, we present a way to encode query plans in SMT for equivalency checking. We use this to create general purpose planner which does its work in a background, continuously producing better plans for a dynamically created set of queries. We also experimentally test our planner with conventional one under a few standard benchmarks. From these benchmarks, we conclude that most of the time our planner performs as well as a state of the art planner. For some queries, it may also find better plans or, if we can not prove equivalency under the restricted DB model, may end up at plans that do not produce expected results