一句话：提出三种基于求解器的方法求解 Datalog 规则选择综合问题，其中编码为 ASP 的方案比现有技术快约 9 倍且综合出更高质量的程序。
给定一组候选 Datalog 规则，Datalog 综合中的“规则选择”问题要求选出一个子集使其满足规格（如输入输出样例）。在已有反例引导归纳综合工作的基础上，本文递进地提出三种基于求解器的方法：前两种可更一般地求解包含 Datalog 谓词的任意 SMT 公式，第三种则将问题编码为标准、现成的答案集编程（ASP）。该 ASP 编码相比当前最先进方法取得显著加速（几何平均约 9 倍），同时综合出更高质量的程序。这一方案序列探索了 SAT/SMT 与 Datalog 的交互空间，表明 ASP 是处理与推理 Datalog 的有前景工具。过程中作者还发现 Datalog 程序可视为单调 SMT 理论，在 SMT 中具有特别高效的交互，并为流行 SMT 求解器实现插件，可将任意 Datalog 程序作为自定义单调理论加载。最后使用多个底层求解器进行评估，给出更全面细致的对比。
Given a set of candidate Datalog rules, the Datalog synthesis-as-rule-selection problem chooses a subset of these rules that satisfies a specification (such as an input-output example). Building off prior work using counterexample-guided inductive synthesis, we present a progression of three solver-based approaches for solving Datalog synthesis-as-rule-selection problems. Two of our approaches offer some advantages over existing approaches, and can be used more generally to solve arbitrary SMT formulas containing Datalog predicates; the third—an encoding into standard, off-the-shelf answer set programming (ASP)—leads to significant speedups (∼ 9× geomean) over the state of the art while synthesizing higher quality programs. Our progression of solutions explores the space of interactions between SAT/SMT and Datalog, identifying ASP as a promising tool for working with and reasoning about Datalog. Along the way, we identify Datalog programs as monotonic SMT theories, which enjoy particularly efficient interactions in SMT; our plugins for popular SMT solvers make it easy to load an arbitrary Datalog program into the SMT solver as a custom monotonic theory. Finally, we evaluate our approaches using multiple underlying solvers to provide a more thorough and nuanced comparison against the current state of the art.
@article{paperbot2071,
title = {From SMT to ASP: Solver-Based Approaches to Solving Datalog Synthesis-as-Rule-Selection Problems},
author = {Aaron Bembenek and Michael Greenberg and Stephen Chong},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {POPL},
year = {2023},
doi = {10.1145/3571200}
}