Как получить список комбинаций в z3py? - PullRequest
Новая
       18

Как получить список комбинаций в z3py?

0 голосов
/ 23 мая 2019

У меня есть список в Python целых чисел, как это: 

myList = [97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57]

Я хочу, чтобы Z3 выводил различные наборы или списки чисел, которые все являются членами myList ... По сути, я хочуиспользуйте Z3, чтобы получить дополнительные списки номеров, которые существуют в myList, но расположены в разных порядках.Иными словами, я хочу получить различные выходные данные из Z3, которые содержат числа в наборе myList выше.

У меня проблемы с этим с Z3py, потому что я не знаю, как заставить z3 возвращать список или набор какмодель, когда я звоню s.model(), предполагая s = Solver().

1 Ответ

1 голос
/ 23 мая 2019 
from z3 import *

myList = [97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57]

s = Solver ()
pick = []
for (i, v) in enumerate(myList):
  b = Bool ('pick_%d' % i)
  s.add(b == b)
  pick += [(b, v)]

while (s.check() == sat):
    m = s.model()

    chosen = []
    block  = []
    for (p, v) in pick:
        if m.eval(p, model_completion=True):
            chosen += [v]
            block.append(Not(p))
        else:
            block.append(p)

    print chosen
    s.add(Or(block))

Обратите внимание, что при этом будут напечатаны 2^n решения, где n - количество элементов в вашем списке;так что это займет некоторое время, если n большой!

...