论文标题
一阶计数查询的近似评估
Approximate Evaluation of First-Order Counting Queries
论文作者
论文摘要
Kuske和Schweikardt将非常表达的一阶计数逻辑（P）引入了使用计数操作的数据库查询。他们表明，具有有限程度的图表上有一个有效的模型检查算法，而Grohe和Schweikardt表明，对于有界深度的树木，可能不存在这种算法。 我们分析了此逻辑的片段fo（{> 0}）。尽管我们删除了两个非原子计数术语之间的减法和比较，但这种逻辑仍然表现得很表现力：我们允许嵌套计数和计数术语和任意数字之间的比较。我们的主要结果是FO（{> 0}）的模型检查问题的近似方案，该方案在有界扩展的结构上以线性fpt时间运行。该计划要么给出正确的答案，要么说“我不知道”。后者的答案只有在公式的数字符号中的小扰动可以使其既满足又不满意时给出。通过表明fo（{> 0}）的准确求解模型检查问题的补充，在有界深度的树上已经很难，并且只是稍微提高了fo（{> 0}）的表现力，甚至在树上也很难近似。
Kuske and Schweikardt introduced the very expressive first-order counting logic FOC(P) to model database queries with counting operations. They showed that there is an efficient model-checking algorithm on graphs with bounded degree, while Grohe and Schweikardt showed that probably no such algorithm exists for trees of bounded depth. We analyze the fragment FO({>0}) of this logic. While we remove for example subtraction and comparison between two non-atomic counting terms, this logic remains quite expressive: We allow nested counting and comparison between counting terms and arbitrarily large numbers. Our main result is an approximation scheme of the model-checking problem for FO({>0}) that runs in linear fpt time on structures with bounded expansion. This scheme either gives the correct answer or says "I do not know." The latter answer may only be given if small perturbations in the number-symbols of the formula could make it both satisfied and unsatisfied. This is complemented by showing that exactly solving the model-checking problem for FO({>0}) is already hard on trees of bounded depth and just slightly increasing the expressiveness of FO({>0}) makes even approximation hard on trees.
