Improving Bit-Blasting for Nonlinear Integer Constraints
动机 前言 介绍文章前，首先需要说明对于经典的 SMT(QF_NIA)，基于 bit-blasting 做法，简而言之主要是以下三步： 先给整数变量一个有限位宽（bit-width）把整数运算翻译成位向量电路再交给 SAT solver 对于第一步而言，一个整数变量 x 其位向量可以表示为位宽为 w 的向量 \bar{x}: <\bar{x}_{w-1}, \cdots, \bar{x}_1, \bar{x}_0>，其中 \bar{x}_{w-1} 为符号位 。