On the Complexity of Fixed-Size Bit-Vector Logics with Binary Encoded Bit-Width
On the Complexity of Fixed-Size Bit-Vector Logics with Binary Encoded Bit-Width
复制标题
关于二进制编码位宽的固定大小位向量逻辑的复杂性
DOI：
10.29007/cvnz
复制
发表时间：
2012
影响因子：
3.6
通讯作者：
Armin Biere
中科院分区：
文献类型：
--
作者：
Gergely Kovásznai;Andreas Fröhlich;Armin Biere
位精确推理对于可满足性模理论的许多实际应用都很重要。近年来，已经开发了用于求解x大小位向量公式的新方法。从理论的角度来看，只有少数结果的复杂性xed大小的位向量逻辑已公布。在本文中，我们表明，这些结果中的一些只持有，如果使用一元编码的位宽的位向量。然后，我们考虑xed大小的位向量逻辑与二进制编码的位宽，并建立新的复杂性结果。我们的证明表明，二进制编码增加了更多的表现力的位向量逻辑，例如，它使xed大小的位向量逻辑，即使没有未解释的功能，也没有量化NExpTime-complete。我们还表明，在一定的限制下，使用二进制编码时，可以避免复杂性的增加。
Bit-precise reasoning is important for many practical applications of Satisability Modulo Theories (SMT). In recent years ecient approaches for solving xed-size bit-vector formulas have been developed. From the theoretical point of view, only few results on the complexity of xed-size bit-vector logics have been published. In this paper we show that some of these results only hold if unary encoding on the bit-width of bit-vectors is used. We then consider xed-size bit-vector logics with binary encoded bit-width and establish new complexity results. Our proofs show that binary encoding adds more expressiveness to bit-vector logics, e.g. it makes xed-size bit-vector logic even without uninterpreted functions nor quantication NExpTime-complete. We also show that under certain restrictions the increase of complexity when using binary encoding can be avoided.