10

我正在从事一个项目，其重点是使用术语重写来解决/简化固定大小的位向量算术问题，这对于一些决策过程（例如基于位爆破的决策过程）的前一步很有用。重写这个术语可能完全解决问题，或者产生一个更简单的等效问题，因此两者的结合可以带来相当大的加速。

我知道许多 SMT 求解器都实施了这种策略（例如 Boolector、Beaver、Alt-Ergo 或 Z3），但很难找到详细描述这些重写步骤的论文/技术报告/等。一般来说，我只找到作者在几段中描述这种简化步骤的论文。我想找到一些详细解释术语重写使用的文档：提供规则示例，讨论 AC 重写和/或其他等式公理的便利性，重写策略的使用等。

目前，我刚刚找到了技术报告A Decision Procedure for Fixed-Width Bit-Vectors，它描述了 CVC Lite 执行的规范化/简化步骤，我想找到更多这样的技术报告！我还找到了一张关于STP 中术语重写的海报，但这只是一个简短的总结。

我已经访问了那些 SMT 求解器的网站，并在他们的出版物页面中进行了搜索...

我将不胜感激任何参考或任何解释如何在当前版本的知名 SMT 求解器中使用术语重写。我对 Z3 特别感兴趣，因为它看起来拥有最智能的简化阶段之一。例如，Z3 3.* 引入了一个新的位向量决策过程，但不幸的是，我找不到任何描述它的论文。

4

2 回答 2

14

我同意你的看法。很难找到描述现代 SMT 求解器中使用的预处理步骤的论文。大多数 SMT 求解器开发人员都同意这些预处理步骤对于位向量理论非常重要。我相信这些技术没有发表有几个原因：它们中的大多数都是一些小技巧，它们本身并不是重大的科学贡献；大多数技术仅适用于特定系统的上下文；一种在求解器上看起来效果很好的技术，在求解器A上却不起作用B。我相信拥有开源 SMT 求解器是解决此问题的唯一方法。即使我们发布了在特定求解器中使用的技术A，如果不查看其源代码，也很难重现求解器 A 的实际行为。

无论如何，这里是Z3执行的预处理的总结，以及重要的细节。

2*x - x ->  x 
x and x -> x
  • 接下来，Z3 执行恒定传播。给定一个等式t = vwherev是一个值。它t到处都用v.
t = 0 and F[t]  -> t = 0 and F[0]

  • 接下来，它对位向量执行高斯消元。但是，只有在算术表达式中最多出现两次的变量才会被消除。此限制用于防止增加公式中的加法器和乘法器的数量。例如，假设我们有和x = y+z+w出现x在p(x+z)、p(x+2*z)和。然后，在消除 之后，我们将有、和。虽然我们消除了，但我们有比原始公式更多的加法器。p(x+3*z)p(x+4*z)xp(y+2*z+w)p(y+3*z+w)p(y+4*z+w)p(y+5*z+w)x

  • 接下来，它消除了不受约束的变量。这种方法在 Robert Brummayer 和 Roberto Brutomesso 的博士论文中有所描述。

  • 然后，执行另一轮简化。这一次，执行本地上下文简化。这些简化可能非常昂贵。因此，使用了要访问的最大节点数的阈值（默认值为 1000 万）。局部上下文简化包含规则，例如

(x != 0 or  y = x+1) ->  (x != 0 or y = 1)
  • 接下来，它尝试使用分布最小化乘数的数量。例子：

a b + a c -> (b+c)*a

  • 然后，它尝试通过应用关联性和交换性来最小化加法器和乘法器的数量。假设公式包含项a + (b + c)和 a + (b + d)。然后，Z3 会将它们重写为:(a+b)+c和(a+b)+d. 在转换之前，Z3 必须对 4 个加法器进行编码。之后，由于 Z3 使用完全共享的表达式，因此只需要对三个加法器进行编码。

  • 如果公式仅包含相等、连接、提取和类似的运算符。然后，Z3 使用基于联合查找和同余闭包的专用求解器。

  • 否则，它将对所有内容进行位爆破，使用 AIG 最小化布尔公式，并调用其 SAT 求解器。

于 2011-11-29T07:10:42.107 回答
2

Z3 对预处理过程中执行的许多简化使用重写。用于 UFBV 策略（带有量词）的许多重写规则在以下论文中进行了详细描述：

Wintersteiger、Hamadi、de Moura：高效求解量化位向量公式，FMCAD，2010

于 2011-11-25T19:03:36.710 回答