在 Z3Py 中获取布尔表达式的所有解永远不会结束 [英] Getting all solutions of a boolean expression in Z3Py never ends

问题描述

可能是与 Z3 相关的一个基本问题:我正在尝试获取布尔表达式的所有解决方案，例如对于 a OR b，我想得到 {(true, true),(false,true),(true,false)}

Probably a basic question related to Z3: i am trying to get all solutions of a boolean expression, e.g. for a OR b, i want to get {(true, true),(false,true),(true,false)}

基于发现的其他回复，例如Z3:找到所有满意的模型，我有以下代码:

Based on other responses found, e.g. Z3: finding all satisfying models, i have the following code:

a = Bool('a')
b = Bool('b')

f1=Or(a,b)
s=Solver()
s.add(f1)

while s.check() == sat:
  print s
  s.add(Not(And(a == s.model()[a], b == s.model()[b])))

问题在于它在第二次迭代时进入无限循环:约束 a == s.model()[a] 被评估为 false b/c s.model()[a] 不再存在.

The issue is that it enters an infinite loop as at the second iteration: the constraint a == s.model()[a] is evaluated to false b/c s.model()[a] does not exist anymore.

谁能告诉我我做错了什么?

Can someone tell what i am doing wrong?

推荐答案

我建议您尝试这样编写循环:

I would advice you to try writing your loop like this instead:

from z3 import *

a = Bool('a')
b = Bool('b')

f1 = Or(a,b)
s = Solver()
s.add(f1)

while s.check() == sat:

    m = s.model()

    v_a = m.eval(a, model_completion=True)
    v_b = m.eval(b, model_completion=True)

    print("Model:")
    print("a := " + str(v_a))
    print("b := " + str(v_b))

    bc = Or(a != v_a, b != v_b)
    s.add(bc)

输出为:

Model:
a := True
b := False
Model:
a := False
b := True
Model:
a := True
b := True

参数 model_completion=True 是必要的，否则 m.eval(x) 的行为就像任何 x 布尔变量的恒等关系当前模型 m 中的 don't care 值，它返回 x 作为结果而不是 True/False>.(查看相关问答)

The argument model_completion=True is necessary because otherwise m.eval(x) behaves like the identity relation for any x Boolean variable with a don't care value in the current model m and it returns x as a result instead of True/False. (See related Q/A)

注意:由于 z3 善意标记不关心布尔变量，另一种选择是编写自己的模型生成器，自动- 完成任何部分模型.这将减少对 s.check() 的调用次数.这种实现的性能影响很难衡量，但可能会稍微快一些.

NOTE: since z3 kindly marks don't care Boolean variables, an alternative option would be to write your own model generator that auto-completes any partial model. This would reduce the number of calls to s.check(). The performance impact of this implementation is hard to gauge, but it might be slightly faster.

这篇关于在 Z3Py 中获取布尔表达式的所有解永远不会结束的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！