EZSMT版本3，成熟版

# EZSMT 第3版，成熟版¹  
¹ 来源：https://arxiv.org/html/2607.13344  

## EZSMT 第3版，成熟版¹  

###### 摘要  

约束回答集编程（CASP）是一种混合推理范式，融合了回答集编程（ASP）、约束处理以及可满足性模理论（SMT），能够对复杂的组合搜索问题进行强大的声明式编码。本文介绍了ezsmtv3的设计与实现，这是一个基于SMT的可扩展CASP框架，推进了CASP求解的翻译式方法。在ezsmt+系统的基础上，ezsmtv3引入了更具表现力的输入语言，支持通过弱约束进行优化，并为新约束类型的便捷集成提供了基础。ezsmtv3不实现自定义搜索过程，而是利用cvc5、yices和z3等最先进的SMT求解器进行推理。本文提供了基准测试结果，将ezsmtv3与其CASP同类系统（如clingcon、clingo[DL]和clingo[LP]）进行比较，同时展示了其处理涉及整数和实数混合域约束的能力。该系统为CASP领域的未来扩展和理论探索提供了稳健的平台。正在考虑发表于《逻辑编程理论与实践》（TPLP）。  

###### 关键词：约束回答集编程，可满足性模理论  

## 1. 引言  

约束回答集编程（CASP）是自动推理中的一种混合方法，整合了回答集编程（Niemelä, 1999; Marek and Truszczyński, 1999; Brewka et al., 2011）、约束处理（Rossi et al., 2008; Jaffar and Maher, 1994）和可满足性模理论（Nieuwenhuis et al., 2006; Barrett et al., 2008; Barrett and Tinelli, 2014）等多个研究领域的进展。Elkabani等（2004）、Mellarkod等（2008）和Lierler（2014）等的工作是CASP的早期参考文献。CASP显示出巨大潜力，催生了众多求解器，例如acsolver（Mellarkod等，2008）、clingcon（Gebser等，2009b）、ezcsp（Balduccini and Lierler, 2017）、idp（Wittocx等，2008）、inca（Drescher and Walsh, 2010）、dingo（Janhunen等，2011）、mingo（Liu等，2012）、aspmt（Bartholomew and Lee, 2014）、clingo[LP]和clingo[DL]（Janhunen等，2017），以及ezsmt+（Susman and Lierler, 2016a; Shen and Lierler, 2018b）。CASP为声明式编程开辟了新的可能性，使其能够处理诸如列车调度和产品配置等复杂任务。

CASP求解器可根据构建策略大致分为集成式和翻译式两类。本文不仅描述了一个采用翻译式方法的求解器，更是一个可扩展的CASP框架，旨在简化该领域新系统的实现。本文介绍了可扩展的基于SMT的约束回答集编程框架ezsmt第3版（ezsmtv3）的设计、开发与实现。我们基于早期ezsmt+系统（Susman and Lierler, 2016a; Shen and Lierler, 2018b）中提出的初步愿景展开工作。具体而言，我们继续倡导自动推理领域中所谓的翻译式方法。ezsmtv3将CASP求解器ezsmt+背后的初步想法转化为一个成熟的、可扩展的CASP框架。因此，ezsmtv3不仅本身是一个求解器，还设计用于以简单、简洁的方式支持该系统对新约束类型的扩展。

简而言之，ezsmtv3系统计算约束回答集（CAS）程序的回答集，并支持多种约束类型。然而，在此过程中，它并不实现原生搜索过程。相反，它将给定的带约束原子的逻辑程序翻译成某种可满足性模理论（SMT）方言的公式。然后，该公式由现成的SMT求解器处理。

历史上，ezsmt+语言采用了为ezcsp系统（Balduccini and Lierler, 2017）开发的CASP语言约定。因此，其约束原子（由关键字`required`标记）仅限于规则头部，这使得某些领域的表示变得繁琐。虽然对于启动概念验证系统而言已经足够，但ezcsp的语言特性揭示了需要更具表现力和灵活性的替代方案。在我们的ezsmtv3工作中，我们找到了这样的替代方案。具体而言，它建立在clingo 5系列（Gebser等，2019; Kaminski等，2023）的发展之上，该系列倡导可扩展性哲学。clingo5系统提供了阐述新构造规范的方法，以便在其基础工具gringo中进行处理（Gebser等，2009a; Gebser, Martin等，2015; Kaminski, 2023）。此外，clingo5提供了集成自定义传播器的方法，以确保对新加入的语法语言特性进行正确处理。在本文中，我们采纳了clingo5的可扩展性哲学，但在搜索机制的自定义实现方面有所偏离。我们主张利用现有的最先进的自动推理工具，特别是SMT求解器。因此，本文依赖于CASP与SMT之间的理论发现以及SMT求解中的一系列复杂算法发展，这些算法产生了诸如cvc4（Barrett等，2011）、cvc5（Barrett等，2021）、z3（De Moura and Bjørner, 2008）和yices（Dutertre and De Moura, 2006）等杰出系统。相反，我们专注于创建与SMT技术的简洁接口。

我们的方法依赖于一个易于扩展的基于组件的架构，包括基础组件、翻译组件和基于SMT的求解组件。系统设计为一个多阶段处理流水线，每个组件的输出作为下一个组件的输入。基础组件的使用方式允许我们扩展现有的语言规范。翻译组件解释基础组件的输出，以支持从ASP到SMT的翻译——为将来无缝集成新的CASP方言铺平道路。基于SMT的求解组件使用翻译后的SMT-LIB程序返回原始ASP程序的回答集。此外，ezsmtv3实现了对优化语句的支持，即弱约束。这个特性是ezsmtv3新增的，而在CASP求解器ezsmt+中缺少。

本文第2节回顾了约束回答集编程的关键概念。第3节首先通过将旅行商问题的一个变体作为运行示例，详细描述了ezsmtv3支持的CASP方言，然后介绍了ezsmtv3系统的架构并讨论了其实现。鉴于优化语句是ezsmtv3相对于其“前辈”ezsmt+的新增特性，第4节介绍了系统中用于表达优化语句的语言构造的语法和语义，并以实现细节作为结尾。在第5节中，我们讨论了ezsmtv3与其最接近的CASP同类系统（如clingcon、clingo[LP]和clingo[DL]）的性能对比基准测试结果。我们注意到ezsmtv3的能力超越了所有这些同类系统，例如，该系统能够支持包含整数和实数变量的约束原子的推理。最后，我们展望了未来工作。

## 2. 背景  

### 2.1 逻辑程序与输入回答集  

本节中的许多定义沿用了Lierler（2023a，第3和第4节）的观点。

##### 逻辑程序  

**词汇表**是一组命题符号，也称为原子。**文字**是原子a或其否定¬a。一个*（命题）逻辑程序*基于词汇表σ是一组**规则**，形式为：
a ← b₁, ..., bₗ, not bₗ₊₁, ..., not bₘ, not not bₘ₊₁, ..., not not bₙ.   (1)
其中a是σ中的原子或⊥，每个b_i（1 ≤ i ≤ n）是σ中的原子。我们将使用规则(1)的缩写形式，即用B表示箭头右侧的部分，也称为**体**。用B⁺表示体B的**正部**，即b₁, ..., bₗ。我们有时将体B等同于命题公式：
b₁ ∧ ... ∧ bₗ ∧ ¬bₗ₊₁ ∧ ... ∧ ¬bₘ ∧ ¬¬bₘ₊₁ ∧ ... ∧ ¬¬bₙ.   (3)
并将规则(1)等同于命题公式（蕴含式）B → a。表达式a是规则的**头**。头部为符号⊥的规则称为**约束（denial）**。体为空（即n=0）的规则(2)称为**事实**；此时通常写作a.（其中B等同于⊤，⊤→a等同于a）。

对于逻辑程序Π（命题公式F），用At(Π)（At(F)）表示出现在Π（F）中的原子集合。通常，对于给定词汇表σ，将σ上的原子集合X等同于：(i) 由X ∪ {¬a | a ∈ σ \ X}构成的σ上完备且一致的文字集合，以及(ii) 将真值true赋给X中每个原子、false赋给σ \ X中每个原子的赋值函数或解释。在本文范围内，我们关注与相应程序相关的原子集合，以便引用该程序的签名。我们说原子集合X满足规则(2)，如果X（理解为赋值函数）满足命题公式B → a。自然，我们可以说集合X满足规则的体或体的负部，因为我们将它们等同于相应的命题公式。我们说X满足程序Π，如果X满足Π中的每条规则。此时，我们也说X是Π的一个模型。我们可能用符号⊧来缩写满足关系（表示原子集合满足规则、体、程序或公式）。

程序Π关于原子集合X的**归结（reduct）**Π^X通过以下方式获得：首先移除所有规则(1)，其中X不满足体的负部（¬bₗ₊₁ ∧ ... ∧ ¬bₘ ∧ ¬¬bₘ₊₁ ∧ ... ∧ ¬¬bₙ），然后将所有剩余规则替换为：a ← b₁, ..., bₗ.

###### 定义1（回答集）  
原子集合X是一个回答集，如果它是满足Π^X所有规则的最小集合（Lifschitz等，1999）。

###### 例1  
考虑程序：
b ← a.
c ← not a.   (4)
该程序只有一个回答集，即{c}。现在，我们通过在程序(4)中添加一个事实来构造新程序：
a.
b ← a.
c ← not a.   (5)
该程序只有一个回答集，即{a,b}。现在考虑另一个程序：
a ← not not a.
b ← a.
c ← not a.   (6)
该程序的第一条规则通常写作：
a.   (如选择规则)
这种形式的规则称为**选择规则**。我们可以直观地将上述规则理解为“原子a可能成立”。该程序有两个回答集：{a,b}和{c}。   (7)

我们现在给出输入回答集的定义，因为它对于定义约束回答集程序至关重要。

###### 定义2（输入回答集）  
对于基于词汇表σ的逻辑程序Π和词汇表ι ⊆ σ，且ι中的元素不出现在Π中任何规则的头中，σ上的原子集合X是Π关于ι的**输入回答集**，当且仅当X是程序Π ∪ (X ∩ ι)的一个回答集。

回忆程序(4)，它关于签名{a}有两个输入回答集。这些回答集列在(7)中。