如何使用Z3解算器解决柯克曼的女学生问题? [英] How to use z3 Solver to solve Kirkman’s Schoolgirl Problem?
本文介绍了如何使用Z3解算器解决柯克曼的女学生问题?的处理方法,对大家解决问题具有一定的参考价值,需要的朋友们下面随着小编来一起学习吧!
问题描述
我是SMT问题的新手,并尝试使用Dennis Yurichev编写的一个例子来复制如何在SAT/SMT中使用Z3/MK85解决Kirkman的女学生问题。但当我试图获得模型(我使用的是Z3)时:
m["%d_%d" % (person , day)]
Python有一些错误:
回溯(最近一次调用):
文件"",第1行,
文件"D:3z3-master z3-master uildpythonz3z3.py",第6138行,in__getitem_z3_Assert(FALSE,"需要整数、Z3声明或Z3常量")
文件"D:3z3-master z3-master uildpythonz3z3.py",第92行,in_z3_assert raise Z3Exception(Msg)z3.z3ypes.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(" ")
我希望对其进行调试或以其他方式解决此问题。
推荐答案
这里的问题是您正在使用错误的索引访问模型。而不是:
m["%d_%d" % (person , day)]
使用:
m[tbl[person][day]]
(您有两个这样的实例,需要在这两个实例中都执行此操作。)
这篇关于如何使用Z3解算器解决柯克曼的女学生问题?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!
查看全文