3

我是 SMT 求解的新手，我正在写信询问一些建议和指示，以了解difficult constraintSMT 求解器真正需要解决的问题，例如 Z3。

我试图调整位向量的长度，例如通过以下方式：

>>> a = BitVec("a", 10000)
>>> b = BitVec("b", 10000)
>>> c = a >> 18 + 6 - 32 + 69 == b <<12 + 7 * 32
>>>
>>> s = Solver()
>>> s.add(c)
>>> s.check()

虽然直觉上这可能会导致相当大的搜索空间，但事实证明它Z3仍然做得很好并且可以迅速解决它。

我知道一些加密哈希函数或数学公式（例如，Collat​​z 猜想）可能会使约束求解变得非常困难。但这似乎很极端。另一方面，例如假设我有以下约束：

a * 4 != b + 5

如何让约束求解器更难求解？有什么通用的方法吗？我的印象是，不知何故，约束变成了“非线性”，那就很难了。但我仍然不清楚它是如何工作的。

==================================

感谢您提供所有友好的注释和有见地的帖子。我非常感激！

因此，根据@usr 的建议，这里有一些试探性的测试：

c = BitVec("c", 256)

for i in range(0, 10):
    c = c ^ (c << 13) + 0x51D36335;

s = Solver()
s.add(c == 0xdeadbeef)
print (s.check())
print (s.model())


➜  work time python test.py
sat
[c = 37865234442889991147654282251706833776025899459583617825773189302332620431087]
python test.py  0.38s user 0.07s system 81% cpu 0.550 total
4

2 回答 2

2

位向量逻辑总是可判定的；所以虽然事情可能需要很长时间，但 z3 可以解决所有位向量问题。当然，如果所涉及的位向量很大，那么求解器可能需要很长时间，或者在找到解决方案之前内存不足。乘法和加密算法是典型的例子，随着比特大小的增加，它们总是会造成困难。

另一方面，我们有非线性整数问题。他们没有决策程序，虽然 z3 “尽力而为”，但由于理论上的原因，这些问题通常超出了范围。您可以在 stack-overflow 帖子中找到许多此类实例。这是最近的一个：Z3 退货型号不可用

于 2019-01-28T17:48:02.017 回答
1

如果您只是想看到 Z3 “非常努力地工作”，您可以尝试数字因式分解，例如a * b = constant并输入一个素数或一个大型复合数。

或者，构建一个简单的哈希函数并获得一个原像：

我所做的是查看SHA-1是如何定义的。然后，我实现了一个简单的版本。SHA-1 由非常简单的操作组成，例如移位、加法、异或。从这个模板中，您可以构建一个简单的散列函数用于测试目的。然后你说y = hash(x) && y = 0x1234Z3会给你x哪个是原像。

为了大家的娱乐，我就当场编一个简单的hash函数：

BitVec currentValue = input;

for (i = 0 to 10)
 currentValue = currentValue ^ (currentValue <<< 13) + 0x51D36335;

BitVec hash = currentValue;

这是一个实际功能性的哈希实现（但不安全）。您可以使用操作、轮数和位向量大小。您可以断言hash = someConstant以获取原像。例如，让 Z3 给你一个input导致零散列的结果。

您也可以应用更多花哨的约束，例如input == hash或hash % 1234 == 0 && hash & 0xF == 7。Z3 可以满足任何条件，只要有足够的计算能力。

我个人觉得这种能力非常迷人。

于 2019-01-28T21:10:03.443 回答