我得到了一个 Z3 解算器(python 接口(interface))似乎无法处理的“简单”公式。它运行了相当长的一段时间(30 分钟),然后返回未知的结果,尽管我可以在一分钟内手动找到令人满意的作业。公式如下:
[Or(<uc 1.0> == 0, <uc 1.0> == 1),
Or(<uc 1.1> == 0, <uc 1.1> == 1),
Or(<uc 1.2> == 0, <uc 1.2> == 1),
<uc 1.0> + <uc 1.1> + <uc 1.2> == 1,
Or(<uc 0.0> == 0, <uc 0.0> == 1),
Or(<uc 0.1> == 0, <uc 0.1> == 1),
Or(<uc 0.2> == 0, <uc 0.2> == 1),
<uc 0.0> + <uc 0.1> + <uc 0.2> == 1,
Or(<uc 2.0> == 0, <uc 2.0> == 1),
Or(<uc 2.1> == 0, <uc 2.1> == 1),
Or(<uc 2.2> == 0, <uc 2.2> == 1),
<uc 2.0> + <uc 2.1> + <uc 2.2> == 1,
ForAll(c,
Or(c > 1000,
Or(c < -1000,
ForAll(b,
Or(b > 1000,
Or(b < -1000,
ForAll(a,
Or(a > 1000,
Or(a < -1000,
And(And(And(True,
a ==
<uc 0.0>*b +
<uc 0.1>*c +
<uc 0.2>*a),
b ==
<uc 1.0>*b +
<uc 1.1>*c +
<uc 1.2>*a),
c ==
<uc 2.0>*b +
<uc 2.1>*c +
<uc 2.2>*a))))))))))]
它可能看起来有点吓人,但让我带您了解一下。 < uc i.j> 都是整型变量。我首先明确指出他们 应该是 0 或 1 然后我引入约束 其中一个应该是 1,其他的应该是 需要为 0(使用总和)。
在第二部分中,您可以忽略所有 Or,这基本上只是将每个变量的搜索空间限制为 [-1000, 1000]。然后,我有最内部的约束,这应该意味着: < uc 0.2> = 1 < uc 1.0> = 1 < uc 2.1> = 1 和所有其他 = 0。仅此而已。我很确定求解器 应该能够解决这个问题,但没有运气。我可以更改金额 约束为 Or(< uc 1.0>,< uc 1.1>,< uc 1.2>) 之类的东西,有趣 足够了,在这种情况下解决了我的问题(求解器 以秒为单位返回正确的分配)但一般来说,这是 显然,不等于我想要的。
问题:
- 有没有类似位的东西,我可以用它来代替整数?
- 有一些推荐的方式来表达只有一个参数为 1 的事实?
- 使用其他方法可以在不更改公式第二部分的情况下解决此问题。
非常感谢!
//编辑:在尝试了几个选项后,我通过将辅助条件放置在 ForAll 条件之后(只需交换两行代码)来“解决”它。这根本不应该有任何影响,但现在他在 0.5 秒内找到了正确的分配 - 什么?我还尝试了使用 4 个变量 (a,b,c,d) 代替 (a,b,c) 的示例,但它又运行了几个小时......有什么帮助吗?用长度和/或改变总和也不起作用。
最佳答案
我尝试使用 bool 值而不是整数来表示 0-1 变量。然而,这并没有太大帮助。就目前而言,量词实例化机制可以改进以处理此类实例。
关于python - 当公式应可满足时,Z3 求解器返回 unsat,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/30263665/