代码之家 › 专栏 › 技术社区 › lllllllllllll

使约束解算器的约束更难求解?

constraint-satisfaction satisfiability smt z3 constraints

1

lllllllllllll · 技术社区 · 7 年前

我是SMT解决的新手,我写信是想询问一些建议和指针,以了解什么是真正的解决方案 difficult constraint 用于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 仍然做得很好,并能迅速解决。

我知道一些加密哈希函数或数学公式(例如Collatz猜想)可能会使约束求解变得非常困难。但这似乎相当极端。另一方面,例如,假设我有以下约束:

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

2 回复 | 直到 7 年前

1

2

alias 7 年前

位向量逻辑总是可判定的;因此,虽然事情可能需要很长时间,但z3可以解决所有位向量问题。当然,如果所涉及的位向量大小很大,那么解算器可能需要非常长的时间,或者在找到解决方案之前耗尽内存。乘法和加密算法是典型的例子,随着位大小的增加,这些算法总是会造成困难。

另一方面,我们有非线性整数问题。他们没有决策程序,虽然z3“尽了最大努力”,但由于理论原因,这些问题通常超出了范围。您可以在堆栈溢出帖子中找到许多这样的实例。这是最近的一个: Z3 returns model not available

2

1

usr 7 年前

如果你只是想看到Z3“非常努力”,你可以尝试数字分解。 a * b = constant 输入一个素数或一个大的复合数。

或者,构建一个简单的哈希函数并获得预映像:

我所做的就是看看怎么做 SHA-1 定义了。然后,我实现了一个简单的版本。SHA-1由非常简单的操作组成,如移位、加法、异或。从这个模板中,您可以构造一个简单的哈希函数来进行测试。那么你说 y = hash(x) && y = 0x1234 Z3会给你 x

为了娱乐您,我将当场编写一个简单的哈希函数:

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

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