2

我得到了一个 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 ij> 都是整数变量。我首先指定它们应该是 0 或 1，然后我引入了一个约束，即它们中的一个应该是 1，而其他的应该是 0（使用总和）。

在第二部分中，您可以忽略所有或基本上只是将每个变量的搜索空间限制为 [-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) 的示例，但它又运行了几个小时......有帮助吗？也用长度和/或改变总和不起作用。

4

2 回答 2

1

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

于 2015-05-19T17:21:26.113 回答
1

因此，如果不重新调整整个方法，我就无法摆脱乘法，所以我所做的是将所有条件（uc=1 或 uc=1 和 sum = 1）的块移动到 forAll 块下方。这在大多数情况下都有效，但仍有一些测试会运行数小时而没有结果。最终为我做的是将 forAll 语句组合在一起，而不是将它们分开。所以而不是：

ForAll(c,
        Or(c > 1000,
           Or(c < -1000,
              ForAll(b,
                     Or(b > 1000,
                        Or(b < -1000...

我会得到这样的东西

ForAll(c,
   ForAll(b,
        Or(c > 1000,
           Or(c < -1000,
              Or(b > 1000,
                 Or(b < -1000...

这最终解决了问题，求解器现在能够处理所有测试用例。我有点失望，花了这么多的尝试和错误才能让它正确，但至少我现在可以解决我的公式。谢谢！

于 2015-05-19T17:28:19.540 回答