在位向量算术的决策过程中使用术语重写

Posted 2023-02-25

【中文标题】在位向量算术的决策过程中使用术语重写

【英文标题】：Use of term rewriting in decision procedures for bit-vector arithmetic

【发布时间】：2012-01-06 13:34:36

【问题描述】：

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

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

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

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

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

【参考方案1】：

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

总之，这里是Z3进行的预处理的总结，以及重要的细节。

几个简化规则，可能会在局部减小这个大小，但在全局范围内增加它。简化器必须避免这种简化导致的内存爆炸。您可以在以下位置找到示例：http://research.microsoft.com/en-us/um/people/leonardo/mit2011.pdf

第一个简化步骤仅执行保持等价的局部简化。 示例：

2*x - x ->  x 
x and x -> x

接下来，Z3 执行恒定传播。给定一个相等t = v，其中v 是一个值。它用v 替换各处的t。

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)。然后，在消除x 之后，我们将有p(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)

接下来，它尝试使用分配性来最小化乘法器的数量。示例：

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

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

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

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

【参考方案2】：

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

Wintersteiger, Hamadi, de Moura: Efficiently Solving Quantified Bit-Vector Formulas, FMCAD, 2010

【讨论】：

感谢您的回答。几个月前我读过那篇论文（它在 Z3 网站的 Publications 部分中被引用），但是 - 如果我没记错的话 - 它非常关注公式所带来的困难是量化的。