从SMT到ASP：基于求解器的Datalog规则

From SMT to ASP: Solver-Based Approaches to Solving

Datalog Synthesis-as-Rule-Selection Problems

从SMT到ASP：基于求解器的Datalog规则选择合成方法

https://dl.acm.org/doi/pdf/10.1145/3571200

给定一组候选 Datalog 规则，Datalog 综合问题（作为规则选择的问题）会选择其中的一个子集，以满足某种规范（例如输入-输出示例）。在以往基于反例引导归纳综合（counterexample-guided inductive synthesis）工作的基础上，我们提出了三种基于求解器的方法来解决 Datalog 规则选择式综合问题。我们的两种方法相较于现有方法具有一些优势，并可以更广泛地用于求解包含 Datalog 谓词的任意 SMT 公式；第三种方法则是将其编码为标准、现成可用的答案集编程（ASP），与当前最先进的方法相比，在合成高质量程序的同时实现了显著的速度提升（几何平均约 9 倍）。

我们的解决方案演进过程探索了 SAT/SMT 与 Datalog 之间的交互空间，并指出 ASP 是处理和推理 Datalog 的一种有前景的工具。在此过程中，我们将 Datalog 程序识别为单调 SMT 理论，这类理论在 SMT 中具有特别高效的交互性能；我们为流行的 SMT 求解器开发的插件使其能够将任意 Datalog 程序作为自定义单调理论轻松加载到 SMT 求解器中。最后，我们使用多种底层求解器对我们的方法进行了评估，从而提供了比当前最先进方法更为全面且细致的对比分析。

CCS 概念：
• 软件及其工程 → 自动编程；约束与逻辑语言；
• 信息系统 → 关系数据库查询语言；
• 计算方法 → 逻辑编程与答案集编程。

附加关键词和短语：程序综合、Datalog、归纳逻辑编程、可满足性。

ACM 引用格式：
Aaron Bembenek, Michael Greenberg 和 Stephen Chong. 2023. 从 SMT 到 ASP：基于求解器的 Datalog 规则选择式综合方法。《ACM 程序设计语言进展》7, POPL, 文章 7 (2023 年 1 月), 33 页。https://doi.org/10.1145/3571200

1 引言

Datalog 是一种简单但出人意料地有用的逻辑编程语言。一个 Datalog 程序由一组推理规则组成，其执行相当于将这些规则运行至固定点（fixed point），从而对初始数据以及任何推导出的数据进行所有可能的推理。

尽管 Datalog 非常简单（或者正因如此），它在多个领域中得到了广泛应用，包括程序分析 [Bravenboer 和 Smaragdakis 2009；Reps 1995；Scholz 等 2016；Whaley 和 Lam 2004]、网络 [Loo 等 2006；Ryzhyk 和 Budiu 2019]、分布式系统 [Alvaro 等 2010a,b] 以及访问控制 [Dougherty 等 2006；Li 和 Mitchell 2003]。

随着人们对 Datalog 的兴趣日益增长，对于 Datalog 程序综合（program synthesis）的兴趣也随之增加。在这一任务中，目标是合成一个 Datalog 程序——即一组推理规则——以满足某种规范（specification），例如输入-输出示例。

一种流行策略包含两个步骤：首先生成一组候选 Datalog 规则；其次选择其中的一个子集，使其满足给定的规范。为了解决第二部分问题（称为“作为规则选择的综合”问题），已有多种技术被提出，包括基于委员会投票查询（query-by-committee）驱动的双向搜索 [Si 等 2018]、数值松弛方法 [Si 等 2019]，以及反例引导归纳综合（CEGIS）[Raghothaman 等 2020]。这些技术已在多个领域的 Datalog 综合问题上取得了稳步进展，包括知识发现、程序分析和关系代数等。

当前最先进的解决方案是 ProSynth [Raghothaman 等 2020]。它使用了 CEGIS [Solar-Lezama 等 2006] 方法，其中 SAT 求解器提出一组规则的选择，然后使用 Datalog 求解器来测试该选择是否符合规范。Datalog 的溯源信息用于向 SAT 求解器添加阻止约束，以引导其找到满足条件的选择。

本文介绍了一系列工具，它们构建在 ProSynth 基础之上，用于解决“作为规则选择的综合”问题。每种工具探索了 SAT 求解与 Horn 子句求值（Datalog 求值/寻找阻止子句）之间的不同平衡方式；不同的平衡方式影响了 SAT 求解器在指数级大的可能解空间中有效探索的能力。最终提出的工具相比 ProSynth 实现了显著的速度提升（几何平均约 9 倍），同时能够生成更高质量的规则选择。

MonoSynth

该工具基于以下观察：每一个 Datalog 程序都可以构成一个单调 SMT 理论的基础。也就是说，可以将任意 Datalog 程序转化为一个（理论上）高效的 SMT 理论。从实践角度看，它是 ProSynth 的一个更紧密集成于 SMT 求解器中的版本：像 ProSynth 一样，它使用 Datalog 求解器测试规则选择，并利用 Datalog 溯源生成冲突；但与 ProSynth 不同的是，它能为 SAT 求解器提供增量反馈，并剪枝不好的部分规则选择。此外，它提供了一种通用方法，可用于求解涉及 Datalog 谓词的 SMT 公式，而不仅限于 Datalog 程序综合。

LoopSynth

受答案集编程（ASP）算法的启发，该工具采用了一种截然不同的方法来整合 SAT 求解与 Horn 子句求值。在 ProSynth 和 MonoSynth 中，SAT 求解器从未看到候选规则；而在本方法中，候选规则的实例化版本（无变量）会被传递给 SAT 求解器。这为 SAT 求解器提供了更多信息，有助于其指导满足赋值的搜索。Datalog 求解器用于确认 SAT 模型确实解决了问题；如果没有，则生成循环公式并加入 SAT 求解器中。与 MonoSynth 类似，LoopSynth 也可以广泛用于求解涉及 Datalog 谓词的 SMT 公式，而不仅限于 Datalog 程序综合。

ASPSynth

比 LoopSynth 更进一步，该工具直接将 Datalog “作为规则选择的综合”问题编码为 ASP 形式。概念上，我们使用的 ASP 求解器结合了 Horn 子句求值与 SAT 求解，与其他工具类似。然而，通过在一个统一的搜索过程中紧密集成这两种范式，ASP 能够更有效地探索解空间。

我们在 ProSynth 基准套件上对四种工具进行了细致的评估。为了排除 SAT 求解器内部机制带来的性能偏差，我们分别基于 Z3 [Moura 和 Bjørner 2008] 和 CVC4 [Barrett 等 2011] 构建了 ProSynth、LoopSynth 和 MonoSynth 的版本，并基于 Clingo [Gebser 等 2011b] 和 WASP [Alviano 等 2013] 构建了 ASPSynth 的版本。

最终我们发现，MonoSynth 和 LoopSynth 相较 ProSynth 可带来一些改进，但结果并不一致且依赖于所使用的求解器。然而，ASPSynth-Clingo 表现出明显的优势。它的性能一方面来源于其作为一个单一、高度集成系统的工程实现，另一方面也得益于这种紧密集成使得它在搜索解空间时遇到的冲突更少。

成功的关键洞察在于视角的转变：从将 Datalog 视为一种独立的（单调的）逻辑编程语言——这是程序语言社区中一个常见且合理的观点，在近年来 Datalog 在该领域获得了应有的关注——转变为将其视为一种更具表达力的（非单调的）逻辑编程范式（即 ASP）的一个片段。这种视角的转变，使得我们能够从 SMT 求解器（程序语言社区首选的约束求解范式）转向 ASP 求解器——这些工具在逻辑编程和人工智能社区中受到了广泛关注，但在程序语言社区中却鲜有应用。

贡献

总而言之，我们做出了如下贡献：

• 我们提出了三种解决 Datalog 作为规则选择的综合问题 的全新方法，所有方法都探索了 SAT 求解与 Horn 子句求值的不同结合方式（见第 4、5 和 6 章）。其中两种方法提供了一种在 SMT 中描述 Datalog 谓词的方式，其应用范围超越了程序综合本身（见第 4 和第 5 章）。

• 我们使用多个后端 SAT 求解器对这些工具与当前最先进的 ProSynth 进行了全面评估（见第 7 章）。我们展示了求解器的选择对基于求解器算法的相对性能可能产生重大影响。

• 我们展示了 ASP 在解决程序语言社区关心的问题上的有效性：我们将 Datalog 综合编码为规则选择问题，并通过 ASP 实现了比当前最先进的 ProSynth 快一个数量级（几何平均约 9 倍）的速度提升（见第 7.4 章）。我们的工作为程序语言社区提供了关于 ASP 技术的实践性概述，涵盖了基于循环公式的 SAT 编码方法（见第 5 章）以及直接求解的方法（见第 6 章）。

• 我们阐明了当前 Datalog 作为规则选择的综合问题 的设定中存在的局限性，并展示了如何将其推广为一种有界模型检测的形式（见第 8 章）。

2 作为规则选择的 Datalog 综合

第 2.1 节介绍 Datalog 的背景知识，第 2.2 节介绍“作为规则选择的 Datalog 综合”问题。第 2.3 节概述了一种基线方法以及我们提出的一系列解决方案。

2.1 Datalog

一个 Datalog 程序 [Gallaire 和 Minker 1978；Green 等 2013] 是一组关于谓词 的推理规则，其中每个规则作用于项（terms）的向量 t 上，并且每条规则都是一个 Horn 子句：

一个项 （term） 要么是一个常量 ，要么是一个变量 （我们使用粗体 c 和 X 分别表示常量和变量的向量）。原子 ₀(t₀) 是该规则的头 （head）；其余的原子构成了规则的体 （body）（可以为空）。头中的变量必须出现在体中 。

直观上，每条规则可以从右向左读作一个蕴含式：对所有变量进行全称量化后，体中原子的合取蕴含头中的原子。

一个 Datalog 程序 的语义是定义在一组输入事实（即基础原子，称为外延数据库，或 EDB）上的。如果我们有输入事实 ，则 () 被定义为在初始事实 的基础上，通过不断应用程序 中的规则所达到的最小不动点 ，通常使用半朴素求值法（semi-naive evaluation）来计算。

最终得到的事实集合就是输出结果（称为内涵数据库，或 IDB）。从函数的角度来看， 是从 EDB 到 IDB 的正单调函数 ：如果 ⊆ ，则 () ⊆ ()。或者，从模型论的角度来看，Datalog 程序与 EDB 结合的意义是：将 EDB 和程序中的规则视为逻辑蕴含时，所得到的最小 Herbrand 模型 。

Datalog 的求值可以非常高效，并且适用于多种强大的优化技术（例如并行计算、目标导向搜索）。尽管它不像通用逻辑编程语言（如 Prolog）那样具有表达力，但 Datalog 在表达能力和性能之间的良好平衡使其成为某些领域中流行的实现选择，例如静态分析 [Bembenek 等 2020；Bravenboer 和 Smaragdakis 2009；Flores-Montoya 和 Schulte 2020；Grech 等 2019, 2018；Guarnieri 和 Livshits 2009；Jordan 等 2016；Livshits 和 Lam 2005；Reps 1995；Scholz 等 2016；Tsankov 等 2018；Whaley 和 Lam 2004]。

2.2 Datalog 的综合

Datalog 程序综合的任务是合成一组满足某种规范的 Datalog 规则。我们建立在一系列 Datalog 综合工作的基础上，这些工作始于 ALPS [Si 等 2018]，该研究提出了一种方法，可以从元规则（meta-rules）生成一组候选 Datalog 规则。

给定这组候选规则后，ALPS 会选择一个子集，使其在输入-输出示例上表现出正确的行为。这个任务——从一组候选 Datalog 规则中筛选出一个满足规范的子集——被称为“作为规则选择的综合”（synthesis as rule selection）。

ALPS 使用一种由委员会投票查询（query-by-committee）驱动的双向搜索策略来解决这一问题。后续的一系列研究专注于“作为规则选择的综合”问题（假设候选规则已由 ALPS 生成），采用了一些受数值松弛方法启发的技术 [Si 等 2019]，以及最近使用的反例引导归纳综合（CEGIS）方法 [Raghothaman 等 2020]。我们的算法正是构建在最后这种方法之上的。

作为规则选择的综合（Synthesis as Rule Selection） 。给定：

• （a）一个输入样本以及正例和负例输出元组（output tuples），

• 和（b）一组候选规则，

任务是生成：

• （c）候选规则的一个子集，使得它能够产生所有正例输出，而不产生任何负例输出。

形式化地，设 为输入元组（即 EDB），T⁺exp 为正输出元组集合（IDB 的一个子集），T⁻exp 为负输出元组集合。如果 all 是所有候选规则的集合，我们需要从中选择一组规则 ⊆ all，使得：

• T⁺exp ⊆ ()（即所有正例输出都包含在结果中），且

• T⁻exp ∩ () = ∅（即不产生任何负例输出）。

例如，在合成图的传递闭包（transitive closure）时，规范可能包括由 edge 谓词定义的一个示例图 ，以及由 path 谓词组成的集合 T⁺exp 和 T⁻exp；而候选规则集合 all 则包含用 edge 和自身来定义 path 的那些规则（见图1）。

2.3 四种方法

我们提出了四种解决 Datalog 作为规则选择的综合问题 的方法：一种是当前最先进的方法，另外三种是我们提出的新方法。我们使用如下图示语言来描绘每种方法：

• SAT 求解

  用蓝色表示，

• Datalog 求值

  用橙色表示；

• 虚线箭头

  表示一次性交互，

• 实线箭头

  表示重复交互；

• 组件标注为独立可执行文件（ .exe ）、库文件（ .lib ）或解释执行的 Python 程序（ .py ）。

我们首先介绍当前最先进的方法 ProSynth [Raghothaman 等 2020]。ProSynth 连接了一个 SAT 求解器和一个增强了“原因溯源”（why 和 why-not provenance）功能的 Datalog 求解器（见第 3 节；图 2），在反例引导综合（CEGIS）循环 [Solar-Lezama 等 2006] 中频繁调用 Datalog 求解和 SAT 求解。

我们的三种方法都旨在减少这种 CEGIS 循环的开销；也就是说，它们减少了在综合过程中为纠正错误猜测而进行的来回调用次数。

我们的第一种方法 MonoSynth 利用了 Datalog 的单调性，将 Datalog 谓词视为 SMT 谓词（见第 4 节；图 3）。MonoSynth 只对 SMT 进行一次调用，但会对 Datalog 求值进行多次调用；与 ProSynth 一样，它也依赖于溯源信息。

我们剩下的两种方法借鉴了答案集编程 （ASP）中的思想。ASP 求解器通常分为两个阶段：实例化 （grounding）和求解 （solving）。

• 实例化阶段会消除所有变量，生成“实例化”规则。这是一个代价较高的过程，在最坏情况下退化为显式枚举所有可能的变量替换组合。

• 实际上，实例化工具使用各种策略来避免简单的枚举。

在 ASP 中，求解阶段 是一种扩展了 SAT 搜索的形式，加入了确保最终模型满足逻辑程序语义的机制（即，与 Horn 子句求解保持一致）。

这两种方法中的第一个是 LoopSynth ，它受到 ASSAT [Lin 和 Zhao 2004] 中“循环公式”（loop formulas）概念的启发（见第 5 节；图 5）。

我们首先将候选规则编码为一个 ASP 程序，并使用 Gringo 实例化器 [Gebser 等 2007] 生成实例化规则。然后我们使用 Clark 完备化 [Clark 1977] 将这些实例化规则和输入-输出示例编码为 SAT 公式，并断言循环公式以确保我们生成的是一个稳定模型（即有效解）。

与 MonoSynth 只调用一次 SMT 不同，LoopSynth 是增量地调用 SAT 。MonoSynth 在每次 CEGIS 迭中可能多次调用 Datalog；而 LoopSynth 则先对程序进行实例化——这相当于生成 IDB 的超集，也就是执行了 Datalog 求值——然后在每次 CEGIS 迭代中只调用一次 Datalog。LoopSynth 不使用任何 Datalog 的溯源信息 。

最后，我们在我们称之为 ASPSynth 的方法中，将问题直接编码为 ASP （见第 6 节；图 8）。

这种方法是最简单且最高效的：没有来回交互，只需将编码好的问题交给现成的 ASP 实例化器和求解器即可。此外，编码为 ASP 使得很容易为规则指定一个成本度量标准，从而提升我们所生成解决方案的质量。

3 当前最先进的方法：ProSynth

ProSynth 是目前解决 Datalog 作为规则选择的综合问题 的最先进工具 [Raghothaman 等 2020]。它通过在 SAT 求解器和 Datalog 求解器之间来回传递信息，实现了反例引导的归纳综合 （CEGIS），其结构如图 2 所示。

ProSynth 的输入是一个 Datalog 程序，其中包含了所有候选规则 all 中的规则，只不过每条规则都被扩展了一个新的前提 rule()，用以标识这是第 条规则。如果在 EDB 中设置了事实 rule()，则启用该候选规则；否则，该规则永远不会被触发。此外，all 中的每条规则都与 SAT 求解器中的一个布尔变量相关联。

SAT 求解器会生成一个猜测，决定启用哪些规则（即，在生成的模型中值为真的那些布尔变量）；对应的 rule()事实会在 Datalog 程序中被启用，并在示例输入上运行该程序。默认情况下，ProSynth 使用 Soufflé 的编译模式[Jordan 等 2016] 进行 Datalog 求值：Datalog 程序会被编译成 C++，然后需要进一步编译执行。

如果 Datalog 程序的输出不满足规范，ProSynth 的算法就会使用溯源 （provenance）[Woodruff 和 Stonebraker 1997] 来生成阻止约束（blocking constraints），并反馈给 SAT 求解器。

• 如果某个不期望的元组 出现在了 () 中，那么 why 溯源 [Buneman 等 2001] 可以指出是哪些规则导致了这个元组的产生——关闭这些规则中的一个或多个，有望排除这个元组。（但 ProSynth 使用的是 Soufflé 的溯源机制 [Zhao 等 2020]，它不会生成多条路径——因此，对于“过度确定”的元组（overdetermined tuples），即使关闭某些规则，它们可能仍然存在 [Green 等 2007]。）

• 如果某个期望的元组缺失 于 ()，那么 why-not 溯源 [Herschel 等 2009；Lee 等 2019] 可以指出有哪些规则本可以导致该元组的产生——启用这些规则中的某一条，有望生成该元组。

为了生成 why-not 溯源信息，ProSynth 使用了一种受 delta 调试 （delta debugging）启发的技术，从所有禁用的规则中筛选出一个更小的子集；只要这个子集中的一条规则未被启用，就无法推导出某个特定的期望元组。这一过程涉及多次调用 Soufflé。

ProSynth 将这些约束返回给 SAT 求解器，求解器再生成一个新的猜测；这一过程不断循环，直到找到一个解，或者搜索空间耗尽。

4 收紧循环：将 Datalog 视为一个单调 SMT 理论

我们的第一种算法直接建立在 ProSynth 的方法之上，并针对其 SAT 求解器与 Datalog 求解器之间松散集成所导致的两个潜在局限性进行了改进。

从工程角度来看，ProSynth 带来了多个操作系统进程之间通信的开销：ProSynth 本身是用 Python 编写的脚本，使用了 Z3 的绑定接口，但它会调用由 Soufflé 编译生成的独立可执行文件来运行 Datalog 程序。

从算法角度来看，在 SAT 求解器选择规则的过程中，Datalog 的计算并不会为其提供任何增量反馈：它只会在 SAT 求解器猜测出一组完整的候选规则（即每条规则都被标记为“启用”或“禁用”）之后才生成反例，即使 SAT 求解器在早期就做出了不可能通向可行解的选择也是如此。

我们的方法通过为 SMT 求解器扩展一个 Datalog 理论来解决这些限制。
与 ProSynth 类似，这个理论使用 Datalog 的 why 和 why-not 溯源机制来推导精确的理论冲突。
但与 ProSynth 不同的是，SAT 求解、Datalog 求解和冲突生成逻辑都发生在一个操作系统进程中。
此外，由于我们提出的 Datalog 理论是一个单调的 SMT 理论 （见第 4.1 和 4.2 节），Datalog 求解器能够基于部分规则选择 （即 SAT 求解器尚未对某些规则做出决定）向 SAT 求解器提供反例，从而使 SAT 求解器可以主动剪枝那些不可能产生解的搜索子空间。

我们的实现（见第 4.3 节）支持 Z3 和 CVC4，并能以一种直接的方式对综合问题进行编码（见第 4.4 节）。

4.1 背景知识：单调理论

在惰性 SMT 求解 [Nieuwenhuis 等 2006；Sebastiani 2007] 中——这是目前最受欢迎的两个 SMT 求解器的基础 [Barrett 等 2011；Moura 和 Bjørner 2008]——核心 SAT 求解器为理论谓词分配真值；如果从理论求解器的角度来看这一赋值不可满足，则会迫使 SAT 求解器回溯并提出新的赋值。

为了使这种集成高效运行，理论求解器应提供两种操作：

• 理论传播

  （theory propagation）：给定理论原子的部分赋值，推断出在该赋值下必须为真的其他理论文字（literals）。

• 冲突生成

  （conflict generation）：给定一个从理论角度看不可满足的部分赋值，生成一个包含冲突原子的子句；核心 SAT 求解器学习该子句的否定。

例如，假设我们有一个理论，其中包含形式为 < ~ 的谓词，且 < 的预期解释是整数小于关系。如果 SAT 求解器将原子 < ~ 和 ~ < 设为真，理论求解器可以传播得出原子 < 也必须为真。如果 SAT 求解器已经将原子 < 设为假，则理论求解器可以生成冲突：
< ~ ∧ ~ < ∧ ¬( < )。

SAT 求解器可以学习其否定，即：
¬( < ~) ∨ ¬(~ < ) ∨ < ，
最终促使搜索找到一个符合我们对 < 解释为“小于”的模型。

当理论满足以下两个条件时，SMT 效果最佳：

1. 在给定一个小的局部赋值时能够进行传播；

2. 在生成冲突时返回小的子句。

Bayless 等人 [2015] 提出了一类被称为单调理论 的理论，这类理论在存在一种有效方式来判定具体实例的情况下，能够同时满足上述两个标准。

一个单调理论是指其唯一的数据类型是布尔型，且所有谓词都是单调的 ，也就是说，对于任意这样的谓词 ，都有如下性质成立：

也就是说，如果一个谓词在某个比特位关闭时成立，那么当这个比特位开启后它仍然成立。

一个单调理论的例子是有限图的可达性 ：
给定边 是否包含在图中取决于变量 是否为真，那么谓词 ℎ,(1, ..., ) 为真当且仅当节点 到节点 存在一条路径。这从直观上看是单调的：当我们向图中添加一条边时，并不会使之前已有的任何路径失效。

如果存在一种高效的算法来判定该理论中具体实例的问题是否可满足，那么一个单调理论就能有效地执行理论传播和冲突生成 。我们上面提到的图可达性例子就符合这一条件：对于一个具体的图，我们可以直接运行标准的图算法。

那么，单调理论是如何进行理论传播和冲突生成的呢？

理论传播（Theory Propagation）

给定一个部分赋值 ，设 是该赋值限制在理论中暴露的布尔变量上的部分赋值（例如，在图可达性例子中的 ）。令 ⁺ 为该赋值的正扩展 ，即对 中未赋值的布尔变量都赋值为 1。

对于一个理论谓词 ，如果我们通过具体实例的判定程序确定 ⁺ ⇒ ¬ 成立，则可以推出 ⇒ ¬，于是我们可以传播文字 ¬。

同样地，使用负扩展 ⁻（即将 中未赋值的布尔变量都赋值为 0），如果 ⁻ ⇒ 成立，则我们可以传播文字 。

冲突生成（Conflict Generation）

给定一个由上述“过近似/欠近似”方案引发的冲突，冲突中总是存在某个理论原子 ，使得暴露的布尔变量的赋值与原子 的赋值一起是不可满足的。

在这种情况下：

• 如果 ⁻ ⇒ 成立，则 中的正文字蕴含 （可以为涉及 的冲突提供理由）；

• 如果 ⁺ ⇒ ¬ 成立，则 中的负文字蕴含 ¬（可以为涉及 ¬ 的冲突提供理由）。

当用于判定具体问题实例的算法能够提供其判断的见证信息 （witness）时，有时可以学习到比这些默认方式更优的子句。例如，从顶点 到顶点 的路径上的边就为原子 ℎ,(1, ..., ) 提供了一个合理的解释：因为这些边对应的布尔变量 必然是启用的 SMT 布尔变量的一个子集，所以它们构成了对该原子更为精确的理由。

单调理论通常用于生成性任务 （generative purposes）。例如：

• 有限图可达性的单调理论被用于生成满足某些可达性约束的图（即对 的赋值）[Bayless 等 2015]，以及合成能够在虚拟云网络中到达特定节点的数据包 [Backes 等 2019]；

• 计算树逻辑（CTL）的单调理论被用于合成由该逻辑描述的系统 [Klenze 等 2016]；

• - 最大流的单调理论被用作求解器组合的一部分，用于生成虚拟数据中心的资源分配方案 [Bayless 等 2020]。

每一个 Datalog 程序 都是一个单调理论 。给定一个纯 Datalog 程序（无否定）和一组可能的 EDB 事实，我们可以构造一个单调的 SMT 理论，其中包含由潜在输入事实参数化的 Datalog 程序输出元组。

考虑一个 Datalog 程序，它有 个可能的外延事实（extensional facts），依次编号为 ₁ 到 ₙ。假设 (c) 是一个可能的推导出的事实（derived fact）。我们构建一个 SMT 谓词符号 c，其类型为 Boolⁿ → Bool。

形式为 c(₁, ..., ₙ) 的谓词在该理论中为真，当且仅当在使用外延事实集合 {ᵢ | ᵢ = 1} 运行 Datalog 程序后，可以推导出事实 (c)。

此外，该谓词满足单调理论的要求：

直观上，ᵢ 允许我们开启或关闭外延事实（extensional facts），因此 SMT 谓词的单调性源于 Datalog 程序本身的单调性：如果在某个外延事实集合 下我们推导出了 (c)，那么在任何包含 的集合下也都能推导出 (c)。

这样一个基于 Datalog 的理论可以自然地融入单调理论框架中：

理论传播（Theory Propagation）

通过两次调用 Datalog 求解器，执行标准的过近似/欠近似方案：

1. 第一次调用计算在负扩展 下的程序，即计算 (⁻)，其中 ⁻ = {ᵢ | ⁻ʙ[ᵢ] = 1}。如果一个原子出现在 (⁻) 中，则它被 ⁻ʙ 中的正变量所蕴含。

2. 第二次调用计算在正扩展 下的程序，即计算 (⁺)，其中 ⁺ = {ᵢ | ⁺ʙ[ᵢ] = 1}。如果一个原子不在 (⁺) 中，则它的否定被 ⁺ʙ 中的负变量所蕴含。

借助溯源信息 ，我们可以比默认冲突解释机制做得更好，后者只是返回 ⁻ʙ 中的正谓词或 ⁺ʙ 中的负谓词。

1. 如果一个理论原子 c(₁, ..., ₙ) 成立，说明事实 (c) 必须出现在 (⁻) 中；提取其溯源信息 。设 是推导出 (c) 所涉及的输入事实集合。作为对 c(₁, ..., ₙ) 的解释，返回集合 {ᵢ | ᵢ ∈ }，这是 ⁻ʙ 中正变量的一个子集。

2. 如果一个理论原子 ¬c(₁, ..., ₙ) 成立，说明事实 (c) 不应出现在 (⁺) 中；使用 ProSynth 的 delta 调试技术 ，从集合 − ⁺ 中找出一个事实子集 ，只要启用这些事实中的某一个，就可以推导出 (c)。返回集合 {ᵢ | ᵢ ∈ } 作为对 ¬c(₁, ..., ₙ) 的解释；这将是 ⁺ʙ 中负变量的一个子集。

将任意 Datalog 程序（配备一组可能的输入事实）转换为一个单调 SMT 理论的能力，在 Datalog 综合之外也有多种潜在用途。

首先，它提供了一种轻量级且声明式的方法来构建可表达为 Datalog 程序的单调理论：只需编写 Datalog 程序，然后依赖我们的框架进行理论上高效的传播与冲突生成。例如，有限图可达性的单调理论可以用一个三规则的 Datalog 程序来表示。虽然这种实现方式肯定不如手写的 SMT 理论高效，但比起编写完整的理论或自定义传播器要节省大量工作。

其次，我们的框架提供了一种方法来求解涉及 Datalog 谓词的 SMT 公式。由于综合是单调理论的主要用途之一，我们推测基于 Datalog 的单调理论可用于那些部分问题以 Datalog 表达、部分问题以其他 SMT 理论表达的综合任务中，如下例所示：

示例 4.1

考虑一个任务：判断是否存在一个 API 调用序列会导致系统进入不良状态，例如敏感信息通过公共通道泄露出去。这是一个具有挑战性的问题，因为可能的序列数量是无限的。我们可以测试随机序列，但这不太可能找到有意义的结果；另一方面，像符号执行这样的更全面测试策略又难以扩展，因为每当执行器决定下一个调用哪个 API 时，路径数量会爆炸式增长。

相比之下，我们的方法将结合：

• Z3 和 CVC4 支持的 SMT 序列理论 ，以及

• 一个基于 Datalog 的单调理论，

来合成潜在有趣的 API 调用序列，之后再使用更精确的技术（如符号执行）进行验证。

作为我们单调理论的后端，我们将使用一种基于 Datalog 的分析方法，用于计算某个 API 调用序列是否可能导致私有信息流入公共接收点（可能是对 Livshits 和 Lam [2005] 提出的 Java 污点分析的一种扩展）。

该分析参数化于允许的 API 调用顺序；具体来说，它接受如下形式的事实作为输入：

• start( )

  （表示 可以作为序列中的第一个 API 调用），

• next( , )

  （表示对 的调用可以直接跟在对 的调用之后）。

作为输出，该分析会在给定允许的 API 调用顺序下，若违反了所需的安全属性，则生成一个 error 事实。

我们的单调 SMT 理论将这些事实暴露为 SMT 层级的布尔变量。

通过构建将 Datalog 事实与 SMT 序列理论中的约束条件连接起来的 SMT 断言，我们能够合成出有趣的 API 调用序列：这些序列根据我们的 Datalog 分析可能引发错误条件，并且也满足我们使用序列理论所施加的任何附加约束（例如匹配某个正则表达式）。

我们从序列理论中使用了谓词 seq.prefixof(, ) 和 seq.contains(, )。设 s 是一个 SMT 变量，它将被实例化为我们生成的调用序列。

• 对于每个 API 方法 ，我们断言：事实 start( ) 成立当且仅当 seq.prefixof("", s) 成立。

• 对于每对 API 方法 和 ，我们断言：事实 next( , ) 成立当且仅当 seq.contains(s, "") 成立。

• 最后，我们断言推导出的事实 error 成立。

如果这一组断言不可满足，那么我们知道不存在任何 API 调用序列会导致安全属性被违反；如果它是可满足的，我们可以提取 s 的一个模型并测试该调用序列。

此外，我们还可以使用序列理论中的其他操作符来引导搜索过程：

• 例如，要强制序列长度为 ，我们可以断言 seq.len(s) = ；

• 要限制序列中 出现在 之后的情况，我们可以使用 Z3 支持的正则表达式，并断言 ¬seq.in.re(s, ".*.*.*") 。

我们认为，原则上这些涉及 Datalog 谓词的 SMT 断言可以编码为 Formulog [Bembenek 等 2020] 程序——这是一种带有表示和推理 SMT 公式机制的 Datalog 变体。然而，这种方法在实践中不太可能表现良好（事实上，我们将“作为规则选择的综合”问题编码为 Formulog 程序时，无法扩展到除最小的 ProSynth 基准之外的任何情况）：

1. Formulog 执行的是穷举式的、基于饱和的推导过程，而不是由 SMT 提供的有指导的搜索；

2. 增量式 SMT 求解允许我们逐步添加新的断言（例如对我们期望解的细化），而无需从头开始重新求解，但 Formulog 不支持增量计算。

像 Formulog 一样，受约束的 Horn 子句 （CHC）求解提供了一种方法来求解 Horn 子句与 SMT 公式的混合形式 [Bjørner 等 2015；Grebenshchikov 等 2012；Gurfinkel 等 2015；Hoder 和 Bjørner 2012]。然而，CHC 求解器在它们支持的理论范围上通常较为有限，而且更根本的问题是：它们寻找的是通用的 SMT 模型，而我们需要在最小模型语义 下解释 Horn 子句，以与 Datalog 保持一致。

4.3 我们的实现

我们实现了该方法的两个版本：

• 一个是在 CVC4 的扩展版本中作为一个 自定义理论 实现；

• 另一个是在 Z3 上作为 用户传播器 （user propagator）实现。

这两个版本拥有基本相同的 API，实现也非常相似。它们都暴露了一个编码器类 （encoder class），构造时需要传入一个特定的求解器实例以及一个 Soufflé 程序的引用（该程序可以作为库动态链接）。⁴

用户将一个（已实例化的）Soufflé 元组传递给编码器；编码器返回一个对应于该元组的布尔类型的 SMT 变量。用户可以在任意包含这些布尔变量的 SMT 公式中进行断言；编码器的后端确保 SAT 核心计算出的任何模型在 Datalog 语义下都是可接受的，遵循上一节中描述的单调理论方法。

编码器使用 Datalog 的 why 和 why-not 溯源机制来生成冲突解释。

我们对 Raghothaman 等人 [2020] 提出的 delta-debugging 技术的实现遵循 ProSynth 中的算法实现，这与论文中描述的算法略有不同：它减少了 Datalog 的调用次数，但返回的 why-not 溯源信息精度较低。

我们的实现使用了若干启发式策略。

首先，我们使用了一个原始的真值维护系统 （truth maintenance system）[Doyle 1979；McAllester 1990]，用于缓存每个部分赋值在其正扩展和负扩展下传播出的理论原子的解释信息。

其次，给定一个部分赋值，可能会存在多个冲突需要报告。ProSynth 的实现会在每个指定的输出关系中报告最多 30 个 why 冲突和 1 个 why-not 冲突。而 Z3 的传播器 API 每次部分赋值只允许报告一个冲突；为了保持一致性，我们在 Z3 和 CVC4 的两个版本中都采用了相同的策略。

总体来说，我们尽量避免进行 Datalog 求值，并返回较小的冲突。

最后，一个重要的启发式策略是：我们应多积极地尝试发现冲突 。并非在每一个部分赋值上都必须检查冲突；相反，我们的实现会将布尔参数的赋值缓存起来，直到达到某个阈值后再进行处理（详见第 7 节）。

4.4 编码综合问题

我们构建了一个工具 MonoSynth ，它利用 Datalog 理论来解决“作为规则选择的 Datalog 综合”问题（见图 3）。

给定一个综合问题后，它以编程方式将候选规则的 Soufflé 程序（如第 3 节所述）作为共享库加载进来，并将示例输入载入该程序中。

通过使用理论接口，它将期望的和不期望的输出元组编码为 SMT 项并进行断言。同时，它也对 rule() 元组进行编码，但不对它们施加约束。

最后，它调用 SMT 求解器检查可满足性并构造模型；MonoSynth 输出与模型中为真的 rule() 对应的规则选择结果。

4.4.2 与先前方法的比较

MonoSynth 在多个关键方面有别于 ProSynth 。

首先，所有计算都在同一个操作系统进程中完成 。
ProSynth 使用一个 Python 进程来执行其逻辑和 SAT 求解器的工作；每次调用 Datalog 程序时都会启动一个新的独立进程。

其次，MonoSynth 利用了 Datalog 的单调性 ，能够在部分规则选择 （partial candidate rule selections）上主动报告冲突 。
而 ProSynth 只有在 SAT 求解器生成了一个完整的规则选择 之后才会发现冲突。

在部分规则选择上报告冲突本身就是一个潜在的优势，同时也使得 MonoSynth 使用 ProSynth 的 delta-debugging 技术生成 why-not 冲突的成本更低：
ProSynth 必须从完整规则选择中排除的所有规则中进行过滤，而 MonoSynth 只需从当前部分赋值中被标记为负的规则中进行过滤。

相关地，ProSynth 的实现可以一次报告多个冲突 ，而如第 4.3 节所述，MonoSynth 每次部分赋值只报告一个冲突 。

总体而言，MonoSynth 相比 ProSynth 实现了良好的加速效果（见第 7 节）。

• MonoSynth-Z3

  相比 ProSynth-Z3 平均实现了约 2 倍的加速 （最小 / 中位数 / 几何平均 / 最大值：0.03× / 2.07× / 1.83× / 21.94×）；

• MonoSynth-CVC4

  相比 ProSynth-CVC4 平均实现了接近一个数量级的加速（0.74× / 9.08× / 9.06× / 103.30×）。

5 放弃单调性：借鉴基于 SAT 的 ASP 思想

MonoSynth 利用了 Datalog 的单调性来求解包含 Datalog 谓词的 SMT 公式。在本节中，我们转而利用 Datalog 在答案集编程 （ASP）中的嵌入能力——这是一种非单调 的编程范式（见第 5.1 节）。

我们借鉴了一个现有的用于 ASP 的算法，展示了如何使用现成的 SAT 求解器来求解包含 Datalog 谓词的 SAT 公式（见第 5.2 节），并将其应用于综合问题（见第 5.3 节）。

5.1 背景知识：基于 SAT 的 ASP 求解

答案集编程 （Answer Set Programming, ASP）是一种用于解决某些类型搜索问题的逻辑编程范式 [Brewka 等 2011；Gelfond 和 Lifschitz 1988]。在表达力上，ASP 介于 Datalog 和 Prolog 之间：

• ASP 程序总是终止的（不像 Prolog），但能解决 NP 难问题（不像 Datalog，它属于 PTIME 类别 [Papadimitriou 1985；Vardi 1982]）。

尽管现代 ASP 系统支持丰富的附加特性，但在最简单的形式下，ASP 就是语法上的 Datalog，只不过在规则体中加入了“失败即否定”（negation-as-failure）的文字 not (t)。

否定文字的加入带来了语义上的困难（不再保证存在最小 Herbrand 模型），为此提出了多种解决方案，例如：

• 分层否定（stratified negation）[Apt 等 1988；Przymusinski 1988；Van Gelder 1989]，

• 完备语义（well-founded semantics）[Van Gelder 等 1991]，

• 以及稳定模型语义（stable model semantics）[Gelfond 和 Lifschitz 1988]，这是 ASP 的基础。

在稳定模型语义下，一个 ASP 问题可以有零个、一个或多个解，这些解被称为答案集 （answer sets）。一个答案集是一个受限的模型：模型中为真的每个原子都必须被解释，并且这种解释不能假设原子本身为真（见表 1）。

要判断一组基础原子集合 是否是程序 的一个答案集，步骤如下：

Datalog 可以嵌入到 ASP 中：
每一个 Datalog 程序，只要给定一个 EDB（外延数据库），就可以被解释为一个具有 唯一答案集 的 ASP 程序，该答案集对应于 EDB 与 IDB 的并集。

ASP 求解通常分为两个阶段：

1. 首先，使用专门的“实例化器”（grounder）对输入的 ASP 程序进行 实例化 （见第 5.1.1 节）；

2. 然后，使用基于 SAT 的技术来寻找该实例化程序的 稳定模型 。

在这里，我们借鉴了 ASSAT 算法 [Lin 和 Zhao 2004]，它使用现成的 SAT 求解器来计算答案集（见第 5.1.2 节）；我们在第 6 节中讨论其他替代方案。

5.1.1 实例化（Grounding）

大多数 ASP 求解过程的第一步是对源程序进行实例化 。我们并不需要生成精确的实例化程序，而只需要生成在稳定模型语义下等价的程序即可。

现代实例化器 [Calimeri 等 2017；Gebser 等 2011a] 使用半朴素求值 来进行部分求值，从而生成更小的实例化程序。

例如，Gringo [Gebser 等 2011a, 2007] 在示例 5.1 上生成的简化实例化程序如下：

尽管进行了优化，但基底化（grounding）仍然是解决某些ASP（Answer Set Programming，即答案集编程）问题的主要瓶颈。值得注意的是，基底化将一个一阶逻辑程序转换为命题逻辑程序，因为每个基底原子()都可以被视为一个命题变量。

5.1.2 ASSAT。ASSAT算法（Lin和Zhao，2004）使用现成的SAT求解器为基底程序计算答案集。由于程序是基底化的，以下我们将所有原子、视为命题原子。对于形式为 :- 1, . . . , 的规则，令ℎ()为，()为{1, . . . , }的集合或合取式Ó ，具体取决于上下文。

ASSAT的第一步是构建基底程序的Clark完备化（Clark 1977），将基底程序的原子编码为命题逻辑：对于基底程序中的每个基底原子，构建方程 ≡ Ô{() | ∈ , ℎ() = }。的Clark完备化是根据导出的所有此类方程的集合。

5.2 我们的实现

ASSAT 是一种用于求解 ASP（Answer Set Programming，答案集程序）问题的算法。我们的工具对其进行了改进，以求解包含 Datalog 谓词 （更一般地说，是 ASP 谓词）的 SAT/SMT 公式。

我们在 Python 中实现了两个版本：一个使用 Z3 的绑定 ，另一个使用 CVC4 的绑定 。这两个版本都对外暴露了一个“编码器”（encoder）接口，该编码器封装了一个 SMT 求解器实例，并根据一个 Datalog 程序和一组可能的输入元组进行构造。

编码器使用 Gringo [Gebser et al. 2011a, 2007] 来对程序进行实例化（即“接地”）。它直接对规则进行编码，同时将每一个可能的输入元组 p(c)编码为一个 ASP 的选择规则（choice rule）：{p(c)}。

这个选择规则是以下两条规则的简写形式：

• p(c) :- not q.
• q :- not p(c).

其中，原子 q 是程序中其他地方不出现的辅助原子，表示选择是否不在答案集中包含 p(c)。

从 Gringo 生成的实例化程序出发，我们的工具构建其 Clark 补全（completion） 并将其断言给 SAT 求解器。

客户端可以向编码器传入一个 Datalog 事实，并获得一个与之对应的布尔 SAT 变量，该变量可以在任意 SAT 公式中使用。

编码器提供了一个方法，用于检查底层求解器状态在稳定模型语义下的可满足性；它按照 ASSAT 算法的方式工作：

1. 使用 SAT 求解器迭代地生成一个模型；

2. 使用 Datalog 求解器对其进行验证；

3. 如有必要，则添加循环公式（loop formulas）来排除非稳定模型。

出于方便考虑，我们的实现在这里使用 Gringo 作为 Datalog 求解器；它也可以同样使用 Soufflé 。它只报告一个循环公式：即针对 SAT 模型中那些地原子（ground atoms）在正向依赖图中构成的强连通分量（SCC）中的最小者——这些原子包含在 SAT 模型中，但被排除在最小模型之外。

5.3 编码合成

我们的工具 LoopSynth 使用上述系统来解决 Datalog 合成中的规则选择问题 （如图5所示）。

给定一个基准问题，它首先将 Soufflé 程序（包含候选规则）解析为抽象语法树（AST）表示，然后用示例输入对其进行扩充，并将结果连同规则元组集合一起传递给基于 ASSAT 的编码器。

接着，该工具使用编码器对问题规范中指定的每一个期望元组（desired tuple）和非期望元组（undesired tuple）进行编码，适当地断言每个返回的布尔 SAT 变量（或其否定）。

然后，向编码器查询一个模型；如果某个规则对应的 SAT 变量在该模型中为真，则认为该规则被选中。

5.3.2 与先前方法的比较

LoopSynth 的方法在几个方面不同于之前的方法。首先，SAT 求解器确实能看到候选规则 ，因为这些规则作为断言给求解器的 Clark 补全的一部分进行了编码。

其次，它调用 Datalog 引擎的频率更低：每个 SAT 调用只调用一次 Datalog 。而在 ProSynth 或 MonoSynth 中，一个 SAT 赋值可能导致多次 Datalog 调用 ，用于生成出处（provenance）以构建冲突信息。

与 MonoSynth 不同的是，LoopSynth 不是增量式的 ：SAT 求解器在获得反馈之前会一次性猜测完整的规则选择。

LoopSynth 在基准测试套件上的性能表现参差不齐（第7节）。CVC4 版本相较于 ProSynth-CVC4 实现了显著的加速（最小 / 中位数 / 几何平均 / 最大加速比：0.00× / 6.61× / 3.14× / 83.87×），但落后于 MonoSynth-CVC4（0.00× / 0.34× / 0.35× / 13.81×）；在 40 个基准测试中，LoopSynth-CVC4 在所有基于 CVC4 的工具中拥有最快的平均运行时间 ，其中有 11 个测试表现最佳。

然而，LoopSynth-Z3 相较于 ProSynth-Z3（0.00× / 0.19× / 0.24× / 25.67×）和 MonoSynth-Z3（0.00× / 0.10× / 0.13× / 7.71×）都表现较差。即便如此，仍有一些基准测试中，LoopSynth-Z3 的平均速度快于这两个工具 。

6 只需一个音符就能命名那首曲子：在 ASP 中的直接编码

现有的方法总是至少对某个系统进行多次调用 ：

• ProSynth

  对 Soufflé 和 SMT 求解器进行了 多次调用 （见第3节）；

• 单调性理论方法

  只对 SMT 求解器进行 一次调用 ，但对 Soufflé 进行了 多次调用 （见第4节）；

• 借鉴基于 SAT 的 ASP 方法的思想，得到了一种对 Datalog 调用次数大大减少、但仍需要对 SAT 求解器进行 多次调用 的方法（见第5节）。

如果我们能够直接在 ASP 中对问题进行编码 ，就可以一次性完成求解：只需进行一次实例化（grounding）调用（相当于 Datalog 的求值过程），以及一次ASP 求解器的调用 即可。

6.1 编码合成

我们将数据目录合成表述为一个ASP程序。我们对规则选择和最小化的编码是ASP程序合成工具ASPAL [Corapi et al. 2011] 用于实例化骨架ASP规则的编码的专门化版本，修改为使用辅助关系来编码输出示例。

接着，我们添加硬性约束（hard constraints）来限制合成程序的输出（见图6(a,b)）。

一个硬性约束是一个 无头规则（headless rule） ；任何使该规则体为真的答案集都会被拒绝。

约束 (C+) 要求所有正例都必须被推导出来，
而约束 (C−) 确保没有任何负例被推导出来。

这些硬性约束共同作用，迫使所选规则符合问题规范。

与 LoopSynth 类似，我们可以使用 ASP 的选择规则（choice rules）直接对规则选择进行编码（见图6(c)）：
rule(n) 可以出现在答案集中，也可以不出现。

实际上，ASP 求解器会自行选择规则。
因此，计算出的答案集就回答了我们的 Datalog 合成问题：
当且仅当 rule(n) 出现在答案集中时，规则 n 应被包含在合成的 Datalog 程序中 。

6.1.4 与先前方法的比较

ASPSynth （见图8）只进行一次“Datalog”调用（实例化）和一次“SAT”调用（ASP 求解） ，这与之前的方法不同。

它在表达能力上不如 MonoSynth 和 LoopSynth ，因为后两者可以求解包含 Datalog 谓词的任意 SMT 公式。

然而，现代 ASP 求解器使得以下两点变得非常容易：
(a) 避免显式枚举所有非期望元组 （这在 MonoSynth 和 LoopSynth 中是必需的）；
(b) 对解的最小化进行编码 （即寻找最简规则集）。

与其他工具相比，ASPSynth 将整个合成问题 ——包括候选规则和规范要求——都统一编码为一个整体形式 ，可以一次性求解。这种方式允许在选择候选规则与根据规范检查这些选择的后果之间进行增量式的交互 。

6.2 实现

我们以两种系统实现了这种直接编码方法：ASPSynth-Clingo 和 ASPSynth-WASP ，
它们分别使用了 ASP 求解器 Clingo v5.4.0 [Gebser 等人，2011b] 和 WASP v2.0 [Alviano 等人，2013]。
这两个系统都使用了实例化工具 Gringo v5.4.0 [Gebser 等人，2011a, 2007]。

Clingo 在内部运行 Gringo：从技术上讲，“Clingo”指的是由 Gringo 和求解器 Clasp [Gebser 等人，2012] 组成的完整系统 。
对于 ASPSynth-WASP ，我们则是单独运行 Gringo ，然后将结果通过管道传递给 WASP。

无论是 Clingo 还是 WASP，它们都是“原生的（native） ” ASP 求解器：
它们是专门设计的求解器，使用了类似 SAT 的技术，但不会将任务委派给外部的 SAT 求解器 。

直接使用 ASP 编码的方法在基准测试套件中整体表现最佳。
WASP 相较于 ProSynth-Z3 有大约 3 倍的平均加速比 （最小 / 中位数 / 几何平均 / 最大加速比：0.03× / 2.63× / 3.62× / 186.10×），
相较于 MonoSynth-Z3 有大约 2 倍的平均加速比 （0.07× / 1.64× / 1.98× / 247.98×）。

而 Clingo 的表现更优：
相较于 ProSynth-Z3 实现了大约 9 倍的平均加速比 （1.16× / 7.50× / 9.47× / 372.19×），
相较于 MonoSynth-Z3 实现了大约 5 倍的平均加速比 （0.33× / 3.88× / 5.17× / 513.80×）。

下一节将给出详细的评估结果。

7评估

我们通过 ProSynth 基准测试套件 对所开发的方法进行了实证评估。我们的基准测试结果报告了十次运行的平均值；实验在一个空闲的 Ubuntu 20.04 AWS 服务器上进行，该服务器配有 32 个 vCPU（主频为 3.1 GHz）、128 GiB 内存和 600 GiB SSD 存储空间。我们使用的是 Z3 v4.8.15 和 CVC4 v1.8。每个单独的基准测试在运行超过十分钟（600 秒）后将超时。所有基准测试和实验脚本都包含在论文的附加工件中 [Bembenek 等人, 2022]。

我们将 ProSynth 作为基线进行比较。我们对原始论文附加工件中的 ProSynth 版本进行了轻微修改，以记录并输出额外的统计信息，并对 SMT 符号名称进行随机化处理。SMT 符号名称的选择可能会对求解器性能产生显著（且任意的）影响，我们不希望 ProSynth 因为这些本质上是随意的求解器相关因素而受到不公平的优势或劣势影响。（我们在基于 SMT 的其他工具中也对符号名称进行了类似的随机化处理。）

此外，我们还创建了一个使用 CVC4 而非 Z3 的 ProSynth 替代版本；这涉及到从 Z3 的 Python 绑定迁移到 CVC4 的一些语法上的小改动。我们修改后的 ProSynth-Z3 版本与原始版本性能相当，并明显优于 CVC4 版本（最小 / 中位数 / 几何平均 / 最大加速比：0.68× / 3.97× / 5.27× / 174.02×）。

每种方法都有其表现良好的用例，但直接的 ASP 编码方法 —— 尤其是 ASPSynth-Clingo —— 在整个基准测试套件中表现最佳（见图9；表7）。ASP 编码整体表现出较快的性能。

其中，ASPSynth-Clingo 表现最优 ：它没有明显的性能较差的异常情况，在每一个基准测试中都能在不到一秒的时间内返回结果 ；即使当它不是最快的工具时，它也仅比最快者慢 0.02 秒。

接下来的内容中，我们将描述基准测试套件（第 7.1 节），并对每种方法的表现进行详细分析（第 7.2、7.3 和 7.4 节），最后将在更广泛的背景下评估 ASPSynth-Clingo（第 7.5 节）。

7.1 基准测试套件

我们使用的是 ProSynth 的基准测试套件 ，它源自为 ALPS [Si 等人, 2018] 开发的测试集，并随后被 DiffLog [Si 等人, 2019] 所采用。

该套件包含不同输出关系的预期输出元组文件，以及一个 Soufflé 程序，其中包含了由 ALPS 生成的候选规则（每条规则都扩展了一个 rule(n) 前提）。

Soufflé 程序会被编译成可执行文件（用于 ProSynth）或共享库（用于 MonoSynth）。
对于规范中的每一个输出关系，我们还生成其补关系中的元组集合（MonoSynth 和 LoopSynth 要求显式枚举所有不期望的元组）。

该测试套件共包含 40 个基准测试 ，其中包括：

• 14 个知识发现任务
• 11 个程序分析任务
• 15 个关系代数任务

规则集的大小从 5 条规则到 688 条规则 不等。
有关完整描述，请参见 ProSynth 论文中的表1和表2 [Raghothaman 等人, 2020]。

7.2 MonoSynth

MonoSynth-Z3 相较于 ProSynth-Z3 实现了大约 2 倍的平均加速比 （最小 / 中位数 / 几何平均 / 最大加速比：0.03× / 2.07× / 1.83× / 21.94×），
而 MonoSynth-CVC4 相较于 ProSynth-CVC4 实现了接近一个数量级的平均加速比 （0.74× / 9.08× / 9.06× / 103.30×）。

虽然 CVC4 的结果显示出明显的改进，但 Z3 的结果则更为模糊：
MonoSynth-Z3 的性能在不同基准测试之间差异较大 ，而且大多数对 ProSynth-Z3 的加速（27 项中有 20 项）发生在那些 ProSynth-Z3 已经很快的任务上（即在不到一秒内完成的任务）。

我们怀疑是我们在选择冲突时使用的启发式方法可能与 Z3 的搜索策略产生了不良交互：
ProSynth-Z3 通常进行数十次 Datalog 调用 ，而 MonoSynth-Z3 则进行数百次调用 。
在那些 ProSynth-Z3 更快的任务（如 downcast、polysite 和 sql-10）上，这种大量调用尤其有害，因为在这些任务中每次 Datalog 调用的平均耗时更长。

ProSynth-CVC4 和 MonoSynth-CVC4 的 Datalog 调用次数与 MonoSynth-Z3 大致相同。

四种工具的大部分时间都花在了 Datalog 求解 上，而在 SAT 求解 上几乎没有花费时间。这并不令人意外，因为无论是 ProSynth 还是 MonoSynth，一般都需要在每个冲突中调用 Datalog 求解器多次（需要多次 Datalog 调用来计算“为何未推导出”的出处信息），而传递给 SAT 求解器的阻塞约束并不特别复杂。

尽管两种 MonoSynth 版本相对于各自的基线（即 ProSynth-Z3 和 ProSynth-CVC4）表现出不同的性能提升，但从整体来看，它们彼此之间的平均表现是相当的。

正如第 4.3 节所指出的那样，MonoSynth 并不需要在每个部分赋值上都检查冲突 。
在实验中，我们会在检查冲突前先缓存五个布尔参数的赋值。
缓存越小，报告冲突的速度就越快，但也会导致更多的 Datalog 调用（尽管这些调用在同一操作系统进程中进行，但仍代价不低）。
在我们的实验中，设置缓存大小为 5 似乎达到了一个合理的平衡。
然而，在所有基准测试中它远非最优，我们预计如果采用更复杂的缓冲启发式方法（例如根据问题特征动态调整缓存大小），可能会带来显著的性能提升。

7.3 LoopSynth

LoopSynth 的表现因所使用的求解器不同而有所差异，结果呈现出混合状态。

在使用 CVC4 的情况下，LoopSynth 的整体表现较为积极：它相比 ProSynth 实现了显著的平均加速（最小 / 中位数 / 几何平均 / 最大加速比：0.00× / 6.61× / 3.14× / 83.87×），但落后于 MonoSynth（0.00× / 0.34× / 0.35× / 13.81×）。总体而言，在所有基于 CVC4 的工具中，LoopSynth-CVC4 在 40 个基准测试中的 11 个上拥有最快的平均运行时间。

而在使用 Z3 的情况下，LoopSynth 的表现则相对较差，与 ProSynth（0.00× / 0.19× / 0.24× / 25.67×）和 MonoSynth（0.00× / 0.10× / 0.13× / 7.71×）相比均处于劣势。即便如此，LoopSynth-Z3 在 40 个基准测试中的 3 个上仍然是所有 Z3 工具中最快的，并且在这两个工具上分别实现了最高达 26 倍 和 8 倍 的加速。

LoopSynth 方法最大的问题或许是其不可靠性 ：

• Z3 版本在 21 次测试中出现超时 （涉及 3 个基准测试），

• CVC4 版本在 35 次测试中出现超时 （涉及 4 个基准测试）。在这些情况下，算法未能生成足够的循环公式来迫使求解器在合理时间内收敛到一个稳定模型。

与 ProSynth 和 MonoSynth 相比，LoopSynth 将时间分布从 Datalog 求解 转移到了 SMT 求解 上。

排除超时结果以及耗时小于一秒的测试后发现：

• LoopSynth-Z3

  在 Datalog 求解上花费的时间比例大致与其在 SMT 求解上的比例相当：

• • Datalog：0.10% / 2.47% / 平均 3.97% / 最高 15.32%

  • SMT：1.18% / 1.83% / 平均 2.33% / 最高 6.18%

• LoopSynth-CVC4

  则在 SMT 求解上花费了更多时间：

• • SMT：7.76% / 13.21% / 平均 16.15% / 最高 31.81%

  • Datalog：0.27% / 2.90% / 平均 9.80% / 最高 28.96%

其余大部分时间用于编码 Clark 补全 和 构造循环公式 。

在 40 个基准测试中，有 15 个是“紧致”（tight）的，因此不需要任何循环公式。对于其余未超时的测试：

• LoopSynth-Z3

  和 LoopSynth-CVC4 大多数情况下只需生成少量循环公式，但在某些不良情况下可生成数百甚至上千个：

• • LoopSynth-Z3：最少 / 中位数 / 平均 / 最多 = 0.00 / 2.00 / 28.99 / 442.30

  • LoopSynth-CVC4：0.00 / 1.00 / 374.51 / 7241.00

每个循环公式都会触发一次 Datalog 调用；由于 Datalog 调用次数相对较少，这在一定程度上缓解了 LoopSynth 使用 Gringo 解释执行 Datalog 程序（而非像 ProSynth 和 MonoSynth 那样调用 Soufflé 编译后的高效程序）所带来的性能劣势。

7.4 ASPSynth

直接使用 ASP 编码的方法是基准测试套件上最有效的解决方案。

ASPSynth-Clingo 在每次测试中都在一秒内完成任务 ，它在 40 个基准测试中的 26 个 上平均表现最快，并且相比 ProSynth-Z3 实现了大约 9 倍的平均加速比 （最小 / 中位数 / 几何平均 / 最大加速比：1.16× / 7.50× / 9.47× / 372.19×）。

ASPSynth-WASP 的表现也很稳健，相比 ProSynth-Z3 实现了大约 3 倍的平均加速比 （0.03× / 2.63× / 3.62× / 186.10×）。然而，它在 sql-15 基准测试上持续超时 。有趣的是，LoopSynth 的两个版本也出现了同样的问题：可能该基准测试中的循环结构对某些基于 ASP 的方法来说难以处理。

是什么让直接面向 ASP 的工具 比其他方法更有效？一个不应忽视的因素是：Clingo 和 WASP 是经过多年优化的高度成熟、工程化的工具 ，而其他方法则是临时构建、尚未高度优化的实现。

Clingo 和 WASP 避免了其他实现所面临的一些开销，例如：

• 多个操作系统进程之间的切换，

• 或不同系统之间（如 Z3 与 Soufflé）在内存中的表示转换。

同样地，ASPSynth 不需要多次执行 Horn 子句求值： 它只需进行一次程序实例化（grounding），而其他工具则要运行显式的 Datalog 求值过程来检查每个提议解是否满足最小模型语义。

此外，ASP 求解器内部将 Horn 子句求解与 SAT 搜索紧密结合 ，使其能更有效地探索解空间。

为了理解这一点，我们可以观察每种方法向 SAT 求解器中添加了多少公式以引导其找到解；一般来说，这个数字越高，说明 SAT 求解器探索了越多无用的搜索空间。

为简洁起见，我们将这些公式统称为“冲突”（conflicts）；它们的具体定义因工具而异，因此比较时不能完全等同（例如，LoopSynth 生成的一个循环公式可能转化为 SAT 求解器中的多个子句；我们对 ProSynth 所遇到的冲突数量进行了低估，因为一次 CEGIS 迭代可能涉及多个冲突）。

尽管如此，这些数据仍有助于我们了解不同算法的性能差异（见表3）：

• ProSynth 和 MonoSynth 方法

  遇到的冲突数量大致相同；

• LoopSynth 方法

  平均遇到一或更少的冲突（中位数），但在不良情况下也可能遇到大量冲突；

• 直接 ASP 编码方法

  平均遇到的冲突最少，其中位数为 零冲突 。

不仅如此，它们在构造冲突解释时也更加高效，因为——不像 ProSynth 或 MonoSynth——它们不需要调用 Datalog 求解器来生成出处信息。

因此，直接的 ASP 编码方法拥有一种“双赢”的组合优势：遇到的冲突更少，且计算这些冲突的成本更低 。

7.5 更广阔的视角：ASPSynth-Clingo 有多高效？

我们工作的一个贡献是对基于求解器的 Datalog 合成（作为规则选择问题）算法设计空间进行探索。然而，既然我们已经找到了一个占主导地位的解决方案——ASPSynth-Clingo ，我们就可能会好奇它与其他可能的技术相比表现如何。

本节进一步评估 ASPSynth-Clingo 在解决 Datalog 合成（作为规则选择）问题上的有效性。总体而言，我们发现它在 ProSynth 基准测试套件上表现非常出色，并且相较于基于候选规则集的其他方法具有良好的扩展性。我们还提出了一些克服当前局限性的建议。

7.5.1 参与比较的工具

在程序合成中，解的质量 至关重要。

我们评估了两个版本的 ASPSynth-Clingo ：

• 原始版本

  （不进行解最小化）

• ASPSynth-Clingo-MinPremise

  （最小化解中的前提数量，见第6.1.2节）

我们还将它与 GenSynth [Mendelson et al. 2021] 、ILASP2 [Law et al. 2015] 的编码版本 和 ProSynth 进行了比较。

GenSynth 是一种 Datalog 合成工具，它使用遗传编程算法生成候选规则，而不是从预定义的规则集中选择。与其它从候选规则集中选择的方法相比，这种方法在某些情况下是劣势（当候选规则集较小时），在另一些情况下则是优势（当候选规则集很大或难以过滤时）。

GenSynth 的论文报告了其相对于某个使用 Soufflé 解释模式的 ProSynth 版本的加速效果（通常 ProSynth 是与 Soufflé 编译出的可执行文件交互的）；但 GenSynth 的评估并未包含与使用编译后 Soufflé 程序的 ProSynth 的对比。GenSynth 自身也是使用 Soufflé 的解释模式，并尝试最小化解。

ILASP2 [Law et al. 2015] 使用元级方法将 ASP 程序合成建模为 ASP 程序，并将其提交给 Clingo 求解。由于 Datalog 是 ASP 的一个片段，我们可以自然地在 ILASP2 中对 Datalog 合成进行编码，类似于第6节中的直接 ASP 编码方式（ILASP 允许显式枚举候选规则，因此我们省略了 rule(n) 原子和选择规则）。

在配置 ILASP2 时，我们将合成程序中字面量数目的上限设为 30，这是默认值的两倍（能工作的最小值是 28）。与 ASPSynth 相比，ILASP2 生成了更复杂的 ASP 程序（涉及元级机制），并调用了两次 Clingo（而不是一次）。ILASP2 也最小化了解中的前提数量。

作为基线，我们使用了一个轻微修改后的 Raghothaman 等人 [2020] 的 ProSynth 实现版本（关闭日志记录并收集额外统计数据）。原始的 ProSynth 论文没有报告 Soufflé 编译候选规则集所需的时间（编译每组规则只进行一次，生成的可执行文件被多次调用）。为了专注于基于求解器的方法部分，在前一节中我们忽略了 ProSynth 和 MonoSynth 的编译时间。但在本节中，我们分别报告了 ProSynth 包含和不包含编译时间的运行时间，因为如果要从头开始使用 ProSynth 来合成程序，就必须编译候选规则。

7.5.2 测试基准

我们使用了两组基准测试：

第一组是第7.1节中讨论的 40 个 ProSynth 基准测试 。

第二组是一组扩展性基准测试 ，用于评估候选规则数量和规范大小的变化对性能的影响。每个测试都试图合成一个用于计算强连通分量（SCC）的程序。

对于候选规则，我们考虑了三种情况：

• 100 条规则

• 500 条规则

• 1000 条规则（取自 ProSynth 论文 [Raghothaman et al. 2020] 中的扩展实验）

对于规范大小，我们考虑了三类 EDB（外延数据库）：

• 10 个元组（scc-1x）

• 100 个元组（scc-10x）

• 1000 个元组（scc-100x）（取自 GenSynth 论文 [Mendelson et al. 2021] 中的扩展实验）

我们考虑了所有规则集大小与规范大小的组合。

7.5.3 实验结果

在 ProSynth 基准测试套件上，ASPSynth-Clingo 平均明显快于其他方法 （见图10(a)）。

与不计 Soufflé 编译时间的 ProSynth 相比，它显著更快（最小 / 中位数 / 几何平均 / 最大加速比：0.65× / 7.58× / 9.33× / 828.86×），并且比 GenSynth 快几个数量级（6.88× / 140.58× / 200.16× / 20000×）。

ILASP2 的编码也明显快于 ProSynth（0.21× / 2.82× / 3.48× / 236.14×）和 GenSynth（4.29× / 45.01× / 74.57× / 6593.40×），这进一步表明 ASP 非常适合这类 Datalog 合成任务。

ASPSynth-Clingo 比 ILASP2 更快（1.31× / 2.89× / 2.68× / 5.07×）。

前提最小化对 ASPSynth-Clingo 的性能影响不大（相对于 -MinPremise 的加速比：中位数 1.00×，几何平均 1.06×）。

GenSynth 产生的输出是最小的 （无论是按规则还是前提数量衡量）。GenSynth 的解在前提数量上适度少于 ASPSynth-Clingo-MinPremise 和 ILASP2（中位数 1.00×，几何平均 0.86×），大幅少于 ASPSynth-Clingo（中位数 0.67×，几何平均 0.54×）和 ProSynth（中位数 0.67×，几何平均 0.56×）。

当我们改变候选规则数量和输入/输出示例数量时，GenSynth 的扩展性最好 （见图10(b)）。它在各种配置下表现相对稳定（除了 scc-1x 超时），并在除最小配置外的所有配置上优于 ProSynth。

基于 ASP 的方法在仅扩展一个维度时扩展性良好，但在同时扩展两个维度时落后于 GenSynth。最大的配置突出了 ASPSynth-Clingo、ASPSynth-Clingo-minpremise 和 ILASP2 之间的性能差异。

尽管 GenSynth 扩展性较好，但它在基准测试套件上的整体速度最慢（见图10(a)）。

8 讨论

我们讨论 ASPSynth 的局限性（第 8.1 节），
基于求解器的算法之间的比较难点（第 8.2 节），
对规则选择问题的批评（第 8.3 节），
以及对该问题的更广泛视角（第 8.4 节）。

8.1 ASPSynth 的局限性

尽管 ASPSynth 的表现优于其他解决方案，但它仍然存在几个局限性。

实例化（grounding） 通常是基于 ASP 的逻辑程序合成工具的主要瓶颈 [Athakravi 等人, 2013；Cropper 和 Morel, 2021]。

ASPSynth 的性能会随着规范（specification）规模的增大而下降，
这是由于地规则（ground rules）数量发生了组合爆炸；
如果 ASP 求解器能在惰性实例化（lazy grounding）与 SAT 技术之间更好地结合 [Weinzierl, 2017]，
ASPSynth 将从中受益。

ASPSynth 可以被扩展以合成包含**分层否定（stratified negation）**的程序 [Apt 等人, 1988；Przymusinski, 1988；Van Gelder, 1989]，这是一种常见的 Datalog 对否定的处理方式，它禁止谓词通过自身（无论是直接还是间接）的否定来定义自己。

合成带有否定的程序本身并不是一个问题（因为我们的编码可以合成一般的 ASP 程序）。

为了确保我们只合成分层程序 ，我们可以添加一些 ASP 规则来定义谓词之间的否定依赖关系 </...