减少最大位向量大小的等价公式

Question

是否有可能将 .smt2 公式转换为等价公式，以这样的方式重写它，即每个

(declare-const a (_ BitVec 256))

都将转换为一组

(declare-const a0 (_ BitVec 8))

。所以最大的BitVec大小变成了8。但是断言的解决方案和逻辑保持不变？

Answer 1

一般来说，这种减少是不可能的。 （即，可以解决任意问题的方法。）

这是一个简单的反例。考虑当

x > 255

被解释为 256 位变量时的单个断言

x

。这显然是可以满足的。但是当你限制

x

为 8 位宽时，它不是。

在你问也许我们可以相应地“缩放”常量之前，答案将保持不变：一般来说，如果你有 N 个 256 位变量，你就有一个

N^256

位的状态空间。如果你保持变量的数量相同，那么使用 8 位你只能表示

N^8

位。 （当然，这个论点适用于任何比特大小的减少，256 和 8 在任何方面都不是特别的。）而且没有办法用更少的变量来保持这个空间的 sat/unsat 分区的对应关系。保持可满足性不变的唯一方法是相应地增加变量的数量，但正如您可以想象的那样，这种增加将是指数级的，这超出了减少的全部目的。

话虽如此，位宽缩减是一种有效的“启发式”技术。这个想法很简单：将您的原始问题置于 256 位之上，并将所有变量视为 8 位。 （如果你愿意，甚至可以更小。）

• 如果减少的实例是

  SAT

  ，拿模型看看那个模型是否也满足原来的问题。 （通过简单地按原样解释常量，因为有直接注入。）如果是这样，你就完成了，你有一个原始公式的模型。如果简化后的模型不能满足原来的问题，你就什么也得不到。 （即，你不能断定原始问题是

  unsat

  或

  sat

  。）你可以尝试在减少的设置中找到不同的模型来尝试，或者增加位大小，或者放弃。

• 如果缩减实例是UNSAT，你不能得出anything的结论。 （这是关键位。）您可以增加减少到的位大小，然后重试。

例如，上述算法本质上是非线性整数求解器的工作原理；通过连续尝试对其进行有限大小的近似，如果迭代没有导致成功的模型，则在一定次数的尝试后放弃。 （并且可能切换到不同的技术。）请注意，这个“技巧”永远无法回答

unsat

，但它可以找到模型。 （有关详细信息，请参阅https://stackoverflow.com/a/13898524/936310。）