python - Z3 求解器在公式可满足时返回 unsat

Question

我得到了 Z3 求解器(python 界面)似乎无法处理的“简单”公式。它运行了相当长的一段时间(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's，它们基本上只是将每个变量的搜索空间限制为 [-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>) 的约束，这很有趣足够了，在这种情况下解决了我的问题(求解器在几秒钟内返回正确的分配)但一般来说，这是显然，不等同于我想要的。

问题:

• 有没有类似 bit 的东西，我可以用它来代替整数？
• 一些推荐的方式来表达恰好一个参数是 1 这一事实？
• 无需更改公式的第二部分即可解决此问题的其他一些方法。

非常感谢!

//编辑:在尝试了几个选项后，我通过将辅助条件放在 ForAll 条件之后(只需交换两行代码)来“解决”它。这根本不应该有什么不同，但现在他在 0.5 秒内找到了正确的分配 - 什么？我还尝试了使用 4 个变量 (a、b、c、d) 而不是 (a、b、c) 的示例，但它又运行了几个小时……有什么帮助吗？同样用长度和/或改变总和也不起作用。

Answer 1

我使用 bool 值而不是 0-1 变量的整数尝试了您的示例。但是，这并没有太大帮助。按照目前的情况，可以改进量词实例化机制以处理此类实例。