Удовлетворить K из N ограничений в Z3Py - PullRequest
Новая
       26

Удовлетворить K из N ограничений в Z3Py

0 голосов
/ 21 октября 2019

У меня есть программа с логикой, как описано в псевдокоде ниже. x является строкой, а x[k] вернет десятичный код символа в индексе k. Оператор ^ возвращает десятичный результат XOR операндов. 

x = input
int checksum = x[0] ^ x[1] ^ x[2]
int sum = 0

sum += x[36] ^ x[23] == 111
sum += x[23] ^ x[29] == 101
sum += x[29] ^ x[30] == 116
sum += x[30] ^ x[9] == 115
sum += x[9] ^ x[25] == 0

return sum == checksum and x[0] ^ x[29] == 100 and x[1] ^ x[30] == 200

Я хочу найти входные данные, которые возвращают эту программу true. Если я хочу решить эту проблему в Z3Py, есть ли способ для меня это сделать? Мне нужно некоторое ограничение K из N, которое позволяет мне выражать ограничения как выражения, но я не нашел поддержки для этого.

Psedocode для того, что я хотел бы сделать с Z3: 

int checksum = x[0] ^ x[1] ^ x[2]

bools = []

bools.append(Bool(x[36] ^ x[23] == 111))
bools.append(Bool(x[23] ^ x[29] == 101))
bools.append(Bool(x[29] ^ x[30] == 116))
bools.append(Bool(x[30] ^ x[9] == 115))
bools.append(Bool(x[9] ^ x[25] == 0))

state.add(bools[0])
state.add(bools[1])
state.add(bools[2])
state.add(bools[3])
state.add(bools[4])
state.add(x[0] ^ x[29] == 100)
state.add(x[1] ^ x[30] == 200)

state.add(PbEq([boolean for boolean in bools], checksum))

1 Ответ

1 голос
/ 21 октября 2019

Читая описание вашей проблемы, я не понимаю, зачем вам нужны ограничения K-out-of-N для этой проблемы. Это кажется простым кодированием с использованием теории битовых векторов. Но, возможно, я не совсем понял проблему, которую вы пытаетесь решить. Было бы полезно показать, что вы пытались, а что не получилось.

В любом случае, если вам действительно нужны ограничения K-out-of-N, то Z3 имеет специальную поддержку для них в различных формах:

Такие ограничения известны как "псевдобулевы" и, следовательно, префикс Pb.

...