используя предыдущее / связанное значение в уравнении - PullRequest
Новая
       8

используя предыдущее / связанное значение в уравнении

1 голос
/ 11 февраля 2020

Можно разрешить такое уравнение: 

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?

Ответы [ 2 ]

0 голосов
/ 12 февраля 2020

Предположим, что 0bcb означает что-то вроде 0xcb, тогда список констант будет [80, 232, 203, 159, 161].

Затем вы запрашиваете 5 переменных, давайте назовем их d0, d1, d2, d3, d4, каждая из которых находится между 32 и 126. А где d0 + d1 == 80 (т. е. d1 <= 48) и d1 + d2 == 232 (т. е. d1 >= 106). Это явно противоречит, в котором Z3 согласен. (Обратите внимание, что ваши ограничения не используют последний элемент const.)

Вот немного более Pythoni c версия кода, которая включает в себя каждую из 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']
0 голосов
/ 11 февраля 2020

Да. После исправления очевидных синтаксических ошибок мой Z3 сообщает, что это неудовлетворительно.

...