constraints - 使约束求解器更难解决约束？

Question

我是 SMT 求解的新手，我写信是想咨询一些建议和指示，以了解什么是 SMT 求解器要解决的真正困难约束，例如 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

Answer 1

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

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