2

我正在尝试编写一个脚本，给定一组（小）常量的偏序，找到可以构建为给定偏序约束的扩展的总顺序（即线性扩展）。

例如，如果a,b,c,d作为常数和a>b && b>d约束给出，程序应该输出这些排序中的任何一个（或所有，如果可行的话 - 线性扩展是#P-complete）： 

c > a > b > d  
a > c > b > d  
a > b > c > d  
a > b > d > c

这是我第一次尝试使用 z3py：

from z3 import *

s = Solver()
s.set("timeout", 3000)

if len(sys.argv) > 1 and sys.argv[1] == "int":
    sort = IntSort()
else:
    sort = DeclareSort('T')
to = Function('>', sort, sort, BoolSort())

x,y,z = Consts('x y z', sort)
s.add(ForAll([x,y], Implies(And(to(x,y),to(y,x)), x==y)))       # antisymmetry
s.add(ForAll([x,y,z], Implies(And(to(x,y),to(y,z)), to(x,z))))  # transitivity
s.add(ForAll([x,y], Or(to(x,y), to(y,x))))                      # totality

a,b,c,d = Consts('a b c d', sort)
s.add(Distinct(a,b,c,d))

s.add(to(a,b))
s.add(to(b,d))
#s.add(to(d,a)) # add cycle to make it unsat

print s.check()
print s.model()

这些是我的问题：

  1. 为什么在定义为的常量上使用总体IntSort约束时会超时？
  2. 有没有办法获得模型的更有用的表示（例如a<b<c<d）？（相关问题：链接）
  3. 有没有更好的方法或更合适的工具来解决这个问题？

提前感谢您的帮助！

4

0 回答 0