7

我正在尝试用 smt-lib 2 语法为 z3 编码 QBF。运行 z3 会导致警告

警告：找不到量词的模式（量词 id：k！14）

可满足性结果为“未知”。

代码如下：

(declare-fun R (Bool Bool Bool Bool) Bool)
(assert
  (forall ((x2 Bool) (x3 Bool)) 
    (exists ((y Bool))
      (forall ((x1 Bool))
        (R x1 x2 x3 y)
      )
    )
  )
)
(check-sat)

我通过将代码重写为

(set-option :auto-config false)
(set-option :mbqi false)
(declare-fun R (Bool Bool Bool Bool) Bool)
(declare-fun x1 () Bool)
(declare-fun x2 () Bool)
(declare-fun x3 () Bool)
(declare-fun y () Bool)
(assert
  (forall ((x2 Bool) (x3 Bool)) 
  (!
    (exists ((y Bool))
    (!
      (forall ((x1 Bool))
      (!
        (R x1 x2 x3 y)
      :pattern((R x1 x2 x3 y)))
      )
    :pattern((R x1 x2 x3 y)))
    )
  :pattern((R x1 x2 x3 y)))
  )
)
(check-sat)

然而，sat-query 的结果仍然是“未知的”。

我猜我需要得到正确的模式？如何为嵌套量词指定它们？不过，带有量词的更简单示例似乎可以在没有模式注释的情况下工作。

不幸的是， Z3中警告消息背后的原因是什么：“未能找到量词的模式（量词id：k！18）”和z3指南对我没有太大帮助。

4

1 回答 1

8

可以忽略此警告消息。它只是通知您，电子匹配引擎将无法处理此量化公式。

电子匹配仅在表明问题不可满足时才有效。由于您的示例可以满足，因此电子匹配不会很有用。也就是说，Z3 将无法sat使用 E 匹配引擎返回。基于模型的量词实例化 (MBQI) 是 Z3 中唯一能够显示包含量词的问题是可满足的引擎。

使用默认配置，Z3 将返回sat您的示例。它返回unknown是因为您禁用了 MBQI 模块。

MBQI 引擎保证 Z3 是许多片段的决策过程（参见http://rise4fun.com/Z3/tutorial/guide）。但是，它通常非常昂贵，当快速和近似的答案足够时应该禁用它。在这种情况下，unknown可以读作probably sat. VCC等验证工具禁用 MBQI 模块，因为它无法确定它们生成的公式。也就是说，VCC生成的公式不在MBQI引擎可以决定的任何片段中。我们说一个片段可以由 Z3 决定，当片段中的任何公式 Z3 将返回sat或unsat（即，它不返回unknown）。当然，这种说法假设我们拥有无限量的资源。unknown也就是说，当 Z3内存不足或用户指定超时时，Z3 也可能因可判定片段而失败（即 return ）。

最后，Z3 3.2在 MBQI 引擎中有一个bug 。该错误已修复，不会影响您的问题。如果您需要，我可以为您提供包含错误修复的 Z3 4.0 的预发布版本。

于 2012-04-05T18:15:00.750 回答