时间戳

首页 > 解决方案 > 在等式中使用先前/链接的值

z3 - 在等式中使用先前/链接的值

问题描述

有可能解决这种方程：

const = [0x50, 0xe8, 0bcb, 0x9f, 0xa1]
data = IntVector('data', len(const))
for i in range(0, len(const)-1):
  s.add(data[i] >= 32, data[i] <= 126)
  s.add(data[i+1] >= 32, data[i+1] <= 126)
  s.add(data[i] + data[i+1] == const[i]

还是我滥用 Z3 库？

标签： z3z3py

解决方案

假设这0bcb意味着类似0xcb，那么常量列表是[80, 232, 203, 159, 161]。

然后你要求 5 个变量，我们称它们d0, d1, d2, d3, d4为 32 到 126 之间的变量。以及 where d0 + d1 == 80(so d1 <= 48) 和d1 + d2 == 232(so d1 >= 106)。这显然与 Z3 同意的地方相矛盾。（请注意，您的约束不使用 . 的最后一个元素const。）

这是代码的稍微 Pythonic 版本，其中包括 5 个常量中的每一个（降低第二个常量以获得可解的约束系统）：

from Z3 import IntVector, Solver, sat

const = [0x50, 0xa9, 0xcb, 0x9f, 0xa1]
s = Solver()
data = IntVector('data', len(const)+1)
for d in data:
    s.add(d >= 32, d <= 126)
for d0, d1, c0 in zip(data, data[1:], const):
    s.add(d0 + d1 == c0)
result = s.check()
if result == sat:
    print("Here is a solution: ")
    m = s.model()
    values = [m[d].as_long() for d in data]
    print(values, " sums:", [hex(v0 + v1) for v0, v1 in zip(values, values[1:])])
elif result == unsat:
    print("There is no solution")
else:
    print("Z3 could not solve the constraints")

输出：

Here is a solution: 
[37, 43, 126, 77, 82, 79]  sums: ['0x50', '0xa9', '0xcb', '0x9f', '0xa1']

推荐阅读