Z3软约束

Question

我对 z3 中软约束的使用感到困惑。当运行这个程序时，我得到以下输出。

from z3 import *
o = Solver()

expr = f"""
(declare-const v Real)
(declare-const v1 Bool)
(assert-soft v1)
(assert (= v1 (<= 0 v)))
(assert (> 10 v))

"""

p = parse_smt2_string(expr)
o.add(p)

print(o.check())
print(o.model())

输出： [v1 = 假，v = -1]

请问有人知道为什么在存在允许软约束的 v 值的情况下不满足软约束吗？

同样，这个程序没有return预期的输出：

from z3 import *
o = Optimize()


expr = f"""
(declare-const v1 Real)
(declare-const e Bool)
(assert (= e (<= 6 v1)))
(assert-soft e)
"""

p = parse_smt2_string(expr)
o.add(p)

print(o.check())
print(o.model())

它 returns [v1 = 0, e = False]。为什么软约束不能实现？

Answer 1

看起来 parse_smt2_string 没有保留软断言。

如果您在调用 check 之前添加 print(o.sexpr())，它会打印：

(declare-fun v () Real)
(declare-fun v1 () Bool)
(assert (= v1 (<= (to_real 0) v)))
(assert (> (to_real 10) v))

如您所见，soft-constraint 已消失。所以，z3 看到的并不是您认为的那样。这解释了意外的输出。

我知道 parse_smt2_string 并不完全忠实，因为它不处理任意 SMTLib 输入。我不确定是否支持这种特殊情况。在 https://github.com/Z3Prover/z3/issues 将其作为问题提交，开发人员可能会查看。

Z3软约束

Z3 soft constraint

constraints

z3

smt