TSAT：可满足性模理论的开放平台

理论计算机科学电子笔记125（2005）25-36www.elsevier.com/locate/entcsTSAT++：一个可满足性模理论的开放平台1亚历山德罗·阿曼多·克劳迪奥·卡斯特利尼·恩里科·琼奇利亚·马西莫·伊迪尼·马尔科·马拉泰亚MRG-DIST热那亚大学Genova，意大利摘要本文介绍了TSAT++，一个开放的平台，实现了懒惰的SAT为基础的方法，可满足性模理论（SMT）。SMT是确定T-文字的比例组合的可满足性的问题，其中T是一阶理论，对于该理论，一组基原子的可满足性过程是已知的。 TSAT++采用模块化设计，和理论特定的满足性检查器合作以解决SMT。模块化允许不同的枚举器和不同理论（或理论组合）的满足性检查器插入，只要它们符合简单且定义良好的接口。TSAT++中还实现了许多优化技术，这些技术与所使用的模块（以及相应的理论）无关。一些实验结果表明，TSAT++，实例化分离逻辑，是有竞争力的，或更快，国家的最先进的求解器，非常逻辑。关键词：布尔可满足性，基决策过程，分离逻辑，硬件验证，形式化方法1介绍可满足性模理论（SMT，见[15]）是确定T-文字的命题组合的可满足性的问题，其中T是一个简单的[1]我们感谢Ofer Strichman和Gilles Audemard对他们的求解器提出的宝贵建议。这项工作得到了COFIN和FIRB项目的部分支持，以及MIUR（意大利教育，大学和研究部）在RoboCare项目下的支持-一个具有智能固定和移动机器人组件的电子邮件：{armando，drwho，enrico，idini，marco} @ mrg.dist.unige.it1571-0661 © 2005 Elsevier B.V. 在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.06.06526A. Armando等人/理论计算机科学电子笔记125（2005）25第一阶理论的实际利益，如，例如，数组理论，列表理论，全线性算术（实数和整数）和分离逻辑[17]。所谓“简单”，我们的意思是，对于一组基原子的合取，理论必须有一个已知的可满足性过程。最近已经提出了用于SMT的许多系统和技术（例如，[4，17，8]），表明问题是极大的兴趣。事实上，复杂的无限状态系统的行为（例如，实时硬件和程序）可以在SMT中严格指定换句话说，SMT似乎是表达性和易处理性之间的一个有趣的折衷。SMT最有前途的方法之一是所谓的基于惰性SAT的方法[1，2，8]。这个想法是通过一个有效的布尔可满足性（SAT）机器来管理对模型的搜索，例如，Davis-Logemann-Loveland算法（参见，例如，开创性的论文[7]），并将一阶推理委托给理论T2的ad-hoc满足性过程。只要巧妙地处理这种解耦，这种方法就可以从以下方面受益：(i) 在搜索中重新使用多年来在SAT研究中获得的大部分技术和技能的可能性(ii) 升级T-可满足性程序的可能性，提高性能和/或扩展合理的可满足性处理的理论范围。据我们所知，虽然到目前为止，人们一直在关注将各种理论的决策过程结合起来的理论和实践问题，但很少或根本没有关注构建一个实用的开放式架构，在这个架构中，SAT推理机和满意度过程可以顺利地结合起来，同时保持良好的性能。(An[10]这是一种新的尝试因此，在本文中，我们提出了一种实现该方法的模式，它模块化地结合了枚举器和满意度检查器。这两个模块依次负责搜索和所需的一阶推理。它们的组合是通过C++抽象类实现的。我们沿着这些路线构建的系统TSAT++是SMT的开放平台，任何这样的模块都可以插入其中，只要它们符合类定义的接口。我们还表明，一些优化技术，无论是从人工智能和正式的方法文学和新的借鉴，可以顺利imple-实际上，这里只需要一个T原子合取集的可满足性过程;但为了简单起见，我们将保留这个术语。A. Armando等人/理论计算机科学电子笔记125（2005）2527不不¬ ∧∨不联系我们在TSAT++中，它们是理论独立的，因为一种技术要么只通过抽象类提供的接口来实现，要么完全在一个模块中实现;这样的技术，然后，可以应用于所有理论，对于这些理论，一个合适的T-可满足性模块，与接口兼容，是可用的。最后，我们证明了TSAT++，为分离逻辑（SL，见[17]）实例化，在来自工业测试用例的合成和真实世界问题上，比最先进的SL求解器表现得本文的组织如下：经过一些说明（第2节），我们提出了TSAT++最后，第6节描述了结论和未来的工作。2背景我们假设一阶逻辑和命题逻辑的基本知识。假设T是一个一阶理论，对于它，一个基原子的合取集合的满足性过程是已知的;那么T-原子是T的原子公式;SMT-原子是T-原子或命题原子，SMT-公式是SMT-原子和SMT-公式通过标准命题连接词（如，和）的布尔组合。SMT文字是SMT原子或其否定。一个SMT赋值σ（或简单赋值，当它不是二义性的时候）是一个从SMT公式中的变量到适当域中的值的映射，以及命题原子到真值的映射。通过定义（1）σ（α）=（α是T原子）当且仅当α在σ下的赋值对于理论的标准解释为真，推广了SMT-赋值σ以将SMT-公式映射到（2）σ（φ）=（φ是SMT公式）。在这方面，一个赋值也被视为一个SMT文字的合取集合。设φ为SMT公式。一个SMT-赋值σ满足φ当且仅当σ（φ）= ;在这种情况下，σ将被称为φ的SMT-模型，或简称为模型。φ是满足的当且仅当存在一个模型。这里我们处理SMT的决策问题，即确定SMT公式是否满足的问题。28A. Armando等人/理论计算机科学电子笔记125（2005）253系统描述根据所谓的基于惰性SAT的方法（参见[1，2，8]），可以构建SMT的决策过程，其执行三个阶段：(i) 抽象。φ首先通过不同T原子到（新的）命题原子的双射映射η映射到布尔公式φ;(ii) Check. 如果不满意，则程序以否定的答案停止。否则，确定T的布尔模型μ，并检查T-原子集η−1（μ）的T-满足性;如果检查成功，则该过程以肯定的答案停止;否则，(iii) 精 炼 。 检 测 到 η−1 （ μ ） 的 一 个 不 满 足 的 子 集 （ 从 现 在 起 称 为reason），并将其添加到k中;然后程序返回到步骤ii。我们已经在一个名为TSAT++的系统中实现了基于惰性SAT的SMT方法，其体系结构如图1所示。SAT+模型/UNSATFig. 1. TSAT++的高级视图。我们现在就上述三个阶段简要说明该架构。然后给出模块之间的接口的概述3.1功能视图抽象阶段由解析/抽象模块快速执行通常情况下，懒惰方法中的抽象基本上包括用一个新的命题变量替换每个不同的T检查阶段如下进行：主模块接收和η，并最初将馈送给枚举器。这个模块的任务是枚举（布尔）模型，我们一般用µ表示。如果主模块预处理−1−1是/否+可满足性检验器向前看解析+抽象回顾枚举器接口接口A. Armando等人/理论计算机科学电子笔记125（2005）2529公式在命题上是不可满足的，也就是说，没有（更多）模型要枚举，TSAT++以否定的答案停止。否则，主模块评估T原子的集合η−1（μ），并将其发送到满足性检查模块。这个模块确定集合是否是T-可满足的。如果η−1（µ）是满意的，则TSAT++以肯定答案退出。(In如果需要，通常很容易给出φ的模型。）否则，一个在图中称为η−1（）的原因将被评估并发送回主模块。然后，它将发送给枚举器，并请求一个新的µ。循环回到检查阶段。3.2建筑观TSAT++是用C++编写的，自然地利用抽象类的机制来实现枚举器和满足性检查器模块的接口。接口由C++抽象类定义，每个模块必须是相关抽象类的具体实例（例如，参见[9]）。每个接口由每个模块可以用来与系统交互的方法和数据结构组成，这些方法和数据结构必须是兼容的（即，模型、T原子集等必须从TSAT++中定义的通用数据结构转换为与模块相关的数据结构在操作上，该模块的代码被单独编译成一个静态库，该静态库随后被链接到TSAT++。这有两个好处：(a)它完全将TSAT++从模块中分离出来，也是在编译/运输级，使得模块的开发独立于系统的开发;以及（b）它使任何可以转换为相关抽象类的实例的模块能够以合理的扩展插入到TSAT++原则上，可以使用不完整或非基于DPLL的枚举器（当然，代价是放弃完整性），以及不同理论或理论组合的满意度检查器。驱动思想是使外来代码能够无缝集成到TSAT++中，最大限度地减少将任何T-satisfiability pro-ccurrence（例如，那些存在于等式定理证明器中的）或SAT机器到TSAT++模块中。到目前为止，如何设计接口的问题已经通过最大必要性的标准得到了解决;换句话说，对模块的要求一直保持在最低限度。详细地说，TSAT++和枚举器之间的接口定义了以下服务：(i) getAssignment搜索并返回一个μ的模型;如果不能满足μ，则返回空的赋值。30A. Armando等人/理论计算机科学电子笔记125（2005）25(ii) isSatisied返回当前是否满足条件。(iii) augmentFormula将一个布尔公式（在签名中）连接到。到目前为止，我们使用的是合取范式中的SMT公式，所以这个方法实际上是向递归添加了一组布尔子句。另一方面，TSAT++和SAT检查器之间的接口定义了以下服务：(i) isSatified返回η−1（µ）是否满足。(ii) deduceConstraints从当前的η−1（µ）推导出新的约束。原则上，该方法可以返回可以从η − 1（μ）推导出的任何约束集，也可以在满足的情况下（这可能发生，例如，如果使用早期修剪，见下文）;到目前为止，它从不满意的η−1（µ）中返回一个原因。4优化技术接口机制不仅使模块的内部工作完全不确定，而且使返回的对象的质量（相对于所处理的理论）完全不确定。例如，TSAT++不可能影响枚举器搜索模型的方式。一方面，这限制了TSAT++对其组件的控制，另一方面，它给了模块开发人员最大的自由来选择算法和优化。然后可以实现广泛的此类技术，这些技术独立于实际模块，因为它们是由TSAT++通过接口实施的，或者因为它们嵌入在单个模块中。下面是在TSAT++中实际实现的一些技术的描述;每次我们也概述了该技术是如何实现的。（2）第二节：第二节：这种技术检测不满意的T原子对（完整版本中的T字面值），并在搜索开始之前将它们作为二元子句添加到表中IS（2）至少在一类综合问题中是有效的（见[2]）。当然，该技术可以从T原子对扩展到T原子的任意元组（字面量）.IS（2）预处理是完全在线完成的，通过反复调用满足性检查器A. Armando等人/理论计算机科学电子笔记125（2005）2531⊆增强、背跳和学习为了符合augmentFormula方法，枚举器必须能够实时地扩充其公式。正如从关于基于惰性SAT的定理证明的文献中所熟知的那样，这可以通过使用现成的SAT求解器（参见[8]）或通过工程化DPLL方法来实现，以便使其更加开放和灵活。 第二个选择从观点上来说更好当然，从效率的角度来看，但是以这种方式重新设计一个现成的SAT求解器通常不是一件小事。枚举器还必须能够“忘记”在搜索过程中通过augmentFormula添加的子句，根据某些策略，因为它们的数量可能是指数级的枚举器还应该能够最大限度地利用在运行中增加其公式的约束;特别是，它应该能够backjump和学习（这些技术在SAT文献中是众所周知的，这里没有解释;读者可以查看[14，6]）。这些优化完全在枚举器本身内部实现减少µ给定μ，我们计算出μ的一个素蕴涵，即一个子集ρ μ，在集合包含下最小，这仍然是对μ的一个非矛盾赋值;然后η−1（ρ）被发送到满足性检查器来代替η−1（μ）。另一种有效减少µ的方法是使用触发，即删除µ中任何不出现在中的文字。可以很容易地证明，这不会改变方法的合理性。触发已经在[20]中引入，并且也用于称为MathSAT的工具[4，5]。一般来说，减少μ通常是有用的：如果η−1（μ）是满意的，那么是η−1（ρ）;如果η−1（μ）是不可满足的，而η−1（ρ）是可满足的，那么我们无论如何都找到了一个η的模型;最后，如果η−1（μ）和η−1（ρ）都是不可满足的，那么检验后者的可满足性，而不是检验前者的可满足性，可以导致指数上少得多的可满足性检验。事实上，任何扩展ρ的赋值也是一个抽象模型，并且可能被生成然后被拒绝。(It必须指出的是，该技术潜在地使系统变慢 如果与早期修剪结合使用，见下文）。µ的减少完全用于主模块，对模块是透明的。早期修剪如果我们放宽getAssignment服务返回模型的要求，而是让它产生不矛盾的分配，即模型32A. Armando等人/理论计算机科学电子笔记125（2005）25的子集，我们可能利用了一个明显的事实，即一个不满意的T-文字集不能通过增加更多的文字变得满意。将这样的赋值输入到满足性检查器可能会比让枚举器生成模型更早地生成有价值的约束集，因此可能会节省时间。这种技术与AI文献中通常称为早期修剪和/或前向检查的技术[16、13、19]）。早期修剪完全在枚举器内部实现。评价方法sat检查器通常可以返回大量的约束。 一般来说，我们必须非常小心地选择返回给枚举器的内容，满足η−1（µ）或不满足。到目前为止，让我们集中讨论后一种情况;一个普遍有用的策略似乎是寻找小的原因;这是由一个明显的事实驱动的，即小的子句通常可以比长的子句修剪更大部分的搜索空间。如果枚举器维护搜索树（所有DPLL实现都是这种情况），则尤其如此在后一种情况下，另一个有益的策略可以是评估η−1（μ），它相对于搜索树在T-文字上诱导的排序是最小的-可以称为“最浅”集。这样的约束可以帮助枚举器尽可能高地回跳。概括一点，注意TSAT++并不局限于用一个子句来扩充reason;因此，即使在从一组不满意的T-文字中检测原因的简单情况下，一个想法是返回所有原因的子集可接受性的评估完全在可接受性检查器内部实现。5实验结果我们已经实例化了第3节中描述的分离逻辑（SL）的体系结构，SL是一种将布尔逻辑与线性运算片段相结合的可判定理论，能够复杂地捕获一大类无限状态系统的行为。最近，人工智能的一些有趣的问题（计划，调度，时间推理，例如，在[19，4]中）和形式方法（硬件的安全性，实时系统的有界模型检查，例如， 在[17]中）被转化为SL-公式的判定问题。 因此，需要 有效的决策程序。目前，枚举器是SIMO的修改版本[11]，一个类似于Cha的SAT求解器;SL的满意度检查器模块依赖于Bellman-FordA. Armando等人/理论计算机科学电子笔记125（2005）2533表1钻石问题DS独特TSAT++SepSEP（无c.m.）MathSAT504N00.030.120.05504Y0.010.840.07时间1005N0.010.131.180.611005Y0.0410.200.17时间2505N0.080.9552.205.42505Y0.21288.300.77时间5005N0.295.92742.9921.225005Y1.05时间4.85时间算法它很容易在检测到不满意后返回最小的原因。我们将TSAT++与两个SL决策程序MathSAT[4]和SEP[17]进行比较。选择的基准是：（1）如[17]中定义的钻石实验在Pentium IV 2.4GHz上运行，RAM为1GHz。我们以秒为单位报告搜索CPU时间。在下表中，TIME表示进程在1000秒后停止方块.给定一个参数D，这些问题的特点是由一个指数大（2D）数量的布尔模型，其中一些对应于SL-模型;硬实例与一个唯一的SL-模型可以生成。第二个参数S用于使SL模型更大，进一步增加了难度。变量在实数范围内变化。表1显示了关于钻石问题的比较结果。第三列表示问题是否具有唯一的SL模型;其余列显示TSAT++的CPU时间，其中包含主蕴涵减少和最小原因检测，SEP有和没有合取矩阵和MathSAT。3TSAT++显然表现最好，往往是数量级最好;[3]所采用的配置是SEP和MathSAT的作者建议的34A. Armando等人/理论计算机科学电子笔记125（2005）25表2现实世界的问题。实例（类别）TSAT++SEP（无c.m.）MathSATabz5-900（a）1.9时间0.82环2 -10（a）0.020.010.01环2 -100（a）2.070.181.074/10（a）0.51时间1.064/11（a）1.01时间2.134/12（a）0.58时间0.91LD-ST-0.3步骤（b）0.030.42-OOO-阴性3步骤（b）0.010.23-除了没有合取矩阵的SEP之外，具有唯一解的实例比非唯一解的实例更加困难。现实世界的问题。这些问题代表（a）时间自动机的调度和有界模型检查，（b）硬件模型的验证，包括加载存储单元和乱序执行单元。考虑表2：我们比较了TSAT++（完全IS（2）预处理，主要蕴涵减少和检测后处理问题的最小原因，以及早期修剪加上其他问题的最小原因），没有合取矩阵的SEP和MathSAT，SEP可以解决的最大问题，在任何类别中发现在类别（b）中，变量被限制为整数值，MathSAT已被排除在比较之外。正如人们所看到的，TSAT++与其竞争对手竞争，或者比其竞争对手更快。值得一提的是，MathSAT是为毕业后问题定制的，SEP是为SL定制的。6结论SMT是一个有趣的和具有挑战性的问题，主要是由于其expressivity;和SAT为基础的方法代表了一个通用的解决范式，这个问题，在同一时间能够实现高性能。该方法的本质是搜索之间的相互作用，由一个A. Armando等人/理论计算机科学电子笔记125（2005）2535枚举器模块，和一阶推理，委托给一个专门的满意度程序。最近已经沿着 这些 路线 进行 了 许多 研究 ， 参见 ， 例 如， Tsat[2] ， CVC[18] ，ICS[8]，MathSAT[4]和UCLID [12]等系统所取得的成果（SEP实际上是作为UCLID的后端而诞生的我们认为开放性和模块化在这里至关重要，以便在灵活性，可扩展性和可扩展性方面获得收益。这就是为什么我们建立了系统TSAT++，其中两个方面的懒惰SAT为基础的方法到SMT嵌入在两个专用模块中，通过简单、定义良好的C++抽象类进行管理。当然，一个悬而未决的问题是，如何在不损失性能的情况下保持系统的在本文中，特别是，我们已经描述了该系统的体系结构，给出了我们已经实现的一些优化技术的概述。这些技术是理论独立的，因为它们要么通过使用接口提供的服务来实现，要么被限制在模块中。最后，我们已经展示了一些实验结果，其中TSAT++，instantiated分离逻辑，是有竞争力的或比专门的求解器更快的逻辑，这至少是一个初步迹象表明，保持系统模块化不一定会降低其性能。TSAT++获得的更多实验结果可以在[3]中看到;此外，有关系统的最新信息，使用的基准测试和TSAT++的可执行文件可以在http://www.mrg.dist.unige.it/Tsat上找到。我们计划在合理的时间内向社区提供源代码，从而扩大可能的应用范围。引用[1] A. Armando 和 E. Giunchiglia 。 在 交 互 式 定 理 证 明 器 中 嵌 入 复 杂 的 决 策 过 程 。 Annals ofMathematics and Arti Ficial Intelligence，8（3[2] Alessandro Armando，Claudio Castellini，and Enrico Giunchiglia.基于SAT的时间推理程序。Susanne Biundo和Maria Fox编辑，第五届欧洲规划会议论文集，计算机科学讲义第1809卷，第97-108页斯普林格，2000年。[3] Alessandro Armando，Claudio Castellini，Enrico Giunchiglia，and Marco Maratea.一个基于卫星的决策程序的布尔组合的差异约束，2004年5月出现在SAT 2004年，温哥华，不列颠哥伦比亚省，加拿大。[4] Gilles Audemard，Piergiorgio Bertoli，Alessandro Cimatti，Artur Kornilowicz，and RobertoPastiani.一个基于SAT的解决布尔和线性数学命题公式的方法。在Andrei Voronkov，编辑，自动演绎-Springer-Verlag，2002年7月27日至30日36A. Armando等人/理论计算机科学电子笔记125（2005）25[5] Gilles Audemard，Alessandro Cimatti，Artur Kornilowicz，and Roberto Pastiani.定时系统的有界模型检验。IFIPWG 6.1 International Conference on Formal Techniques for Networkedand Distributed Systems（FORTE），LNCS，2002年第22卷。[6] R. J. Bayardo，Jr.和D. P·米兰克。约束满足问题空间有界学习算法的复杂性分析。 在procAAAI，第298-304页，1996年。[7] M.戴维斯，G。Logemann和D.洛夫兰 一种用于定理证明的机器程序。 杂志ACM，5（7），1962年。[8] 列奥纳多·德·科雷亚，哈拉尔德·鲁埃托，玛丽亚·索里亚。有限域上有界模型检验的懒惰定理证明。计算机科学讲义，2392：438[9] Erich Gamma，Richard Helm，Ralph Johnson，and John Vlissides. 设计模式。艾迪森·韦斯利，马萨诸塞州雷丁，一九九五年[10] Harald Ganzinger ， George Hagen ， Robert Nieuwenhuis ， Albert Oliveras ， and CesareTinelli. DPLL（T）：快速决策程序。2004年7月出现在2004年的CAV[11] Enrico Giunchiglia，Marco Maratea，and Armando Tacchella.现代sat解算器中的前视与后视技术。2003年5月在意大利波尔图举行的SAT 03-第六届国际会议上接受了满意度测试的理论和应用[12] 舒文杜湾Lahiri，Sanjit A. Seshia和Randal E.布莱恩特UCLID中乱序微处理器的建模与验证。计算机科学讲义，2517：142[13] A. Oddi和A. Cesta 析取时态问题的增量前向检验。第14届欧洲人工智能会议（ECAI-2000），第108-112页，柏林，2000年[14] 帕特里克·普罗瑟。约束满足问题的混合算法。Computational Intelligence，9（3）：268[15] Silvio Ranise ， Cesare Tinelli ， et al. SMT library （ Satifiability Modulo Theory ） .http://www.smtlib.org的网站。[16] Kostas Stergiou和Manolis Koubarakis。时态约束析取的回溯算法Arti Ficial Intelligence，120（1）：81[17] Ofer Strichman，Sanjit A. Seshia和Randal E.布莱恩特 确定分离公式， 饱和计算机科学讲义，2404：209[18] 作者：Aaron Stump Barrett，and David L. 迪尔CVC：一个合作的有效性检查器。在JC。Godskesen，编辑，计算机辅助验证国际会议论文集，计算机科学讲义，2002年。[19] 艾欧尼斯·查马迪诺斯和玛莎·波拉克。析取时态推理问题的有效求解技术。人工智能，2003年。地出现。[20] 史蒂文·沃夫曼和丹尼尔·韦尔德。LPSAT引擎及其在资源规划中的应用。在Proc. IJCAI-99，1999中。