Z3 答案不满足约束

Question

我刚开始使用 Z3，我给它出了一道玩具题。这个想法是针对 (a,b,c) 的所有赋值，至少有一个 (fa(b,c) == a, fb(a,c) == b, fc(a,b) == c)一定是真的。

模型报告

[fc = [else -> And(Not(Var(1)), Var(0))],
  fa = [else -> And(Var(1), Var(0))],
  fb = [else -> False]]

这似乎不满足 (a=False, b=True, c=True) 情况的约束，如下文 table 中所述。

我做错了什么，我怎样才能得到满足约束的解决方案，就像第二个 table 中提出的规则？

import pandas as pd
from z3 import Bools, Function, BoolSort, Solver, ForAll, Or

a, b, c = Bools("a b c")
fa = Function("fa", BoolSort(), BoolSort(), BoolSort())
fb = Function("fb", BoolSort(), BoolSort(), BoolSort())
fc = Function("fc", BoolSort(), BoolSort(), BoolSort())

s = Solver()
s.add(ForAll([a, b, c], Or(fa(b, c) == a, fb(a, c) == b, fc(a, b) == c)))


def tabulate(fa, fb, fc):
    mi = pd.MultiIndex.from_product(
        [[False, True] for _ in range(3)], names=["a", "b", "c"]
    )
    df = pd.DataFrame(index=mi).reset_index()
    return (
        df.assign(fa=fa, fb=fb, fc=fc)
        .assign(
            fb_correct=lambda x: x.fb == x.b,
            fa_correct=lambda x: x.fa == x.a,
            fc_correct=lambda x: x.fc == x.c,
        )
        .assign(any_correct=lambda x: x.fb_correct | x.fa_correct | x.fc_correct)
        .astype(int)
    )


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

# sat
# [fc = [else -> And(Not(Var(1)), Var(0))],
#  fa = [else -> And(Var(1), Var(0))],
#  fb = [else -> False]]

print(tabulate(fb=False, fa=lambda x: x.b & x.c, fc=lambda x: x.a & ~x.b))

#    a  b  c  fa  fb  fc  fb_correct  fa_correct  fc_correct  any_correct
# 0  0  0  0   0   0   0           1           1           1            1
# 1  0  0  1   0   0   0           1           1           0            1
# 2  0  1  0   0   0   0           0           1           1            1
# 3  0  1  1   1   0   0           0           0           0            0
# 4  1  0  0   0   0   1           1           0           0            1
# 5  1  0  1   0   0   1           1           0           1            1
# 6  1  1  0   0   0   0           0           0           1            1
# 7  1  1  1   1   0   0           0           1           0            1


# Correct answer:
print(
    tabulate(fb=lambda x: ~x.a | x.b, fa=lambda x: x.b & x.c, fc=lambda x: x.a & ~x.b)
)

#    a  b  c  fa  fb  fc  fb_correct  fa_correct  fc_correct  any_correct
# 0  0  0  0   0   1   0           0           1           1            1
# 1  0  0  1   0   1   0           0           1           0            1
# 2  0  1  0   0   1   0           1           1           1            1
# 3  0  1  1   1   1   0           1           0           0            1
# 4  1  0  0   0   0   1           1           0           0            1
# 5  1  0  1   0   0   1           1           0           1            1
# 6  1  1  0   0   1   0           1           0           1            1
# 7  1  1  1   1   1   0           1           1           0            1

版本：z3-solver==4.8.0.0.post1

Answer 1

我无法复制这个。当我运行你的程序时，我得到：

[fc = [else -> And(Var(0), Var(1))],
 fa = [else -> And(Var(0), Not(Var(1)))],
 fb = [else -> False]]

这似乎是正确的模型。请注意，这与您得到的不同，因为在您的情况下它似乎交换了 fc 和 fa。

这很可能是一个已经修复的错误；我正在使用来自 github 来源的新编译的 z3。您能否升级您的 z3 安装并查看问题是否消失？

Z3 答案不满足约束

Z3 answer does not satisfy constraint

z3

z3py