z3 - 量词和模式(QBF 公式)

Question

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

WARNING: failed to find a pattern for quantifier (quantifier 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 的结果仍然是“未知的”。

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

What is the reason behind the warning message in Z3: "failed to find a pattern for quantifier (quantifier id: k!18) "的答案|不幸的是，z3指南并没有给我太多帮助。

Answer 1

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

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

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

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

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