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

Question

我正在研究一个项目,其重点是使用术语重写来解决/简化固定大小的位向量算术问题,这对于某些决策程序(例如基于钻头爆破的程序)的先前步骤是有用的.术语重写可以完全解决问题,或者产生更简单的等效问题,因此两者的组合可以导致相当大的加速.

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

目前,我刚刚找到了技术报告"固定宽度位向量的决策程序",描述了CVC Lite执行的规范化/简化步骤,我想找到更多这样的技术报告!我还发现了一张关于STP术语重写的海报,但这只是一个简短的总结.

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

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

Answer 1

我同意你的看法.很难找到描述现代SMT求解器中使用的预处理步骤的论文.大多数SMT求解器开发人员都认为这些预处理步骤对于Bit-Vector理论非常重要.我相信这些技术不会出于几个原因出现:大多数技巧本身并不是一项重大的科学贡献; 大多数技术仅适用于特定系统的环境; 一种似乎在求解器上运行良好的技术,对解算器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是一个值.它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).然后,消除后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)

• 接下来,它尝试使用分布最小化乘数的数量.例:

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

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

• 如果公式仅包含相等,连接,提取和类似运算符.然后,Z3使用基于union-find和同余闭包的专用求解器.

• 否则,它会使所有内容爆炸,使用AIG来最小化布尔公式,并调用其SAT求解器.