python - Z3 による半次数の線形拡張

Question

(小さな) 一連の定数に対する部分順序を指定して、指定された部分順序制約の拡張 (つまり、線形拡張)として構築できる合計順序を見つけるスクリプトを作成しようとしています。

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. この問題を解決するためのより良い方法またはより適切なツールはありますか?

助けてくれてありがとう！