Как использовать z3 Solver для решения проблемы школьницы Киркмана? - PullRequest
Новая
       14

Как использовать z3 Solver для решения проблемы школьницы Киркмана?

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

Я новичок в проблемах SMT и пытался скопировать, как решить проблему школьницы Киркмана с z3 / MK85 в SAT / SMT, используя пример, написанный Денисом Юричевым.Но когда я попытался получить модель (я использовал Z3):

m["%d_%d" % (person , day)]

Python имеет некоторые ошибки:

Traceback (самая последняяпоследний вызов):

Файл "", строка 1, в

Файл "D: \ Z3 \ z3-master \ z3-master \ build \ python \ z3 \ z3.py",строка 6138, в __getitem ___ z3_assert (False, «Ожидается целочисленное значение, объявление Z3 или ожидается постоянная Z3»)

Файл «D: \ Z3 \ z3-master \ z3-master \ build \ python \ z3 \ z3.py", строка 92, в _z3_assert повысить Z3Exception (msg) z3.z3types.Z3Exception: ожидается целое число, объявление Z3 или константа Z3

Интересно, не запутался ли я в выражении модели?.Я хотел бы отладить это.Кроме того, мне интересно, есть ли другой способ решения этой проблемы в Z3 и разница выражений между z3 и MK85. 

from z3 import *
import itertools
PERSONS , DAYS , GROUPS = 15, 7, 5
s=Solver()
tbl=[[BitVec("%d_%d"%(person , day), 16) for day in range(DAYS)] for person in range(PERSONS)]
for person in range(PERSONS):
   for day in range(DAYS):
      s.add(And(tbl[person][day]>=0, tbl[person][day] < GROUPS))
def only_one_in_pair_can_be_equal(l1, l2):
   assert len(l1)==len(l2)
   expr=[]
   for pair_eq in range(len(l1)):
             tmp=[]
             for i in range(len(l1)):
                     if pair_eq==i:
                             tmp.append(l1[i]==l2[i])
                     else:
                             tmp.append(l1[i]!=l2[i])
             expr.append(And(*tmp))
   s.add(Or(*expr))
for pair in itertools.combinations(range(PERSONS), r=2):
   only_one_in_pair_can_be_equal (tbl[pair[0]], tbl[pair[1]])
assert s.check()
m=s.model()
print("group for each person:")
print("person:"+"".join([chr(ord('A')+i)+" " for i in range(PERSONS)]))
for day in range(DAYS):
   print("day=%d:" % day)
   for person in range(PERSONS):
      print(m["%d_%d" % (person , day)])  #error
   print("")

def persons_in_group(day, group):
     rt=""
     for person in range(PERSONS):
             if m["%d_%d" % (person , day)]==group:#error
                     rt=rt+chr(ord('A')+person)
     return rt
for day in range(DAYS):
     print( "day=%d:" % day)
     for group in range(GROUPS):
             print(persons_in_group(day, group)+" ")
     print(" ")

Я ожидаю отладки или решения этого вопроса другим способом.

1 Ответ

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

Проблема в том, что вы обращаетесь к модели с неверным индексом.Вместо: 

m["%d_%d" % (person , day)]

Использование: 

m[tbl[person][day]]

(у вас есть два экземпляра, вам нужно сделать это в обоих.)

...