The separation problem for a class Q of database queries is to find a query in Q that distinguishes between a given set of `positive' and `negative' data examples. Separation provides explanations of examples and underpins the query-by-example paradigm to support database users in constructing and refining queries. As the space of all separating queries can be large, it is helpful to succinctly represent this space by means of its most specific (logically strongest) and general (weakest) members. We investigate this extremal separation problem for classes of instance queries formulated in linear temporal logic LTL with the operators conjunction, next, and eventually. Our results range from tight complexity bounds for verifying and counting extremal separators to algorithms computing them.
翻译:数据库查询类Q的分离问题旨在从Q中找到一个查询,用以区分给定的“正例”与“负例”数据样本。分离为样本提供解释,并构成了“按例查询”范式的基础,以支持数据库用户构建与优化查询。由于所有分离查询的搜索空间可能非常庞大,通过其最具体(逻辑上最强)与最一般(最弱)的成员来简洁地表示该空间具有重要价值。我们研究了在具有合取、下一个与最终算子的线性时序逻辑LTL中公式化的实例查询类的极值分离问题。我们的研究成果涵盖了从验证与计数极值分离器的紧致复杂度界限,到计算这些分离器的算法。