查询与约束可满足性的判定

在数据密集型系统中评估并提升数据质量是基础挑战，已催生众多针对数据转换与清洗的应用。然而，尽管模式设计、数据清洗与数据迁移如今在孤立情形下已得到较好理解，这些领域问题处理工具之间的相互作用却鲜受关注。我们的关注点在于判定是否存在数据转换过程序列，当其应用于（未转换的）输入数据时，能产生满足执行相关任务所需条件的数据。我们的目标是以关系设定为起点，开发一个解决该问题的框架。本文将数据处理工具抽象为黑盒过程。该抽象通过说明过程可能修改数据库的哪些部分，以及规定应用过程前后数据库所需状态的约束来描述过程。接着我们研究此背景下产生的基本算法问题，例如理解何时能保证过程序列适用于原始或转换后数据、何时成功改进数据，以及知识库何时能表示过程结果。最后，我们转向判定将过程序列应用于数据库是否导致由查询或约束指定的性质得到满足的问题。我们证明，对于某些广泛且现实的步骤与性质类，即便允许过程改变实例的模式，该问题也是可判定的。