z3 - Z3 答案不满足约束
问题描述
我开始使用 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) 情况的约束,如下表所示。
我做错了什么,我怎样才能得到一个满足约束的解决方案,比如第二个表中的规则?
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
解决方案
我无法复制这个。当我运行你的程序时,我得到:
[fc = [else -> And(Var(0), Var(1))],
fa = [else -> And(Var(0), Not(Var(1)))],
fb = [else -> False]]
这似乎是正确的模型。请注意,这与您所得到的不同,因为它似乎可以交换fc
并且fa
在您的情况下。
这很可能是一个已经修复的错误;我正在使用来自 github 源代码的新编译的 z3。您能否升级您的 z3 安装并查看问题是否消失?
推荐阅读
- outlook - 用阿拉伯语创建邮箱别名
- javascript - 如何使用 ngx 数据绑定将复选框绑定到选择禁用的属性?
- c# - 清除 Winform 文本框代码片段说明
- java - 如何使用 getAllSelectedOptions 从多个下拉列表中获取选定的选项
- svn - VisualSVN 服务器从 Windows 2008 迁移到 2012(Svn 版本 2.7.14)
- php - SwaggerUI 传递参数
- c# - 用另一个覆盖 IExternal 命令
- python - 如何从 Django 字段中检索数据?
- python - 使用 email.mime 时无法在电子邮件正文中看到 pandas 数据框
- node.js - Node 中 Http Get 的异步使用