From SMT to ASP: Solver-Based Approaches to Solving

Datalog Synthesis-as-Rule-Selection Problems

從SMT到ASP：基于求解器的Datalog規(guī)則選擇合成方法

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

給定一組候選 Datalog 規(guī)則，Datalog 綜合問(wèn)題（作為規(guī)則選擇的問(wèn)題）會(huì)選擇其中的一個(gè)子集，以滿足某種規(guī)范（例如輸入-輸出示例）。在以往基于反例引導(dǎo)歸納綜合（counterexample-guided inductive synthesis）工作的基礎(chǔ)上，我們提出了三種基于求解器的方法來(lái)解決 Datalog 規(guī)則選擇式綜合問(wèn)題。我們的兩種方法相較于現(xiàn)有方法具有一些優(yōu)勢(shì)，并可以更廣泛地用于求解包含 Datalog 謂詞的任意 SMT 公式；第三種方法則是將其編碼為標(biāo)準(zhǔn)、現(xiàn)成可用的答案集編程（ASP），與當(dāng)前最先進(jìn)的方法相比，在合成高質(zhì)量程序的同時(shí)實(shí)現(xiàn)了顯著的速度提升（幾何平均約 9 倍）。

我們的解決方案演進(jìn)過(guò)程探索了 SAT/SMT 與 Datalog 之間的交互空間，并指出 ASP 是處理和推理 Datalog 的一種有前景的工具。在此過(guò)程中，我們將 Datalog 程序識(shí)別為單調(diào) SMT 理論，這類理論在 SMT 中具有特別高效的交互性能；我們?yōu)榱餍械?SMT 求解器開(kāi)發(fā)的插件使其能夠?qū)⑷我?Datalog 程序作為自定義單調(diào)理論輕松加載到 SMT 求解器中。最后，我們使用多種底層求解器對(duì)我們的方法進(jìn)行了評(píng)估，從而提供了比當(dāng)前最先進(jìn)方法更為全面且細(xì)致的對(duì)比分析。

CCS 概念：
? 軟件及其工程 → 自動(dòng)編程；約束與邏輯語(yǔ)言；
? 信息系統(tǒng) → 關(guān)系數(shù)據(jù)庫(kù)查詢語(yǔ)言；
? 計(jì)算方法 → 邏輯編程與答案集編程。

附加關(guān)鍵詞和短語(yǔ)：程序綜合、Datalog、歸納邏輯編程、可滿足性。

ACM 引用格式：
Aaron Bembenek, Michael Greenberg 和 Stephen Chong. 2023. 從 SMT 到 ASP：基于求解器的 Datalog 規(guī)則選擇式綜合方法。《ACM 程序設(shè)計(jì)語(yǔ)言進(jìn)展》7, POPL, 文章 7 (2023 年 1 月), 33 頁(yè)。https://doi.org/10.1145/3571200

1 引言

Datalog 是一種簡(jiǎn)單但出人意料地有用的邏輯編程語(yǔ)言。一個(gè) Datalog 程序由一組推理規(guī)則組成，其執(zhí)行相當(dāng)于將這些規(guī)則運(yùn)行至固定點(diǎn)（fixed point），從而對(duì)初始數(shù)據(jù)以及任何推導(dǎo)出的數(shù)據(jù)進(jìn)行所有可能的推理。

盡管 Datalog 非常簡(jiǎn)單（或者正因如此），它在多個(gè)領(lǐng)域中得到了廣泛應(yīng)用，包括程序分析 [Bravenboer 和 Smaragdakis 2009；Reps 1995；Scholz 等 2016；Whaley 和 Lam 2004]、網(wǎng)絡(luò) [Loo 等 2006；Ryzhyk 和 Budiu 2019]、分布式系統(tǒng) [Alvaro 等 2010a,b] 以及訪問(wèn)控制 [Dougherty 等 2006；Li 和 Mitchell 2003]。

隨著人們對(duì) Datalog 的興趣日益增長(zhǎng)，對(duì)于 Datalog 程序綜合（program synthesis）的興趣也隨之增加。在這一任務(wù)中，目標(biāo)是合成一個(gè) Datalog 程序——即一組推理規(guī)則——以滿足某種規(guī)范（specification），例如輸入-輸出示例。

一種流行策略包含兩個(gè)步驟：首先生成一組候選 Datalog 規(guī)則；其次選擇其中的一個(gè)子集，使其滿足給定的規(guī)范。為了解決第二部分問(wèn)題（稱為“作為規(guī)則選擇的綜合”問(wèn)題），已有多種技術(shù)被提出，包括基于委員會(huì)投票查詢（query-by-committee）驅(qū)動(dòng)的雙向搜索 [Si 等 2018]、數(shù)值松弛方法 [Si 等 2019]，以及反例引導(dǎo)歸納綜合（CEGIS）[Raghothaman 等 2020]。這些技術(shù)已在多個(gè)領(lǐng)域的 Datalog 綜合問(wèn)題上取得了穩(wěn)步進(jìn)展，包括知識(shí)發(fā)現(xiàn)、程序分析和關(guān)系代數(shù)等。

當(dāng)前最先進(jìn)的解決方案是 ProSynth [Raghothaman 等 2020]。它使用了 CEGIS [Solar-Lezama 等 2006] 方法，其中 SAT 求解器提出一組規(guī)則的選擇，然后使用 Datalog 求解器來(lái)測(cè)試該選擇是否符合規(guī)范。Datalog 的溯源信息用于向 SAT 求解器添加阻止約束，以引導(dǎo)其找到滿足條件的選擇。

本文介紹了一系列工具，它們構(gòu)建在 ProSynth 基礎(chǔ)之上，用于解決“作為規(guī)則選擇的綜合”問(wèn)題。每種工具探索了 SAT 求解與 Horn 子句求值（Datalog 求值/尋找阻止子句）之間的不同平衡方式；不同的平衡方式影響了 SAT 求解器在指數(shù)級(jí)大的可能解空間中有效探索的能力。最終提出的工具相比 ProSynth 實(shí)現(xiàn)了顯著的速度提升（幾何平均約 9 倍），同時(shí)能夠生成更高質(zhì)量的規(guī)則選擇。

MonoSynth

該工具基于以下觀察：每一個(gè) Datalog 程序都可以構(gòu)成一個(gè)單調(diào) SMT 理論的基礎(chǔ)。也就是說(shuō)，可以將任意 Datalog 程序轉(zhuǎn)化為一個(gè)（理論上）高效的 SMT 理論。從實(shí)踐角度看，它是 ProSynth 的一個(gè)更緊密集成于 SMT 求解器中的版本：像 ProSynth 一樣，它使用 Datalog 求解器測(cè)試規(guī)則選擇，并利用 Datalog 溯源生成沖突；但與 ProSynth 不同的是，它能為 SAT 求解器提供增量反饋，并剪枝不好的部分規(guī)則選擇。此外，它提供了一種通用方法，可用于求解涉及 Datalog 謂詞的 SMT 公式，而不僅限于 Datalog 程序綜合。

LoopSynth

受答案集編程（ASP）算法的啟發(fā)，該工具采用了一種截然不同的方法來(lái)整合 SAT 求解與 Horn 子句求值。在 ProSynth 和 MonoSynth 中，SAT 求解器從未看到候選規(guī)則；而在本方法中，候選規(guī)則的實(shí)例化版本（無(wú)變量）會(huì)被傳遞給 SAT 求解器。這為 SAT 求解器提供了更多信息，有助于其指導(dǎo)滿足賦值的搜索。Datalog 求解器用于確認(rèn) SAT 模型確實(shí)解決了問(wèn)題；如果沒(méi)有，則生成循環(huán)公式并加入 SAT 求解器中。與 MonoSynth 類似，LoopSynth 也可以廣泛用于求解涉及 Datalog 謂詞的 SMT 公式，而不僅限于 Datalog 程序綜合。

ASPSynth

比 LoopSynth 更進(jìn)一步，該工具直接將 Datalog “作為規(guī)則選擇的綜合”問(wèn)題編碼為 ASP 形式。概念上，我們使用的 ASP 求解器結(jié)合了 Horn 子句求值與 SAT 求解，與其他工具類似。然而，通過(guò)在一個(gè)統(tǒng)一的搜索過(guò)程中緊密集成這兩種范式，ASP 能夠更有效地探索解空間。

我們?cè)?ProSynth 基準(zhǔn)套件上對(duì)四種工具進(jìn)行了細(xì)致的評(píng)估。為了排除 SAT 求解器內(nèi)部機(jī)制帶來(lái)的性能偏差，我們分別基于 Z3 [Moura 和 Bj?rner 2008] 和 CVC4 [Barrett 等 2011] 構(gòu)建了 ProSynth、LoopSynth 和 MonoSynth 的版本，并基于 Clingo [Gebser 等 2011b] 和 WASP [Alviano 等 2013] 構(gòu)建了 ASPSynth 的版本。

最終我們發(fā)現(xiàn)，MonoSynth 和 LoopSynth 相較 ProSynth 可帶來(lái)一些改進(jìn)，但結(jié)果并不一致且依賴于所使用的求解器。然而，ASPSynth-Clingo 表現(xiàn)出明顯的優(yōu)勢(shì)。它的性能一方面來(lái)源于其作為一個(gè)單一、高度集成系統(tǒng)的工程實(shí)現(xiàn)，另一方面也得益于這種緊密集成使得它在搜索解空間時(shí)遇到的沖突更少。

成功的關(guān)鍵洞察在于視角的轉(zhuǎn)變：從將 Datalog 視為一種獨(dú)立的（單調(diào)的）邏輯編程語(yǔ)言——這是程序語(yǔ)言社區(qū)中一個(gè)常見(jiàn)且合理的觀點(diǎn)，在近年來(lái) Datalog 在該領(lǐng)域獲得了應(yīng)有的關(guān)注——轉(zhuǎn)變?yōu)閷⑵湟暈橐环N更具表達(dá)力的（非單調(diào)的）邏輯編程范式（即 ASP）的一個(gè)片段。這種視角的轉(zhuǎn)變，使得我們能夠從 SMT 求解器（程序語(yǔ)言社區(qū)首選的約束求解范式）轉(zhuǎn)向 ASP 求解器——這些工具在邏輯編程和人工智能社區(qū)中受到了廣泛關(guān)注，但在程序語(yǔ)言社區(qū)中卻鮮有應(yīng)用。

貢獻(xiàn)

總而言之，我們做出了如下貢獻(xiàn)：

• 我們提出了三種解決 Datalog 作為規(guī)則選擇的綜合問(wèn)題 的全新方法，所有方法都探索了 SAT 求解與 Horn 子句求值的不同結(jié)合方式（見(jiàn)第 4、5 和 6 章）。其中兩種方法提供了一種在 SMT 中描述 Datalog 謂詞的方式，其應(yīng)用范圍超越了程序綜合本身（見(jiàn)第 4 和第 5 章）。

• 我們使用多個(gè)后端 SAT 求解器對(duì)這些工具與當(dāng)前最先進(jìn)的 ProSynth 進(jìn)行了全面評(píng)估（見(jiàn)第 7 章）。我們展示了求解器的選擇對(duì)基于求解器算法的相對(duì)性能可能產(chǎn)生重大影響。

• 我們展示了 ASP 在解決程序語(yǔ)言社區(qū)關(guān)心的問(wèn)題上的有效性：我們將 Datalog 綜合編碼為規(guī)則選擇問(wèn)題，并通過(guò) ASP 實(shí)現(xiàn)了比當(dāng)前最先進(jìn)的 ProSynth 快一個(gè)數(shù)量級(jí)（幾何平均約 9 倍）的速度提升（見(jiàn)第 7.4 章）。我們的工作為程序語(yǔ)言社區(qū)提供了關(guān)于 ASP 技術(shù)的實(shí)踐性概述，涵蓋了基于循環(huán)公式的 SAT 編碼方法（見(jiàn)第 5 章）以及直接求解的方法（見(jiàn)第 6 章）。

• 我們闡明了當(dāng)前 Datalog 作為規(guī)則選擇的綜合問(wèn)題 的設(shè)定中存在的局限性，并展示了如何將其推廣為一種有界模型檢測(cè)的形式（見(jiàn)第 8 章）。

2 作為規(guī)則選擇的 Datalog 綜合

第 2.1 節(jié)介紹 Datalog 的背景知識(shí)，第 2.2 節(jié)介紹“作為規(guī)則選擇的 Datalog 綜合”問(wèn)題。第 2.3 節(jié)概述了一種基線方法以及我們提出的一系列解決方案。

2.1 Datalog

一個(gè) Datalog 程序 [Gallaire 和 Minker 1978；Green 等 2013] 是一組關(guān)于謂詞 的推理規(guī)則，其中每個(gè)規(guī)則作用于項(xiàng)（terms）的向量 t 上，并且每條規(guī)則都是一個(gè) Horn 子句：

一個(gè)項(xiàng) （term） 要么是一個(gè)常量 ，要么是一個(gè)變量 （我們使用粗體 c 和 X 分別表示常量和變量的向量）。原子 ?(t?) 是該規(guī)則的頭 （head）；其余的原子構(gòu)成了規(guī)則的體 （body）（可以為空）。頭中的變量必須出現(xiàn)在體中 。

直觀上，每條規(guī)則可以從右向左讀作一個(gè)蘊(yùn)含式：對(duì)所有變量進(jìn)行全稱量化后，體中原子的合取蘊(yùn)含頭中的原子。

一個(gè) Datalog 程序 的語(yǔ)義是定義在一組輸入事實(shí)（即基礎(chǔ)原子，稱為外延數(shù)據(jù)庫(kù)，或 EDB）上的。如果我們有輸入事實(shí) ，則 () 被定義為在初始事實(shí) 的基礎(chǔ)上，通過(guò)不斷應(yīng)用程序 中的規(guī)則所達(dá)到的最小不動(dòng)點(diǎn) ，通常使用半樸素求值法（semi-naive evaluation）來(lái)計(jì)算。

最終得到的事實(shí)集合就是輸出結(jié)果（稱為內(nèi)涵數(shù)據(jù)庫(kù)，或 IDB）。從函數(shù)的角度來(lái)看， 是從 EDB 到 IDB 的正單調(diào)函數(shù) ：如果 ? ，則 () ? ()。或者，從模型論的角度來(lái)看，Datalog 程序與 EDB 結(jié)合的意義是：將 EDB 和程序中的規(guī)則視為邏輯蘊(yùn)含時(shí)，所得到的最小 Herbrand 模型 。

Datalog 的求值可以非常高效，并且適用于多種強(qiáng)大的優(yōu)化技術(shù)（例如并行計(jì)算、目標(biāo)導(dǎo)向搜索）。盡管它不像通用邏輯編程語(yǔ)言（如 Prolog）那樣具有表達(dá)力，但 Datalog 在表達(dá)能力和性能之間的良好平衡使其成為某些領(lǐng)域中流行的實(shí)現(xiàn)選擇，例如靜態(tài)分析 [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 程序綜合的任務(wù)是合成一組滿足某種規(guī)范的 Datalog 規(guī)則。我們建立在一系列 Datalog 綜合工作的基礎(chǔ)上，這些工作始于 ALPS [Si 等 2018]，該研究提出了一種方法，可以從元規(guī)則（meta-rules）生成一組候選 Datalog 規(guī)則。

給定這組候選規(guī)則后，ALPS 會(huì)選擇一個(gè)子集，使其在輸入-輸出示例上表現(xiàn)出正確的行為。這個(gè)任務(wù)——從一組候選 Datalog 規(guī)則中篩選出一個(gè)滿足規(guī)范的子集——被稱為“作為規(guī)則選擇的綜合”（synthesis as rule selection）。

ALPS 使用一種由委員會(huì)投票查詢（query-by-committee）驅(qū)動(dòng)的雙向搜索策略來(lái)解決這一問(wèn)題。后續(xù)的一系列研究專注于“作為規(guī)則選擇的綜合”問(wèn)題（假設(shè)候選規(guī)則已由 ALPS 生成），采用了一些受數(shù)值松弛方法啟發(fā)的技術(shù) [Si 等 2019]，以及最近使用的反例引導(dǎo)歸納綜合（CEGIS）方法 [Raghothaman 等 2020]。我們的算法正是構(gòu)建在最后這種方法之上的。

作為規(guī)則選擇的綜合（Synthesis as Rule Selection） 。給定：

• （a）一個(gè)輸入樣本以及正例和負(fù)例輸出元組（output tuples），

• 和（b）一組候選規(guī)則，

任務(wù)是生成：

• （c）候選規(guī)則的一個(gè)子集，使得它能夠產(chǎn)生所有正例輸出，而不產(chǎn)生任何負(fù)例輸出。

形式化地，設(shè) 為輸入元組（即 EDB），T?exp 為正輸出元組集合（IDB 的一個(gè)子集），T?exp 為負(fù)輸出元組集合。如果 all 是所有候選規(guī)則的集合，我們需要從中選擇一組規(guī)則 ? all，使得：

• T?exp ? ()（即所有正例輸出都包含在結(jié)果中），且

• T?exp ∩ () = ?（即不產(chǎn)生任何負(fù)例輸出）。

例如，在合成圖的傳遞閉包（transitive closure）時(shí)，規(guī)范可能包括由 edge 謂詞定義的一個(gè)示例圖 ，以及由 path 謂詞組成的集合 T?exp 和 T?exp；而候選規(guī)則集合 all 則包含用 edge 和自身來(lái)定義 path 的那些規(guī)則（見(jiàn)圖1）。

2.3 四種方法

我們提出了四種解決 Datalog 作為規(guī)則選擇的綜合問(wèn)題 的方法：一種是當(dāng)前最先進(jìn)的方法，另外三種是我們提出的新方法。我們使用如下圖示語(yǔ)言來(lái)描繪每種方法：

• SAT 求解

  用藍(lán)色表示，

• Datalog 求值

  用橙色表示；

• 虛線箭頭

  表示一次性交互，

• 實(shí)線箭頭

  表示重復(fù)交互；

• 組件標(biāo)注為獨(dú)立可執(zhí)行文件（ .exe ）、庫(kù)文件（ .lib ）或解釋執(zhí)行的 Python 程序（ .py ）。

我們首先介紹當(dāng)前最先進(jìn)的方法 ProSynth [Raghothaman 等 2020]。ProSynth 連接了一個(gè) SAT 求解器和一個(gè)增強(qiáng)了“原因溯源”（why 和 why-not provenance）功能的 Datalog 求解器（見(jiàn)第 3 節(jié)；圖 2），在反例引導(dǎo)綜合（CEGIS）循環(huán) [Solar-Lezama 等 2006] 中頻繁調(diào)用 Datalog 求解和 SAT 求解。

我們的三種方法都旨在減少這種 CEGIS 循環(huán)的開(kāi)銷；也就是說(shuō)，它們減少了在綜合過(guò)程中為糾正錯(cuò)誤猜測(cè)而進(jìn)行的來(lái)回調(diào)用次數(shù)。

我們的第一種方法 MonoSynth 利用了 Datalog 的單調(diào)性，將 Datalog 謂詞視為 SMT 謂詞（見(jiàn)第 4 節(jié)；圖 3）。MonoSynth 只對(duì) SMT 進(jìn)行一次調(diào)用，但會(huì)對(duì) Datalog 求值進(jìn)行多次調(diào)用；與 ProSynth 一樣，它也依賴于溯源信息。

我們剩下的兩種方法借鑒了答案集編程 （ASP）中的思想。ASP 求解器通常分為兩個(gè)階段：實(shí)例化 （grounding）和求解 （solving）。

• 實(shí)例化階段會(huì)消除所有變量，生成“實(shí)例化”規(guī)則。這是一個(gè)代價(jià)較高的過(guò)程，在最壞情況下退化為顯式枚舉所有可能的變量替換組合。

• 實(shí)際上，實(shí)例化工具使用各種策略來(lái)避免簡(jiǎn)單的枚舉。

在 ASP 中，求解階段 是一種擴(kuò)展了 SAT 搜索的形式，加入了確保最終模型滿足邏輯程序語(yǔ)義的機(jī)制（即，與 Horn 子句求解保持一致）。

這兩種方法中的第一個(gè)是 LoopSynth ，它受到 ASSAT [Lin 和 Zhao 2004] 中“循環(huán)公式”（loop formulas）概念的啟發(fā)（見(jiàn)第 5 節(jié)；圖 5）。

我們首先將候選規(guī)則編碼為一個(gè) ASP 程序，并使用 Gringo 實(shí)例化器 [Gebser 等 2007] 生成實(shí)例化規(guī)則。然后我們使用 Clark 完備化 [Clark 1977] 將這些實(shí)例化規(guī)則和輸入-輸出示例編碼為 SAT 公式，并斷言循環(huán)公式以確保我們生成的是一個(gè)穩(wěn)定模型（即有效解）。

與 MonoSynth 只調(diào)用一次 SMT 不同，LoopSynth 是增量地調(diào)用 SAT 。MonoSynth 在每次 CEGIS 迭中可能多次調(diào)用 Datalog；而 LoopSynth 則先對(duì)程序進(jìn)行實(shí)例化——這相當(dāng)于生成 IDB 的超集，也就是執(zhí)行了 Datalog 求值——然后在每次 CEGIS 迭代中只調(diào)用一次 Datalog。LoopSynth 不使用任何 Datalog 的溯源信息 。

最后，我們?cè)谖覀兎Q之為 ASPSynth 的方法中，將問(wèn)題直接編碼為 ASP （見(jiàn)第 6 節(jié)；圖 8）。

這種方法是最簡(jiǎn)單且最高效的：沒(méi)有來(lái)回交互，只需將編碼好的問(wèn)題交給現(xiàn)成的 ASP 實(shí)例化器和求解器即可。此外，編碼為 ASP 使得很容易為規(guī)則指定一個(gè)成本度量標(biāo)準(zhǔn)，從而提升我們所生成解決方案的質(zhì)量。

3 當(dāng)前最先進(jìn)的方法：ProSynth

ProSynth 是目前解決 Datalog 作為規(guī)則選擇的綜合問(wèn)題 的最先進(jìn)工具 [Raghothaman 等 2020]。它通過(guò)在 SAT 求解器和 Datalog 求解器之間來(lái)回傳遞信息，實(shí)現(xiàn)了反例引導(dǎo)的歸納綜合 （CEGIS），其結(jié)構(gòu)如圖 2 所示。

ProSynth 的輸入是一個(gè) Datalog 程序，其中包含了所有候選規(guī)則 all 中的規(guī)則，只不過(guò)每條規(guī)則都被擴(kuò)展了一個(gè)新的前提 rule()，用以標(biāo)識(shí)這是第 條規(guī)則。如果在 EDB 中設(shè)置了事實(shí) rule()，則啟用該候選規(guī)則；否則，該規(guī)則永遠(yuǎn)不會(huì)被觸發(fā)。此外，all 中的每條規(guī)則都與 SAT 求解器中的一個(gè)布爾變量相關(guān)聯(lián)。

SAT 求解器會(huì)生成一個(gè)猜測(cè)，決定啟用哪些規(guī)則（即，在生成的模型中值為真的那些布爾變量）；對(duì)應(yīng)的 rule()事實(shí)會(huì)在 Datalog 程序中被啟用，并在示例輸入上運(yùn)行該程序。默認(rèn)情況下，ProSynth 使用 Soufflé 的編譯模式[Jordan 等 2016] 進(jìn)行 Datalog 求值：Datalog 程序會(huì)被編譯成 C++，然后需要進(jìn)一步編譯執(zhí)行。

如果 Datalog 程序的輸出不滿足規(guī)范，ProSynth 的算法就會(huì)使用溯源 （provenance）[Woodruff 和 Stonebraker 1997] 來(lái)生成阻止約束（blocking constraints），并反饋給 SAT 求解器。

• 如果某個(gè)不期望的元組 出現(xiàn)在了 () 中，那么 why 溯源 [Buneman 等 2001] 可以指出是哪些規(guī)則導(dǎo)致了這個(gè)元組的產(chǎn)生——關(guān)閉這些規(guī)則中的一個(gè)或多個(gè)，有望排除這個(gè)元組。（但 ProSynth 使用的是 Soufflé 的溯源機(jī)制 [Zhao 等 2020]，它不會(huì)生成多條路徑——因此，對(duì)于“過(guò)度確定”的元組（overdetermined tuples），即使關(guān)閉某些規(guī)則，它們可能仍然存在 [Green 等 2007]。）

• 如果某個(gè)期望的元組缺失 于 ()，那么 why-not 溯源 [Herschel 等 2009；Lee 等 2019] 可以指出有哪些規(guī)則本可以導(dǎo)致該元組的產(chǎn)生——啟用這些規(guī)則中的某一條，有望生成該元組。

為了生成 why-not 溯源信息，ProSynth 使用了一種受 delta 調(diào)試 （delta debugging）啟發(fā)的技術(shù)，從所有禁用的規(guī)則中篩選出一個(gè)更小的子集；只要這個(gè)子集中的一條規(guī)則未被啟用，就無(wú)法推導(dǎo)出某個(gè)特定的期望元組。這一過(guò)程涉及多次調(diào)用 Soufflé。

ProSynth 將這些約束返回給 SAT 求解器，求解器再生成一個(gè)新的猜測(cè)；這一過(guò)程不斷循環(huán)，直到找到一個(gè)解，或者搜索空間耗盡。

4 收緊循環(huán)：將 Datalog 視為一個(gè)單調(diào) SMT 理論

我們的第一種算法直接建立在 ProSynth 的方法之上，并針對(duì)其 SAT 求解器與 Datalog 求解器之間松散集成所導(dǎo)致的兩個(gè)潛在局限性進(jìn)行了改進(jìn)。

從工程角度來(lái)看，ProSynth 帶來(lái)了多個(gè)操作系統(tǒng)進(jìn)程之間通信的開(kāi)銷：ProSynth 本身是用 Python 編寫(xiě)的腳本，使用了 Z3 的綁定接口，但它會(huì)調(diào)用由 Soufflé 編譯生成的獨(dú)立可執(zhí)行文件來(lái)運(yùn)行 Datalog 程序。

從算法角度來(lái)看，在 SAT 求解器選擇規(guī)則的過(guò)程中，Datalog 的計(jì)算并不會(huì)為其提供任何增量反饋：它只會(huì)在 SAT 求解器猜測(cè)出一組完整的候選規(guī)則（即每條規(guī)則都被標(biāo)記為“啟用”或“禁用”）之后才生成反例，即使 SAT 求解器在早期就做出了不可能通向可行解的選擇也是如此。

我們的方法通過(guò)為 SMT 求解器擴(kuò)展一個(gè) Datalog 理論來(lái)解決這些限制。
與 ProSynth 類似，這個(gè)理論使用 Datalog 的 why 和 why-not 溯源機(jī)制來(lái)推導(dǎo)精確的理論沖突。
但與 ProSynth 不同的是，SAT 求解、Datalog 求解和沖突生成邏輯都發(fā)生在一個(gè)操作系統(tǒng)進(jìn)程中。
此外，由于我們提出的 Datalog 理論是一個(gè)單調(diào)的 SMT 理論 （見(jiàn)第 4.1 和 4.2 節(jié)），Datalog 求解器能夠基于部分規(guī)則選擇 （即 SAT 求解器尚未對(duì)某些規(guī)則做出決定）向 SAT 求解器提供反例，從而使 SAT 求解器可以主動(dòng)剪枝那些不可能產(chǎn)生解的搜索子空間。

我們的實(shí)現(xiàn)（見(jiàn)第 4.3 節(jié)）支持 Z3 和 CVC4，并能以一種直接的方式對(duì)綜合問(wèn)題進(jìn)行編碼（見(jiàn)第 4.4 節(jié)）。

4.1 背景知識(shí)：?jiǎn)握{(diào)理論

在惰性 SMT 求解 [Nieuwenhuis 等 2006；Sebastiani 2007] 中——這是目前最受歡迎的兩個(gè) SMT 求解器的基礎(chǔ) [Barrett 等 2011；Moura 和 Bj?rner 2008]——核心 SAT 求解器為理論謂詞分配真值；如果從理論求解器的角度來(lái)看這一賦值不可滿足，則會(huì)迫使 SAT 求解器回溯并提出新的賦值。

為了使這種集成高效運(yùn)行，理論求解器應(yīng)提供兩種操作：

• 理論傳播

  （theory propagation）：給定理論原子的部分賦值，推斷出在該賦值下必須為真的其他理論文字（literals）。

• 沖突生成

  （conflict generation）：給定一個(gè)從理論角度看不可滿足的部分賦值，生成一個(gè)包含沖突原子的子句；核心 SAT 求解器學(xué)習(xí)該子句的否定。

例如，假設(shè)我們有一個(gè)理論，其中包含形式為 < ~ 的謂詞，且 < 的預(yù)期解釋是整數(shù)小于關(guān)系。如果 SAT 求解器將原子 < ~ 和 ~ < 設(shè)為真，理論求解器可以傳播得出原子 < 也必須為真。如果 SAT 求解器已經(jīng)將原子 < 設(shè)為假，則理論求解器可以生成沖突：
< ~ ∧ ~ < ∧ ?( < )。

SAT 求解器可以學(xué)習(xí)其否定，即：
?( < ~) ∨ ?(~ < ) ∨ < ，
最終促使搜索找到一個(gè)符合我們對(duì) < 解釋為“小于”的模型。

當(dāng)理論滿足以下兩個(gè)條件時(shí)，SMT 效果最佳：

1. 在給定一個(gè)小的局部賦值時(shí)能夠進(jìn)行傳播；

2. 在生成沖突時(shí)返回小的子句。

Bayless 等人 [2015] 提出了一類被稱為單調(diào)理論 的理論，這類理論在存在一種有效方式來(lái)判定具體實(shí)例的情況下，能夠同時(shí)滿足上述兩個(gè)標(biāo)準(zhǔn)。

一個(gè)單調(diào)理論是指其唯一的數(shù)據(jù)類型是布爾型，且所有謂詞都是單調(diào)的 ，也就是說(shuō)，對(duì)于任意這樣的謂詞 ，都有如下性質(zhì)成立：

也就是說(shuō)，如果一個(gè)謂詞在某個(gè)比特位關(guān)閉時(shí)成立，那么當(dāng)這個(gè)比特位開(kāi)啟后它仍然成立。

一個(gè)單調(diào)理論的例子是有限圖的可達(dá)性 ：
給定邊 是否包含在圖中取決于變量 是否為真，那么謂詞 ?,(1, ..., ) 為真當(dāng)且僅當(dāng)節(jié)點(diǎn) 到節(jié)點(diǎn) 存在一條路徑。這從直觀上看是單調(diào)的：當(dāng)我們向圖中添加一條邊時(shí)，并不會(huì)使之前已有的任何路徑失效。

如果存在一種高效的算法來(lái)判定該理論中具體實(shí)例的問(wèn)題是否可滿足，那么一個(gè)單調(diào)理論就能有效地執(zhí)行理論傳播和沖突生成 。我們上面提到的圖可達(dá)性例子就符合這一條件：對(duì)于一個(gè)具體的圖，我們可以直接運(yùn)行標(biāo)準(zhǔn)的圖算法。

那么，單調(diào)理論是如何進(jìn)行理論傳播和沖突生成的呢？

理論傳播（Theory Propagation）

給定一個(gè)部分賦值 ，設(shè) 是該賦值限制在理論中暴露的布爾變量上的部分賦值（例如，在圖可達(dá)性例子中的 ）。令 ? 為該賦值的正擴(kuò)展 ，即對(duì) 中未賦值的布爾變量都賦值為 1。

對(duì)于一個(gè)理論謂詞 ，如果我們通過(guò)具體實(shí)例的判定程序確定 ? ? ? 成立，則可以推出 ? ?，于是我們可以傳播文字 ?。

同樣地，使用負(fù)擴(kuò)展 ?（即將 中未賦值的布爾變量都賦值為 0），如果 ? ? 成立，則我們可以傳播文字 。

沖突生成（Conflict Generation）

給定一個(gè)由上述“過(guò)近似/欠近似”方案引發(fā)的沖突，沖突中總是存在某個(gè)理論原子 ，使得暴露的布爾變量的賦值與原子 的賦值一起是不可滿足的。

在這種情況下：

• 如果 ? ? 成立，則 中的正文字蘊(yùn)含 （可以為涉及 的沖突提供理由）；

• 如果 ? ? ? 成立，則 中的負(fù)文字蘊(yùn)含 ?（可以為涉及 ? 的沖突提供理由）。

當(dāng)用于判定具體問(wèn)題實(shí)例的算法能夠提供其判斷的見(jiàn)證信息 （witness）時(shí)，有時(shí)可以學(xué)習(xí)到比這些默認(rèn)方式更優(yōu)的子句。例如，從頂點(diǎn) 到頂點(diǎn) 的路徑上的邊就為原子 ?,(1, ..., ) 提供了一個(gè)合理的解釋：因?yàn)檫@些邊對(duì)應(yīng)的布爾變量 必然是啟用的 SMT 布爾變量的一個(gè)子集，所以它們構(gòu)成了對(duì)該原子更為精確的理由。

單調(diào)理論通常用于生成性任務(wù) （generative purposes）。例如：

• 有限圖可達(dá)性的單調(diào)理論被用于生成滿足某些可達(dá)性約束的圖（即對(duì) 的賦值）[Bayless 等 2015]，以及合成能夠在虛擬云網(wǎng)絡(luò)中到達(dá)特定節(jié)點(diǎn)的數(shù)據(jù)包 [Backes 等 2019]；

• 計(jì)算樹(shù)邏輯（CTL）的單調(diào)理論被用于合成由該邏輯描述的系統(tǒng) [Klenze 等 2016]；

• - 最大流的單調(diào)理論被用作求解器組合的一部分，用于生成虛擬數(shù)據(jù)中心的資源分配方案 [Bayless 等 2020]。

每一個(gè) Datalog 程序 都是一個(gè)單調(diào)理論 。給定一個(gè)純 Datalog 程序（無(wú)否定）和一組可能的 EDB 事實(shí)，我們可以構(gòu)造一個(gè)單調(diào)的 SMT 理論，其中包含由潛在輸入事實(shí)參數(shù)化的 Datalog 程序輸出元組。

考慮一個(gè) Datalog 程序，它有 個(gè)可能的外延事實(shí)（extensional facts），依次編號(hào)為 ? 到 ?。假設(shè) (c) 是一個(gè)可能的推導(dǎo)出的事實(shí)（derived fact）。我們構(gòu)建一個(gè) SMT 謂詞符號(hào) c，其類型為 Bool? → Bool。

形式為 c(?, ..., ?) 的謂詞在該理論中為真，當(dāng)且僅當(dāng)在使用外延事實(shí)集合 {? | ? = 1} 運(yùn)行 Datalog 程序后，可以推導(dǎo)出事實(shí) (c)。

此外，該謂詞滿足單調(diào)理論的要求：

直觀上，? 允許我們開(kāi)啟或關(guān)閉外延事實(shí)（extensional facts），因此 SMT 謂詞的單調(diào)性源于 Datalog 程序本身的單調(diào)性：如果在某個(gè)外延事實(shí)集合 下我們推導(dǎo)出了 (c)，那么在任何包含 的集合下也都能推導(dǎo)出 (c)。

這樣一個(gè)基于 Datalog 的理論可以自然地融入單調(diào)理論框架中：

理論傳播（Theory Propagation）

通過(guò)兩次調(diào)用 Datalog 求解器，執(zhí)行標(biāo)準(zhǔn)的過(guò)近似/欠近似方案：

1. 第一次調(diào)用計(jì)算在負(fù)擴(kuò)展 下的程序，即計(jì)算 (?)，其中 ? = {? | ??[?] = 1}。如果一個(gè)原子出現(xiàn)在 (?) 中，則它被 ?? 中的正變量所蘊(yùn)含。

2. 第二次調(diào)用計(jì)算在正擴(kuò)展 下的程序，即計(jì)算 (?)，其中 ? = {? | ??[?] = 1}。如果一個(gè)原子不在 (?) 中，則它的否定被 ?? 中的負(fù)變量所蘊(yùn)含。

借助溯源信息 ，我們可以比默認(rèn)沖突解釋機(jī)制做得更好，后者只是返回 ?? 中的正謂詞或 ?? 中的負(fù)謂詞。

1. 如果一個(gè)理論原子 c(?, ..., ?) 成立，說(shuō)明事實(shí) (c) 必須出現(xiàn)在 (?) 中；提取其溯源信息 。設(shè) 是推導(dǎo)出 (c) 所涉及的輸入事實(shí)集合。作為對(duì) c(?, ..., ?) 的解釋，返回集合 {? | ? ∈ }，這是 ?? 中正變量的一個(gè)子集。

2. 如果一個(gè)理論原子 ?c(?, ..., ?) 成立，說(shuō)明事實(shí) (c) 不應(yīng)出現(xiàn)在 (?) 中；使用 ProSynth 的 delta 調(diào)試技術(shù) ，從集合 ? ? 中找出一個(gè)事實(shí)子集 ，只要啟用這些事實(shí)中的某一個(gè)，就可以推導(dǎo)出 (c)。返回集合 {? | ? ∈ } 作為對(duì) ?c(?, ..., ?) 的解釋；這將是 ?? 中負(fù)變量的一個(gè)子集。

將任意 Datalog 程序（配備一組可能的輸入事實(shí)）轉(zhuǎn)換為一個(gè)單調(diào) SMT 理論的能力，在 Datalog 綜合之外也有多種潛在用途。

首先，它提供了一種輕量級(jí)且聲明式的方法來(lái)構(gòu)建可表達(dá)為 Datalog 程序的單調(diào)理論：只需編寫(xiě) Datalog 程序，然后依賴我們的框架進(jìn)行理論上高效的傳播與沖突生成。例如，有限圖可達(dá)性的單調(diào)理論可以用一個(gè)三規(guī)則的 Datalog 程序來(lái)表示。雖然這種實(shí)現(xiàn)方式肯定不如手寫(xiě)的 SMT 理論高效，但比起編寫(xiě)完整的理論或自定義傳播器要節(jié)省大量工作。

其次，我們的框架提供了一種方法來(lái)求解涉及 Datalog 謂詞的 SMT 公式。由于綜合是單調(diào)理論的主要用途之一，我們推測(cè)基于 Datalog 的單調(diào)理論可用于那些部分問(wèn)題以 Datalog 表達(dá)、部分問(wèn)題以其他 SMT 理論表達(dá)的綜合任務(wù)中，如下例所示：

示例 4.1

考慮一個(gè)任務(wù)：判斷是否存在一個(gè) API 調(diào)用序列會(huì)導(dǎo)致系統(tǒng)進(jìn)入不良狀態(tài)，例如敏感信息通過(guò)公共通道泄露出去。這是一個(gè)具有挑戰(zhàn)性的問(wèn)題，因?yàn)榭赡艿男蛄袛?shù)量是無(wú)限的。我們可以測(cè)試隨機(jī)序列，但這不太可能找到有意義的結(jié)果；另一方面，像符號(hào)執(zhí)行這樣的更全面測(cè)試策略又難以擴(kuò)展，因?yàn)槊慨?dāng)執(zhí)行器決定下一個(gè)調(diào)用哪個(gè) API 時(shí)，路徑數(shù)量會(huì)爆炸式增長(zhǎng)。

相比之下，我們的方法將結(jié)合：

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

• 一個(gè)基于 Datalog 的單調(diào)理論，

來(lái)合成潛在有趣的 API 調(diào)用序列，之后再使用更精確的技術(shù)（如符號(hào)執(zhí)行）進(jìn)行驗(yàn)證。

作為我們單調(diào)理論的后端，我們將使用一種基于 Datalog 的分析方法，用于計(jì)算某個(gè) API 調(diào)用序列是否可能導(dǎo)致私有信息流入公共接收點(diǎn)（可能是對(duì) Livshits 和 Lam [2005] 提出的 Java 污點(diǎn)分析的一種擴(kuò)展）。

該分析參數(shù)化于允許的 API 調(diào)用順序；具體來(lái)說(shuō)，它接受如下形式的事實(shí)作為輸入：

• start( )

  （表示 可以作為序列中的第一個(gè) API 調(diào)用），

• next( , )

  （表示對(duì) 的調(diào)用可以直接跟在對(duì) 的調(diào)用之后）。

作為輸出，該分析會(huì)在給定允許的 API 調(diào)用順序下，若違反了所需的安全屬性，則生成一個(gè) error 事實(shí)。

我們的單調(diào) SMT 理論將這些事實(shí)暴露為 SMT 層級(jí)的布爾變量。

通過(guò)構(gòu)建將 Datalog 事實(shí)與 SMT 序列理論中的約束條件連接起來(lái)的 SMT 斷言，我們能夠合成出有趣的 API 調(diào)用序列：這些序列根據(jù)我們的 Datalog 分析可能引發(fā)錯(cuò)誤條件，并且也滿足我們使用序列理論所施加的任何附加約束（例如匹配某個(gè)正則表達(dá)式）。

我們從序列理論中使用了謂詞 seq.prefixof(, ) 和 seq.contains(, )。設(shè) s 是一個(gè) SMT 變量，它將被實(shí)例化為我們生成的調(diào)用序列。

• 對(duì)于每個(gè) API 方法 ，我們斷言：事實(shí) start( ) 成立當(dāng)且僅當(dāng) seq.prefixof("", s) 成立。

• 對(duì)于每對(duì) API 方法 和 ，我們斷言：事實(shí) next( , ) 成立當(dāng)且僅當(dāng) seq.contains(s, "") 成立。

• 最后，我們斷言推導(dǎo)出的事實(shí) error 成立。

如果這一組斷言不可滿足，那么我們知道不存在任何 API 調(diào)用序列會(huì)導(dǎo)致安全屬性被違反；如果它是可滿足的，我們可以提取 s 的一個(gè)模型并測(cè)試該調(diào)用序列。

此外，我們還可以使用序列理論中的其他操作符來(lái)引導(dǎo)搜索過(guò)程：

• 例如，要強(qiáng)制序列長(zhǎng)度為 ，我們可以斷言 seq.len(s) = ；

• 要限制序列中 出現(xiàn)在 之后的情況，我們可以使用 Z3 支持的正則表達(dá)式，并斷言 ?seq.in.re(s, ".*.*.*") 。

我們認(rèn)為，原則上這些涉及 Datalog 謂詞的 SMT 斷言可以編碼為 Formulog [Bembenek 等 2020] 程序——這是一種帶有表示和推理 SMT 公式機(jī)制的 Datalog 變體。然而，這種方法在實(shí)踐中不太可能表現(xiàn)良好（事實(shí)上，我們將“作為規(guī)則選擇的綜合”問(wèn)題編碼為 Formulog 程序時(shí)，無(wú)法擴(kuò)展到除最小的 ProSynth 基準(zhǔn)之外的任何情況）：

1. Formulog 執(zhí)行的是窮舉式的、基于飽和的推導(dǎo)過(guò)程，而不是由 SMT 提供的有指導(dǎo)的搜索；

2. 增量式 SMT 求解允許我們逐步添加新的斷言（例如對(duì)我們期望解的細(xì)化），而無(wú)需從頭開(kāi)始重新求解，但 Formulog 不支持增量計(jì)算。

像 Formulog 一樣，受約束的 Horn 子句 （CHC）求解提供了一種方法來(lái)求解 Horn 子句與 SMT 公式的混合形式 [Bj?rner 等 2015；Grebenshchikov 等 2012；Gurfinkel 等 2015；Hoder 和 Bj?rner 2012]。然而，CHC 求解器在它們支持的理論范圍上通常較為有限，而且更根本的問(wèn)題是：它們尋找的是通用的 SMT 模型，而我們需要在最小模型語(yǔ)義 下解釋 Horn 子句，以與 Datalog 保持一致。

4.3 我們的實(shí)現(xiàn)

我們實(shí)現(xiàn)了該方法的兩個(gè)版本：

• 一個(gè)是在 CVC4 的擴(kuò)展版本中作為一個(gè) 自定義理論 實(shí)現(xiàn)；

• 另一個(gè)是在 Z3 上作為 用戶傳播器 （user propagator）實(shí)現(xiàn)。

這兩個(gè)版本擁有基本相同的 API，實(shí)現(xiàn)也非常相似。它們都暴露了一個(gè)編碼器類 （encoder class），構(gòu)造時(shí)需要傳入一個(gè)特定的求解器實(shí)例以及一個(gè) Soufflé 程序的引用（該程序可以作為庫(kù)動(dòng)態(tài)鏈接）。?

用戶將一個(gè)（已實(shí)例化的）Soufflé 元組傳遞給編碼器；編碼器返回一個(gè)對(duì)應(yīng)于該元組的布爾類型的 SMT 變量。用戶可以在任意包含這些布爾變量的 SMT 公式中進(jìn)行斷言；編碼器的后端確保 SAT 核心計(jì)算出的任何模型在 Datalog 語(yǔ)義下都是可接受的，遵循上一節(jié)中描述的單調(diào)理論方法。

編碼器使用 Datalog 的 why 和 why-not 溯源機(jī)制來(lái)生成沖突解釋。

我們對(duì) Raghothaman 等人 [2020] 提出的 delta-debugging 技術(shù)的實(shí)現(xiàn)遵循 ProSynth 中的算法實(shí)現(xiàn)，這與論文中描述的算法略有不同：它減少了 Datalog 的調(diào)用次數(shù)，但返回的 why-not 溯源信息精度較低。

我們的實(shí)現(xiàn)使用了若干啟發(fā)式策略。

首先，我們使用了一個(gè)原始的真值維護(hù)系統(tǒng) （truth maintenance system）[Doyle 1979；McAllester 1990]，用于緩存每個(gè)部分賦值在其正擴(kuò)展和負(fù)擴(kuò)展下傳播出的理論原子的解釋信息。

其次，給定一個(gè)部分賦值，可能會(huì)存在多個(gè)沖突需要報(bào)告。ProSynth 的實(shí)現(xiàn)會(huì)在每個(gè)指定的輸出關(guān)系中報(bào)告最多 30 個(gè) why 沖突和 1 個(gè) why-not 沖突。而 Z3 的傳播器 API 每次部分賦值只允許報(bào)告一個(gè)沖突；為了保持一致性，我們?cè)?Z3 和 CVC4 的兩個(gè)版本中都采用了相同的策略。

總體來(lái)說(shuō)，我們盡量避免進(jìn)行 Datalog 求值，并返回較小的沖突。

最后，一個(gè)重要的啟發(fā)式策略是：我們應(yīng)多積極地嘗試發(fā)現(xiàn)沖突 。并非在每一個(gè)部分賦值上都必須檢查沖突；相反，我們的實(shí)現(xiàn)會(huì)將布爾參數(shù)的賦值緩存起來(lái)，直到達(dá)到某個(gè)閾值后再進(jìn)行處理（詳見(jiàn)第 7 節(jié)）。

4.4 編碼綜合問(wèn)題

我們構(gòu)建了一個(gè)工具 MonoSynth ，它利用 Datalog 理論來(lái)解決“作為規(guī)則選擇的 Datalog 綜合”問(wèn)題（見(jiàn)圖 3）。

給定一個(gè)綜合問(wèn)題后，它以編程方式將候選規(guī)則的 Soufflé 程序（如第 3 節(jié)所述）作為共享庫(kù)加載進(jìn)來(lái)，并將示例輸入載入該程序中。

通過(guò)使用理論接口，它將期望的和不期望的輸出元組編碼為 SMT 項(xiàng)并進(jìn)行斷言。同時(shí)，它也對(duì) rule() 元組進(jìn)行編碼，但不對(duì)它們施加約束。

最后，它調(diào)用 SMT 求解器檢查可滿足性并構(gòu)造模型；MonoSynth 輸出與模型中為真的 rule() 對(duì)應(yīng)的規(guī)則選擇結(jié)果。

4.4.2 與先前方法的比較

MonoSynth 在多個(gè)關(guān)鍵方面有別于 ProSynth 。

首先，所有計(jì)算都在同一個(gè)操作系統(tǒng)進(jìn)程中完成 。
ProSynth 使用一個(gè) Python 進(jìn)程來(lái)執(zhí)行其邏輯和 SAT 求解器的工作；每次調(diào)用 Datalog 程序時(shí)都會(huì)啟動(dòng)一個(gè)新的獨(dú)立進(jìn)程。

其次，MonoSynth 利用了 Datalog 的單調(diào)性 ，能夠在部分規(guī)則選擇 （partial candidate rule selections）上主動(dòng)報(bào)告沖突 。
而 ProSynth 只有在 SAT 求解器生成了一個(gè)完整的規(guī)則選擇 之后才會(huì)發(fā)現(xiàn)沖突。

在部分規(guī)則選擇上報(bào)告沖突本身就是一個(gè)潛在的優(yōu)勢(shì)，同時(shí)也使得 MonoSynth 使用 ProSynth 的 delta-debugging 技術(shù)生成 why-not 沖突的成本更低：
ProSynth 必須從完整規(guī)則選擇中排除的所有規(guī)則中進(jìn)行過(guò)濾，而 MonoSynth 只需從當(dāng)前部分賦值中被標(biāo)記為負(fù)的規(guī)則中進(jìn)行過(guò)濾。

相關(guān)地，ProSynth 的實(shí)現(xiàn)可以一次報(bào)告多個(gè)沖突 ，而如第 4.3 節(jié)所述，MonoSynth 每次部分賦值只報(bào)告一個(gè)沖突 。

總體而言，MonoSynth 相比 ProSynth 實(shí)現(xiàn)了良好的加速效果（見(jiàn)第 7 節(jié)）。

• MonoSynth-Z3

  相比 ProSynth-Z3 平均實(shí)現(xiàn)了約 2 倍的加速 （最小 / 中位數(shù) / 幾何平均 / 最大值：0.03× / 2.07× / 1.83× / 21.94×）；

• MonoSynth-CVC4

  相比 ProSynth-CVC4 平均實(shí)現(xiàn)了接近一個(gè)數(shù)量級(jí)的加速（0.74× / 9.08× / 9.06× / 103.30×）。

5 放棄單調(diào)性：借鑒基于 SAT 的 ASP 思想

MonoSynth 利用了 Datalog 的單調(diào)性來(lái)求解包含 Datalog 謂詞的 SMT 公式。在本節(jié)中，我們轉(zhuǎn)而利用 Datalog 在答案集編程 （ASP）中的嵌入能力——這是一種非單調(diào) 的編程范式（見(jiàn)第 5.1 節(jié)）。

我們借鑒了一個(gè)現(xiàn)有的用于 ASP 的算法，展示了如何使用現(xiàn)成的 SAT 求解器來(lái)求解包含 Datalog 謂詞的 SAT 公式（見(jiàn)第 5.2 節(jié)），并將其應(yīng)用于綜合問(wèn)題（見(jiàn)第 5.3 節(jié)）。

5.1 背景知識(shí)：基于 SAT 的 ASP 求解

答案集編程 （Answer Set Programming, ASP）是一種用于解決某些類型搜索問(wèn)題的邏輯編程范式 [Brewka 等 2011；Gelfond 和 Lifschitz 1988]。在表達(dá)力上，ASP 介于 Datalog 和 Prolog 之間：

• ASP 程序總是終止的（不像 Prolog），但能解決 NP 難問(wèn)題（不像 Datalog，它屬于 PTIME 類別 [Papadimitriou 1985；Vardi 1982]）。

盡管現(xiàn)代 ASP 系統(tǒng)支持豐富的附加特性，但在最簡(jiǎn)單的形式下，ASP 就是語(yǔ)法上的 Datalog，只不過(guò)在規(guī)則體中加入了“失敗即否定”（negation-as-failure）的文字 not (t)。

否定文字的加入帶來(lái)了語(yǔ)義上的困難（不再保證存在最小 Herbrand 模型），為此提出了多種解決方案，例如：

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

• 完備語(yǔ)義（well-founded semantics）[Van Gelder 等 1991]，

• 以及穩(wěn)定模型語(yǔ)義（stable model semantics）[Gelfond 和 Lifschitz 1988]，這是 ASP 的基礎(chǔ)。

在穩(wěn)定模型語(yǔ)義下，一個(gè) ASP 問(wèn)題可以有零個(gè)、一個(gè)或多個(gè)解，這些解被稱為答案集 （answer sets）。一個(gè)答案集是一個(gè)受限的模型：模型中為真的每個(gè)原子都必須被解釋，并且這種解釋不能假設(shè)原子本身為真（見(jiàn)表 1）。

要判斷一組基礎(chǔ)原子集合 是否是程序 的一個(gè)答案集，步驟如下：

Datalog 可以嵌入到 ASP 中：
每一個(gè) Datalog 程序，只要給定一個(gè) EDB（外延數(shù)據(jù)庫(kù)），就可以被解釋為一個(gè)具有 唯一答案集 的 ASP 程序，該答案集對(duì)應(yīng)于 EDB 與 IDB 的并集。

ASP 求解通常分為兩個(gè)階段：

1. 首先，使用專門的“實(shí)例化器”（grounder）對(duì)輸入的 ASP 程序進(jìn)行 實(shí)例化 （見(jiàn)第 5.1.1 節(jié)）；

2. 然后，使用基于 SAT 的技術(shù)來(lái)尋找該實(shí)例化程序的 穩(wěn)定模型 。

在這里，我們借鑒了 ASSAT 算法 [Lin 和 Zhao 2004]，它使用現(xiàn)成的 SAT 求解器來(lái)計(jì)算答案集（見(jiàn)第 5.1.2 節(jié)）；我們?cè)诘?6 節(jié)中討論其他替代方案。

5.1.1 實(shí)例化（Grounding）

大多數(shù) ASP 求解過(guò)程的第一步是對(duì)源程序進(jìn)行實(shí)例化 。我們并不需要生成精確的實(shí)例化程序，而只需要生成在穩(wěn)定模型語(yǔ)義下等價(jià)的程序即可。

現(xiàn)代實(shí)例化器 [Calimeri 等 2017；Gebser 等 2011a] 使用半樸素求值 來(lái)進(jìn)行部分求值，從而生成更小的實(shí)例化程序。

例如，Gringo [Gebser 等 2011a, 2007] 在示例 5.1 上生成的簡(jiǎn)化實(shí)例化程序如下：

盡管進(jìn)行了優(yōu)化，但基底化（grounding）仍然是解決某些ASP（Answer Set Programming，即答案集編程）問(wèn)題的主要瓶頸。值得注意的是，基底化將一個(gè)一階邏輯程序轉(zhuǎn)換為命題邏輯程序，因?yàn)槊總€(gè)基底原子()都可以被視為一個(gè)命題變量。

5.1.2 ASSAT。ASSAT算法（Lin和Zhao，2004）使用現(xiàn)成的SAT求解器為基底程序計(jì)算答案集。由于程序是基底化的，以下我們將所有原子、視為命題原子。對(duì)于形式為 :- 1, . . . , 的規(guī)則，令?()為，()為{1, . . . , }的集合或合取式ó ，具體取決于上下文。

ASSAT的第一步是構(gòu)建基底程序的Clark完備化（Clark 1977），將基底程序的原子編碼為命題邏輯：對(duì)于基底程序中的每個(gè)基底原子，構(gòu)建方程 ≡ ?{() | ∈ , ?() = }。的Clark完備化是根據(jù)導(dǎo)出的所有此類方程的集合。

5.2 我們的實(shí)現(xiàn)

ASSAT 是一種用于求解 ASP（Answer Set Programming，答案集程序）問(wèn)題的算法。我們的工具對(duì)其進(jìn)行了改進(jìn)，以求解包含 Datalog 謂詞 （更一般地說(shuō)，是 ASP 謂詞）的 SAT/SMT 公式。

我們?cè)?Python 中實(shí)現(xiàn)了兩個(gè)版本：一個(gè)使用 Z3 的綁定 ，另一個(gè)使用 CVC4 的綁定 。這兩個(gè)版本都對(duì)外暴露了一個(gè)“編碼器”（encoder）接口，該編碼器封裝了一個(gè) SMT 求解器實(shí)例，并根據(jù)一個(gè) Datalog 程序和一組可能的輸入元組進(jìn)行構(gòu)造。

編碼器使用 Gringo [Gebser et al. 2011a, 2007] 來(lái)對(duì)程序進(jìn)行實(shí)例化（即“接地”）。它直接對(duì)規(guī)則進(jìn)行編碼，同時(shí)將每一個(gè)可能的輸入元組 p(c)編碼為一個(gè) ASP 的選擇規(guī)則（choice rule）：{p(c)}。

這個(gè)選擇規(guī)則是以下兩條規(guī)則的簡(jiǎn)寫(xiě)形式：

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

其中，原子 q 是程序中其他地方不出現(xiàn)的輔助原子，表示選擇是否不在答案集中包含 p(c)。

從 Gringo 生成的實(shí)例化程序出發(fā)，我們的工具構(gòu)建其 Clark 補(bǔ)全（completion） 并將其斷言給 SAT 求解器。

客戶端可以向編碼器傳入一個(gè) Datalog 事實(shí)，并獲得一個(gè)與之對(duì)應(yīng)的布爾 SAT 變量，該變量可以在任意 SAT 公式中使用。

編碼器提供了一個(gè)方法，用于檢查底層求解器狀態(tài)在穩(wěn)定模型語(yǔ)義下的可滿足性；它按照 ASSAT 算法的方式工作：

1. 使用 SAT 求解器迭代地生成一個(gè)模型；

2. 使用 Datalog 求解器對(duì)其進(jìn)行驗(yàn)證；

3. 如有必要，則添加循環(huán)公式（loop formulas）來(lái)排除非穩(wěn)定模型。

出于方便考慮，我們的實(shí)現(xiàn)在這里使用 Gringo 作為 Datalog 求解器；它也可以同樣使用 Soufflé 。它只報(bào)告一個(gè)循環(huán)公式：即針對(duì) SAT 模型中那些地原子（ground atoms）在正向依賴圖中構(gòu)成的強(qiáng)連通分量（SCC）中的最小者——這些原子包含在 SAT 模型中，但被排除在最小模型之外。

5.3 編碼合成

我們的工具 LoopSynth 使用上述系統(tǒng)來(lái)解決 Datalog 合成中的規(guī)則選擇問(wèn)題 （如圖5所示）。

給定一個(gè)基準(zhǔn)問(wèn)題，它首先將 Soufflé 程序（包含候選規(guī)則）解析為抽象語(yǔ)法樹(shù)（AST）表示，然后用示例輸入對(duì)其進(jìn)行擴(kuò)充，并將結(jié)果連同規(guī)則元組集合一起傳遞給基于 ASSAT 的編碼器。

接著，該工具使用編碼器對(duì)問(wèn)題規(guī)范中指定的每一個(gè)期望元組（desired tuple）和非期望元組（undesired tuple）進(jìn)行編碼，適當(dāng)?shù)財(cái)嘌悦總€(gè)返回的布爾 SAT 變量（或其否定）。

然后，向編碼器查詢一個(gè)模型；如果某個(gè)規(guī)則對(duì)應(yīng)的 SAT 變量在該模型中為真，則認(rèn)為該規(guī)則被選中。

5.3.2 與先前方法的比較

LoopSynth 的方法在幾個(gè)方面不同于之前的方法。首先，SAT 求解器確實(shí)能看到候選規(guī)則 ，因?yàn)檫@些規(guī)則作為斷言給求解器的 Clark 補(bǔ)全的一部分進(jìn)行了編碼。

其次，它調(diào)用 Datalog 引擎的頻率更低：每個(gè) SAT 調(diào)用只調(diào)用一次 Datalog 。而在 ProSynth 或 MonoSynth 中，一個(gè) SAT 賦值可能導(dǎo)致多次 Datalog 調(diào)用 ，用于生成出處（provenance）以構(gòu)建沖突信息。

與 MonoSynth 不同的是，LoopSynth 不是增量式的 ：SAT 求解器在獲得反饋之前會(huì)一次性猜測(cè)完整的規(guī)則選擇。

LoopSynth 在基準(zhǔn)測(cè)試套件上的性能表現(xiàn)參差不齊（第7節(jié)）。CVC4 版本相較于 ProSynth-CVC4 實(shí)現(xiàn)了顯著的加速（最小 / 中位數(shù) / 幾何平均 / 最大加速比：0.00× / 6.61× / 3.14× / 83.87×），但落后于 MonoSynth-CVC4（0.00× / 0.34× / 0.35× / 13.81×）；在 40 個(gè)基準(zhǔn)測(cè)試中，LoopSynth-CVC4 在所有基于 CVC4 的工具中擁有最快的平均運(yùn)行時(shí)間 ，其中有 11 個(gè)測(cè)試表現(xiàn)最佳。

然而，LoopSynth-Z3 相較于 ProSynth-Z3（0.00× / 0.19× / 0.24× / 25.67×）和 MonoSynth-Z3（0.00× / 0.10× / 0.13× / 7.71×）都表現(xiàn)較差。即便如此，仍有一些基準(zhǔn)測(cè)試中，LoopSynth-Z3 的平均速度快于這兩個(gè)工具 。

6 只需一個(gè)音符就能命名那首曲子：在 ASP 中的直接編碼

現(xiàn)有的方法總是至少對(duì)某個(gè)系統(tǒng)進(jìn)行多次調(diào)用 ：

• ProSynth

  對(duì) Soufflé 和 SMT 求解器進(jìn)行了 多次調(diào)用 （見(jiàn)第3節(jié)）；

• 單調(diào)性理論方法

  只對(duì) SMT 求解器進(jìn)行 一次調(diào)用 ，但對(duì) Soufflé 進(jìn)行了 多次調(diào)用 （見(jiàn)第4節(jié)）；

• 借鑒基于 SAT 的 ASP 方法的思想，得到了一種對(duì) Datalog 調(diào)用次數(shù)大大減少、但仍需要對(duì) SAT 求解器進(jìn)行 多次調(diào)用 的方法（見(jiàn)第5節(jié)）。

如果我們能夠直接在 ASP 中對(duì)問(wèn)題進(jìn)行編碼 ，就可以一次性完成求解：只需進(jìn)行一次實(shí)例化（grounding）調(diào)用（相當(dāng)于 Datalog 的求值過(guò)程），以及一次ASP 求解器的調(diào)用 即可。

6.1 編碼合成

我們將數(shù)據(jù)目錄合成表述為一個(gè)ASP程序。我們對(duì)規(guī)則選擇和最小化的編碼是ASP程序合成工具ASPAL [Corapi et al. 2011] 用于實(shí)例化骨架ASP規(guī)則的編碼的專門化版本，修改為使用輔助關(guān)系來(lái)編碼輸出示例。

接著，我們添加硬性約束（hard constraints）來(lái)限制合成程序的輸出（見(jiàn)圖6(a,b)）。

一個(gè)硬性約束是一個(gè) 無(wú)頭規(guī)則（headless rule） ；任何使該規(guī)則體為真的答案集都會(huì)被拒絕。

約束 (C+) 要求所有正例都必須被推導(dǎo)出來(lái)，
而約束 (C?) 確保沒(méi)有任何負(fù)例被推導(dǎo)出來(lái)。

這些硬性約束共同作用，迫使所選規(guī)則符合問(wèn)題規(guī)范。

與 LoopSynth 類似，我們可以使用 ASP 的選擇規(guī)則（choice rules）直接對(duì)規(guī)則選擇進(jìn)行編碼（見(jiàn)圖6(c)）：
rule(n) 可以出現(xiàn)在答案集中，也可以不出現(xiàn)。

實(shí)際上，ASP 求解器會(huì)自行選擇規(guī)則。
因此，計(jì)算出的答案集就回答了我們的 Datalog 合成問(wèn)題：
當(dāng)且僅當(dāng) rule(n) 出現(xiàn)在答案集中時(shí)，規(guī)則 n 應(yīng)被包含在合成的 Datalog 程序中 。

6.1.4 與先前方法的比較

ASPSynth （見(jiàn)圖8）只進(jìn)行一次“Datalog”調(diào)用（實(shí)例化）和一次“SAT”調(diào)用（ASP 求解） ，這與之前的方法不同。

它在表達(dá)能力上不如 MonoSynth 和 LoopSynth ，因?yàn)楹髢烧呖梢郧蠼獍?Datalog 謂詞的任意 SMT 公式。

然而，現(xiàn)代 ASP 求解器使得以下兩點(diǎn)變得非常容易：
(a) 避免顯式枚舉所有非期望元組 （這在 MonoSynth 和 LoopSynth 中是必需的）；
(b) 對(duì)解的最小化進(jìn)行編碼 （即尋找最簡(jiǎn)規(guī)則集）。

與其他工具相比，ASPSynth 將整個(gè)合成問(wèn)題 ——包括候選規(guī)則和規(guī)范要求——都統(tǒng)一編碼為一個(gè)整體形式 ，可以一次性求解。這種方式允許在選擇候選規(guī)則與根據(jù)規(guī)范檢查這些選擇的后果之間進(jìn)行增量式的交互 。

6.2 實(shí)現(xiàn)

我們以兩種系統(tǒng)實(shí)現(xiàn)了這種直接編碼方法：ASPSynth-Clingo 和 ASPSynth-WASP ，
它們分別使用了 ASP 求解器 Clingo v5.4.0 [Gebser 等人，2011b] 和 WASP v2.0 [Alviano 等人，2013]。
這兩個(gè)系統(tǒng)都使用了實(shí)例化工具 Gringo v5.4.0 [Gebser 等人，2011a, 2007]。

Clingo 在內(nèi)部運(yùn)行 Gringo：從技術(shù)上講，“Clingo”指的是由 Gringo 和求解器 Clasp [Gebser 等人，2012] 組成的完整系統(tǒng) 。
對(duì)于 ASPSynth-WASP ，我們則是單獨(dú)運(yùn)行 Gringo ，然后將結(jié)果通過(guò)管道傳遞給 WASP。

無(wú)論是 Clingo 還是 WASP，它們都是“原生的（native） ” ASP 求解器：
它們是專門設(shè)計(jì)的求解器，使用了類似 SAT 的技術(shù)，但不會(huì)將任務(wù)委派給外部的 SAT 求解器 。

直接使用 ASP 編碼的方法在基準(zhǔn)測(cè)試套件中整體表現(xiàn)最佳。
WASP 相較于 ProSynth-Z3 有大約 3 倍的平均加速比 （最小 / 中位數(shù) / 幾何平均 / 最大加速比：0.03× / 2.63× / 3.62× / 186.10×），
相較于 MonoSynth-Z3 有大約 2 倍的平均加速比 （0.07× / 1.64× / 1.98× / 247.98×）。

而 Clingo 的表現(xiàn)更優(yōu)：
相較于 ProSynth-Z3 實(shí)現(xiàn)了大約 9 倍的平均加速比 （1.16× / 7.50× / 9.47× / 372.19×），
相較于 MonoSynth-Z3 實(shí)現(xiàn)了大約 5 倍的平均加速比 （0.33× / 3.88× / 5.17× / 513.80×）。

下一節(jié)將給出詳細(xì)的評(píng)估結(jié)果。

7評(píng)估

我們通過(guò) ProSynth 基準(zhǔn)測(cè)試套件 對(duì)所開(kāi)發(fā)的方法進(jìn)行了實(shí)證評(píng)估。我們的基準(zhǔn)測(cè)試結(jié)果報(bào)告了十次運(yùn)行的平均值；實(shí)驗(yàn)在一個(gè)空閑的 Ubuntu 20.04 AWS 服務(wù)器上進(jìn)行，該服務(wù)器配有 32 個(gè) vCPU（主頻為 3.1 GHz）、128 GiB 內(nèi)存和 600 GiB SSD 存儲(chǔ)空間。我們使用的是 Z3 v4.8.15 和 CVC4 v1.8。每個(gè)單獨(dú)的基準(zhǔn)測(cè)試在運(yùn)行超過(guò)十分鐘（600 秒）后將超時(shí)。所有基準(zhǔn)測(cè)試和實(shí)驗(yàn)?zāi)_本都包含在論文的附加工件中 [Bembenek 等人, 2022]。

我們將 ProSynth 作為基線進(jìn)行比較。我們對(duì)原始論文附加工件中的 ProSynth 版本進(jìn)行了輕微修改，以記錄并輸出額外的統(tǒng)計(jì)信息，并對(duì) SMT 符號(hào)名稱進(jìn)行隨機(jī)化處理。SMT 符號(hào)名稱的選擇可能會(huì)對(duì)求解器性能產(chǎn)生顯著（且任意的）影響，我們不希望 ProSynth 因?yàn)檫@些本質(zhì)上是隨意的求解器相關(guān)因素而受到不公平的優(yōu)勢(shì)或劣勢(shì)影響。（我們?cè)诨?SMT 的其他工具中也對(duì)符號(hào)名稱進(jìn)行了類似的隨機(jī)化處理。）

此外，我們還創(chuàng)建了一個(gè)使用 CVC4 而非 Z3 的 ProSynth 替代版本；這涉及到從 Z3 的 Python 綁定遷移到 CVC4 的一些語(yǔ)法上的小改動(dòng)。我們修改后的 ProSynth-Z3 版本與原始版本性能相當(dāng)，并明顯優(yōu)于 CVC4 版本（最小 / 中位數(shù) / 幾何平均 / 最大加速比：0.68× / 3.97× / 5.27× / 174.02×）。

每種方法都有其表現(xiàn)良好的用例，但直接的 ASP 編碼方法 —— 尤其是 ASPSynth-Clingo —— 在整個(gè)基準(zhǔn)測(cè)試套件中表現(xiàn)最佳（見(jiàn)圖9；表7）。ASP 編碼整體表現(xiàn)出較快的性能。

其中，ASPSynth-Clingo 表現(xiàn)最優(yōu) ：它沒(méi)有明顯的性能較差的異常情況，在每一個(gè)基準(zhǔn)測(cè)試中都能在不到一秒的時(shí)間內(nèi)返回結(jié)果 ；即使當(dāng)它不是最快的工具時(shí)，它也僅比最快者慢 0.02 秒。

接下來(lái)的內(nèi)容中，我們將描述基準(zhǔn)測(cè)試套件（第 7.1 節(jié)），并對(duì)每種方法的表現(xiàn)進(jìn)行詳細(xì)分析（第 7.2、7.3 和 7.4 節(jié)），最后將在更廣泛的背景下評(píng)估 ASPSynth-Clingo（第 7.5 節(jié)）。

7.1 基準(zhǔn)測(cè)試套件

我們使用的是 ProSynth 的基準(zhǔn)測(cè)試套件 ，它源自為 ALPS [Si 等人, 2018] 開(kāi)發(fā)的測(cè)試集，并隨后被 DiffLog [Si 等人, 2019] 所采用。

該套件包含不同輸出關(guān)系的預(yù)期輸出元組文件，以及一個(gè) Soufflé 程序，其中包含了由 ALPS 生成的候選規(guī)則（每條規(guī)則都擴(kuò)展了一個(gè) rule(n) 前提）。

Soufflé 程序會(huì)被編譯成可執(zhí)行文件（用于 ProSynth）或共享庫(kù)（用于 MonoSynth）。
對(duì)于規(guī)范中的每一個(gè)輸出關(guān)系，我們還生成其補(bǔ)關(guān)系中的元組集合（MonoSynth 和 LoopSynth 要求顯式枚舉所有不期望的元組）。

該測(cè)試套件共包含 40 個(gè)基準(zhǔn)測(cè)試 ，其中包括：

• 14 個(gè)知識(shí)發(fā)現(xiàn)任務(wù)
• 11 個(gè)程序分析任務(wù)
• 15 個(gè)關(guān)系代數(shù)任務(wù)

規(guī)則集的大小從 5 條規(guī)則到 688 條規(guī)則 不等。
有關(guān)完整描述，請(qǐng)參見(jiàn) ProSynth 論文中的表1和表2 [Raghothaman 等人, 2020]。

7.2 MonoSynth

MonoSynth-Z3 相較于 ProSynth-Z3 實(shí)現(xiàn)了大約 2 倍的平均加速比 （最小 / 中位數(shù) / 幾何平均 / 最大加速比：0.03× / 2.07× / 1.83× / 21.94×），
而 MonoSynth-CVC4 相較于 ProSynth-CVC4 實(shí)現(xiàn)了接近一個(gè)數(shù)量級(jí)的平均加速比 （0.74× / 9.08× / 9.06× / 103.30×）。

雖然 CVC4 的結(jié)果顯示出明顯的改進(jìn)，但 Z3 的結(jié)果則更為模糊：
MonoSynth-Z3 的性能在不同基準(zhǔn)測(cè)試之間差異較大 ，而且大多數(shù)對(duì) ProSynth-Z3 的加速（27 項(xiàng)中有 20 項(xiàng)）發(fā)生在那些 ProSynth-Z3 已經(jīng)很快的任務(wù)上（即在不到一秒內(nèi)完成的任務(wù)）。

我們懷疑是我們?cè)谶x擇沖突時(shí)使用的啟發(fā)式方法可能與 Z3 的搜索策略產(chǎn)生了不良交互：
ProSynth-Z3 通常進(jìn)行數(shù)十次 Datalog 調(diào)用 ，而 MonoSynth-Z3 則進(jìn)行數(shù)百次調(diào)用 。
在那些 ProSynth-Z3 更快的任務(wù)（如 downcast、polysite 和 sql-10）上，這種大量調(diào)用尤其有害，因?yàn)樵谶@些任務(wù)中每次 Datalog 調(diào)用的平均耗時(shí)更長(zhǎng)。

ProSynth-CVC4 和 MonoSynth-CVC4 的 Datalog 調(diào)用次數(shù)與 MonoSynth-Z3 大致相同。

四種工具的大部分時(shí)間都花在了 Datalog 求解 上，而在 SAT 求解 上幾乎沒(méi)有花費(fèi)時(shí)間。這并不令人意外，因?yàn)闊o(wú)論是 ProSynth 還是 MonoSynth，一般都需要在每個(gè)沖突中調(diào)用 Datalog 求解器多次（需要多次 Datalog 調(diào)用來(lái)計(jì)算“為何未推導(dǎo)出”的出處信息），而傳遞給 SAT 求解器的阻塞約束并不特別復(fù)雜。

盡管兩種 MonoSynth 版本相對(duì)于各自的基線（即 ProSynth-Z3 和 ProSynth-CVC4）表現(xiàn)出不同的性能提升，但從整體來(lái)看，它們彼此之間的平均表現(xiàn)是相當(dāng)?shù)摹?/p>

正如第 4.3 節(jié)所指出的那樣，MonoSynth 并不需要在每個(gè)部分賦值上都檢查沖突 。
在實(shí)驗(yàn)中，我們會(huì)在檢查沖突前先緩存五個(gè)布爾參數(shù)的賦值。
緩存越小，報(bào)告沖突的速度就越快，但也會(huì)導(dǎo)致更多的 Datalog 調(diào)用（盡管這些調(diào)用在同一操作系統(tǒng)進(jìn)程中進(jìn)行，但仍代價(jià)不低）。
在我們的實(shí)驗(yàn)中，設(shè)置緩存大小為 5 似乎達(dá)到了一個(gè)合理的平衡。
然而，在所有基準(zhǔn)測(cè)試中它遠(yuǎn)非最優(yōu)，我們預(yù)計(jì)如果采用更復(fù)雜的緩沖啟發(fā)式方法（例如根據(jù)問(wèn)題特征動(dòng)態(tài)調(diào)整緩存大小），可能會(huì)帶來(lái)顯著的性能提升。

7.3 LoopSynth

LoopSynth 的表現(xiàn)因所使用的求解器不同而有所差異，結(jié)果呈現(xiàn)出混合狀態(tài)。

在使用 CVC4 的情況下，LoopSynth 的整體表現(xiàn)較為積極：它相比 ProSynth 實(shí)現(xiàn)了顯著的平均加速（最小 / 中位數(shù) / 幾何平均 / 最大加速比：0.00× / 6.61× / 3.14× / 83.87×），但落后于 MonoSynth（0.00× / 0.34× / 0.35× / 13.81×）。總體而言，在所有基于 CVC4 的工具中，LoopSynth-CVC4 在 40 個(gè)基準(zhǔn)測(cè)試中的 11 個(gè)上擁有最快的平均運(yùn)行時(shí)間。

而在使用 Z3 的情況下，LoopSynth 的表現(xiàn)則相對(duì)較差，與 ProSynth（0.00× / 0.19× / 0.24× / 25.67×）和 MonoSynth（0.00× / 0.10× / 0.13× / 7.71×）相比均處于劣勢(shì)。即便如此，LoopSynth-Z3 在 40 個(gè)基準(zhǔn)測(cè)試中的 3 個(gè)上仍然是所有 Z3 工具中最快的，并且在這兩個(gè)工具上分別實(shí)現(xiàn)了最高達(dá) 26 倍 和 8 倍 的加速。

LoopSynth 方法最大的問(wèn)題或許是其不可靠性 ：

• Z3 版本在 21 次測(cè)試中出現(xiàn)超時(shí) （涉及 3 個(gè)基準(zhǔn)測(cè)試），

• CVC4 版本在 35 次測(cè)試中出現(xiàn)超時(shí) （涉及 4 個(gè)基準(zhǔn)測(cè)試）。在這些情況下，算法未能生成足夠的循環(huán)公式來(lái)迫使求解器在合理時(shí)間內(nèi)收斂到一個(gè)穩(wěn)定模型。

與 ProSynth 和 MonoSynth 相比，LoopSynth 將時(shí)間分布從 Datalog 求解 轉(zhuǎn)移到了 SMT 求解 上。

排除超時(shí)結(jié)果以及耗時(shí)小于一秒的測(cè)試后發(fā)現(xiàn)：

• LoopSynth-Z3

  在 Datalog 求解上花費(fèi)的時(shí)間比例大致與其在 SMT 求解上的比例相當(dāng)：

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

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

• LoopSynth-CVC4

  則在 SMT 求解上花費(fèi)了更多時(shí)間：

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

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

其余大部分時(shí)間用于編碼 Clark 補(bǔ)全 和 構(gòu)造循環(huán)公式 。

在 40 個(gè)基準(zhǔn)測(cè)試中，有 15 個(gè)是“緊致”（tight）的，因此不需要任何循環(huán)公式。對(duì)于其余未超時(shí)的測(cè)試：

• LoopSynth-Z3

  和 LoopSynth-CVC4 大多數(shù)情況下只需生成少量循環(huán)公式，但在某些不良情況下可生成數(shù)百甚至上千個(gè)：

• • LoopSynth-Z3：最少 / 中位數(shù) / 平均 / 最多 = 0.00 / 2.00 / 28.99 / 442.30

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

每個(gè)循環(huán)公式都會(huì)觸發(fā)一次 Datalog 調(diào)用；由于 Datalog 調(diào)用次數(shù)相對(duì)較少，這在一定程度上緩解了 LoopSynth 使用 Gringo 解釋執(zhí)行 Datalog 程序（而非像 ProSynth 和 MonoSynth 那樣調(diào)用 Soufflé 編譯后的高效程序）所帶來(lái)的性能劣勢(shì)。

7.4 ASPSynth

直接使用 ASP 編碼的方法是基準(zhǔn)測(cè)試套件上最有效的解決方案。

ASPSynth-Clingo 在每次測(cè)試中都在一秒內(nèi)完成任務(wù) ，它在 40 個(gè)基準(zhǔn)測(cè)試中的 26 個(gè) 上平均表現(xiàn)最快，并且相比 ProSynth-Z3 實(shí)現(xiàn)了大約 9 倍的平均加速比 （最小 / 中位數(shù) / 幾何平均 / 最大加速比：1.16× / 7.50× / 9.47× / 372.19×）。

ASPSynth-WASP 的表現(xiàn)也很穩(wěn)健，相比 ProSynth-Z3 實(shí)現(xiàn)了大約 3 倍的平均加速比 （0.03× / 2.63× / 3.62× / 186.10×）。然而，它在 sql-15 基準(zhǔn)測(cè)試上持續(xù)超時(shí) 。有趣的是，LoopSynth 的兩個(gè)版本也出現(xiàn)了同樣的問(wèn)題：可能該基準(zhǔn)測(cè)試中的循環(huán)結(jié)構(gòu)對(duì)某些基于 ASP 的方法來(lái)說(shuō)難以處理。

是什么讓直接面向 ASP 的工具 比其他方法更有效？一個(gè)不應(yīng)忽視的因素是：Clingo 和 WASP 是經(jīng)過(guò)多年優(yōu)化的高度成熟、工程化的工具 ，而其他方法則是臨時(shí)構(gòu)建、尚未高度優(yōu)化的實(shí)現(xiàn)。

Clingo 和 WASP 避免了其他實(shí)現(xiàn)所面臨的一些開(kāi)銷，例如：

• 多個(gè)操作系統(tǒng)進(jìn)程之間的切換，

• 或不同系統(tǒng)之間（如 Z3 與 Soufflé）在內(nèi)存中的表示轉(zhuǎn)換。

同樣地，ASPSynth 不需要多次執(zhí)行 Horn 子句求值： 它只需進(jìn)行一次程序?qū)嵗╣rounding），而其他工具則要運(yùn)行顯式的 Datalog 求值過(guò)程來(lái)檢查每個(gè)提議解是否滿足最小模型語(yǔ)義。

此外，ASP 求解器內(nèi)部將 Horn 子句求解與 SAT 搜索緊密結(jié)合 ，使其能更有效地探索解空間。

為了理解這一點(diǎn)，我們可以觀察每種方法向 SAT 求解器中添加了多少公式以引導(dǎo)其找到解；一般來(lái)說(shuō)，這個(gè)數(shù)字越高，說(shuō)明 SAT 求解器探索了越多無(wú)用的搜索空間。

為簡(jiǎn)潔起見(jiàn)，我們將這些公式統(tǒng)稱為“沖突”（conflicts）；它們的具體定義因工具而異，因此比較時(shí)不能完全等同（例如，LoopSynth 生成的一個(gè)循環(huán)公式可能轉(zhuǎn)化為 SAT 求解器中的多個(gè)子句；我們對(duì) ProSynth 所遇到的沖突數(shù)量進(jìn)行了低估，因?yàn)橐淮?CEGIS 迭代可能涉及多個(gè)沖突）。

盡管如此，這些數(shù)據(jù)仍有助于我們了解不同算法的性能差異（見(jiàn)表3）：

• ProSynth 和 MonoSynth 方法

  遇到的沖突數(shù)量大致相同；

• LoopSynth 方法

  平均遇到一或更少的沖突（中位數(shù)），但在不良情況下也可能遇到大量沖突；

• 直接 ASP 編碼方法

  平均遇到的沖突最少，其中位數(shù)為 零沖突 。

不僅如此，它們?cè)跇?gòu)造沖突解釋時(shí)也更加高效，因?yàn)椤幌?ProSynth 或 MonoSynth——它們不需要調(diào)用 Datalog 求解器來(lái)生成出處信息。

因此，直接的 ASP 編碼方法擁有一種“雙贏”的組合優(yōu)勢(shì)：遇到的沖突更少，且計(jì)算這些沖突的成本更低 。

7.5 更廣闊的視角：ASPSynth-Clingo 有多高效？

我們工作的一個(gè)貢獻(xiàn)是對(duì)基于求解器的 Datalog 合成（作為規(guī)則選擇問(wèn)題）算法設(shè)計(jì)空間進(jìn)行探索。然而，既然我們已經(jīng)找到了一個(gè)占主導(dǎo)地位的解決方案——ASPSynth-Clingo ，我們就可能會(huì)好奇它與其他可能的技術(shù)相比表現(xiàn)如何。

本節(jié)進(jìn)一步評(píng)估 ASPSynth-Clingo 在解決 Datalog 合成（作為規(guī)則選擇）問(wèn)題上的有效性。總體而言，我們發(fā)現(xiàn)它在 ProSynth 基準(zhǔn)測(cè)試套件上表現(xiàn)非常出色，并且相較于基于候選規(guī)則集的其他方法具有良好的擴(kuò)展性。我們還提出了一些克服當(dāng)前局限性的建議。

7.5.1 參與比較的工具

在程序合成中，解的質(zhì)量 至關(guān)重要。

我們?cè)u(píng)估了兩個(gè)版本的 ASPSynth-Clingo ：

• 原始版本

  （不進(jìn)行解最小化）

• ASPSynth-Clingo-MinPremise

  （最小化解中的前提數(shù)量，見(jiàn)第6.1.2節(jié)）

我們還將它與 GenSynth [Mendelson et al. 2021] 、ILASP2 [Law et al. 2015] 的編碼版本 和 ProSynth 進(jìn)行了比較。

GenSynth 是一種 Datalog 合成工具，它使用遺傳編程算法生成候選規(guī)則，而不是從預(yù)定義的規(guī)則集中選擇。與其它從候選規(guī)則集中選擇的方法相比，這種方法在某些情況下是劣勢(shì)（當(dāng)候選規(guī)則集較小時(shí)），在另一些情況下則是優(yōu)勢(shì)（當(dāng)候選規(guī)則集很大或難以過(guò)濾時(shí)）。

GenSynth 的論文報(bào)告了其相對(duì)于某個(gè)使用 Soufflé 解釋模式的 ProSynth 版本的加速效果（通常 ProSynth 是與 Soufflé 編譯出的可執(zhí)行文件交互的）；但 GenSynth 的評(píng)估并未包含與使用編譯后 Soufflé 程序的 ProSynth 的對(duì)比。GenSynth 自身也是使用 Soufflé 的解釋模式，并嘗試最小化解。

ILASP2 [Law et al. 2015] 使用元級(jí)方法將 ASP 程序合成建模為 ASP 程序，并將其提交給 Clingo 求解。由于 Datalog 是 ASP 的一個(gè)片段，我們可以自然地在 ILASP2 中對(duì) Datalog 合成進(jìn)行編碼，類似于第6節(jié)中的直接 ASP 編碼方式（ILASP 允許顯式枚舉候選規(guī)則，因此我們省略了 rule(n) 原子和選擇規(guī)則）。

在配置 ILASP2 時(shí)，我們將合成程序中字面量數(shù)目的上限設(shè)為 30，這是默認(rèn)值的兩倍（能工作的最小值是 28）。與 ASPSynth 相比，ILASP2 生成了更復(fù)雜的 ASP 程序（涉及元級(jí)機(jī)制），并調(diào)用了兩次 Clingo（而不是一次）。ILASP2 也最小化了解中的前提數(shù)量。

作為基線，我們使用了一個(gè)輕微修改后的 Raghothaman 等人 [2020] 的 ProSynth 實(shí)現(xiàn)版本（關(guān)閉日志記錄并收集額外統(tǒng)計(jì)數(shù)據(jù)）。原始的 ProSynth 論文沒(méi)有報(bào)告 Soufflé 編譯候選規(guī)則集所需的時(shí)間（編譯每組規(guī)則只進(jìn)行一次，生成的可執(zhí)行文件被多次調(diào)用）。為了專注于基于求解器的方法部分，在前一節(jié)中我們忽略了 ProSynth 和 MonoSynth 的編譯時(shí)間。但在本節(jié)中，我們分別報(bào)告了 ProSynth 包含和不包含編譯時(shí)間的運(yùn)行時(shí)間，因?yàn)槿绻獜念^開(kāi)始使用 ProSynth 來(lái)合成程序，就必須編譯候選規(guī)則。

7.5.2 測(cè)試基準(zhǔn)

我們使用了兩組基準(zhǔn)測(cè)試：

第一組是第7.1節(jié)中討論的 40 個(gè) ProSynth 基準(zhǔn)測(cè)試 。

第二組是一組擴(kuò)展性基準(zhǔn)測(cè)試 ，用于評(píng)估候選規(guī)則數(shù)量和規(guī)范大小的變化對(duì)性能的影響。每個(gè)測(cè)試都試圖合成一個(gè)用于計(jì)算強(qiáng)連通分量（SCC）的程序。

對(duì)于候選規(guī)則，我們考慮了三種情況：

• 100 條規(guī)則

• 500 條規(guī)則

• 1000 條規(guī)則（取自 ProSynth 論文 [Raghothaman et al. 2020] 中的擴(kuò)展實(shí)驗(yàn)）

對(duì)于規(guī)范大小，我們考慮了三類 EDB（外延數(shù)據(jù)庫(kù)）：

• 10 個(gè)元組（scc-1x）

• 100 個(gè)元組（scc-10x）

• 1000 個(gè)元組（scc-100x）（取自 GenSynth 論文 [Mendelson et al. 2021] 中的擴(kuò)展實(shí)驗(yàn)）

我們考慮了所有規(guī)則集大小與規(guī)范大小的組合。

7.5.3 實(shí)驗(yàn)結(jié)果

在 ProSynth 基準(zhǔn)測(cè)試套件上，ASPSynth-Clingo 平均明顯快于其他方法 （見(jiàn)圖10(a)）。

與不計(jì) Soufflé 編譯時(shí)間的 ProSynth 相比，它顯著更快（最小 / 中位數(shù) / 幾何平均 / 最大加速比：0.65× / 7.58× / 9.33× / 828.86×），并且比 GenSynth 快幾個(gè)數(shù)量級(jí)（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×），這進(jìn)一步表明 ASP 非常適合這類 Datalog 合成任務(wù)。

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

前提最小化對(duì) ASPSynth-Clingo 的性能影響不大（相對(duì)于 -MinPremise 的加速比：中位數(shù) 1.00×，幾何平均 1.06×）。

GenSynth 產(chǎn)生的輸出是最小的 （無(wú)論是按規(guī)則還是前提數(shù)量衡量）。GenSynth 的解在前提數(shù)量上適度少于 ASPSynth-Clingo-MinPremise 和 ILASP2（中位數(shù) 1.00×，幾何平均 0.86×），大幅少于 ASPSynth-Clingo（中位數(shù) 0.67×，幾何平均 0.54×）和 ProSynth（中位數(shù) 0.67×，幾何平均 0.56×）。

當(dāng)我們改變候選規(guī)則數(shù)量和輸入/輸出示例數(shù)量時(shí)，GenSynth 的擴(kuò)展性最好 （見(jiàn)圖10(b)）。它在各種配置下表現(xiàn)相對(duì)穩(wěn)定（除了 scc-1x 超時(shí)），并在除最小配置外的所有配置上優(yōu)于 ProSynth。

基于 ASP 的方法在僅擴(kuò)展一個(gè)維度時(shí)擴(kuò)展性良好，但在同時(shí)擴(kuò)展兩個(gè)維度時(shí)落后于 GenSynth。最大的配置突出了 ASPSynth-Clingo、ASPSynth-Clingo-minpremise 和 ILASP2 之間的性能差異。

盡管 GenSynth 擴(kuò)展性較好，但它在基準(zhǔn)測(cè)試套件上的整體速度最慢（見(jiàn)圖10(a)）。

8 討論

我們討論 ASPSynth 的局限性（第 8.1 節(jié)），
基于求解器的算法之間的比較難點(diǎn)（第 8.2 節(jié)），
對(duì)規(guī)則選擇問(wèn)題的批評(píng)（第 8.3 節(jié)），
以及對(duì)該問(wèn)題的更廣泛視角（第 8.4 節(jié)）。

8.1 ASPSynth 的局限性

盡管 ASPSynth 的表現(xiàn)優(yōu)于其他解決方案，但它仍然存在幾個(gè)局限性。

實(shí)例化（grounding） 通常是基于 ASP 的邏輯程序合成工具的主要瓶頸 [Athakravi 等人, 2013；Cropper 和 Morel, 2021]。

ASPSynth 的性能會(huì)隨著規(guī)范（specification）規(guī)模的增大而下降，
這是由于地規(guī)則（ground rules）數(shù)量發(fā)生了組合爆炸；
如果 ASP 求解器能在惰性實(shí)例化（lazy grounding）與 SAT 技術(shù)之間更好地結(jié)合 [Weinzierl, 2017]，
ASPSynth 將從中受益。

ASPSynth 可以被擴(kuò)展以合成包含**分層否定（stratified negation）**的程序 [Apt 等人, 1988；Przymusinski, 1988；Van Gelder, 1989]，這是一種常見(jiàn)的 Datalog 對(duì)否定的處理方式，它禁止謂詞通過(guò)自身（無(wú)論是直接還是間接）的否定來(lái)定義自己。

合成帶有否定的程序本身并不是一個(gè)問(wèn)題（因?yàn)槲覀兊木幋a可以合成一般的 ASP 程序）。

為了確保我們只合成分層程序 ，我們可以添加一些 ASP 規(guī)則來(lái)定義謂詞之間的否定依賴關(guān)系 </...