model - Dose z3 は、すべての飽和可能なモデルを見つけます

Question

x + y > 5 、x > 3 、y < 4 などの制約があるため、モデルのセット x = 4 y= 3 は z3 によって与えられます。線量 z3 は、モデル x=5,y = 2? の別のセットなど、モデルを段階的に与えることができます。ありがとう。よろしく

Answer 1

これで何が起こるか教えてください：

x,y = Bools('x y')

s = Solver()
s.add(Or(x,y))


count = 0
while s.check() == sat and count <= 50:
  print s.model()
  s.add(Or(x != s.model()[x], y != s.model()[y])) 
  count = count + 1
print count

出力は次のとおりです。

[y = False, x = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
 51

ここでオンライン