Создать или-ограничение над списком Bools - PullRequest
Новая
       10

Создать или-ограничение над списком Bools

1 голос
/ 09 марта 2019

Я играю с Z3 в Python, чтобы генерировать решения для головоломки растворения.У меня нет опыта работы с SAT / SMT-решателями или Z3, и даже мой Python все еще находится на уровне pidgin.Поэтому, пожалуйста, будьте осторожны.

В моем подходе у меня есть два списка xs и ys Bools.Из других ограничений я знаю, что в каждом из двух списков самое большее одна из записей - «Истина», а все остальные - «Ложь».Либо ноль, либо одна запись True в каждом списке.

Я хочу добавить ограничение, которое сравнивает два списка на том, есть ли у них запись True или оба ложные.

Итак, я хочучто-то вроде or(all_the_xs)==or(all_the_ys).У меня есть ощущение, что это должно быть довольно родным для Z3, но я не могу понять, как это сформулировать.

Мне удалось сделать это, сравнив число истинных значений с использованием z3.Sum([z3.If(x,1,0) for x in xs]), но это действительно требуетэто из области простых логических.Это также кажется неэластичным и менее эффективным, насколько это возможно.

Вот типичный автономный пример моего кода в боджинге, использующего Sum(): 

import z3

solver = z3.Solver()

xs = [ z3.Bool("x_{i}".format(i=i)) for i in range(0,10) ]
ys = [ z3.Bool("y_{i}".format(i=i)) for i in range(0,10) ]

xsum = z3.Sum([z3.If(x,1,0) for x in xs])
ysum = z3.Sum([z3.If(x,1,0) for x in ys])

solver.add(xsum == ysum)

solver.check()
print(solver.model())

Можете ли вы помочь мне повторить это вкрасивее и более Z3-дружественная форма?Или уверить меня, что все в порядке?

Спасибо, что читаете и думаете, Мариан

1 Ответ

2 голосов
/ 09 марта 2019

Вам повезло!z3py поставляется с Or, который принимает список логических значений: 

import z3

solver = z3.Solver()

xs = [ z3.Bool("x_{i}".format(i=i)) for i in range(0,10) ]
ys = [ z3.Bool("y_{i}".format(i=i)) for i in range(0,10) ]

solver.add(z3.Or(xs) == z3.Or(ys))

solver.check()
print(solver.model())

Это печатает: 

[x_0 = False,
 x_1 = False,
 x_2 = False,
 x_3 = False,
 x_4 = False,
 x_5 = False,
 x_6 = False,
 x_7 = False,
 x_8 = False,
 x_9 = False,
 y_0 = False,
 y_1 = False,
 y_2 = False,
 y_3 = False,
 y_4 = False,
 y_5 = False,
 y_6 = False,
 y_7 = False,
 y_8 = False,
 y_9 = False]

Не самая интересная модель, но я считаю, что это именно то, что выищу!

...