量词和模式（QBF 公式）答案

【问题标题】：Quantifiers and patterns (QBF formula)量词和模式（QBF 公式）
【发布时间】：2012-04-18 06:07:50
【问题描述】：

我正在尝试在 z3 的 smt-lib 2 语法中编码 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)

但是，卫星查询的结果仍然“未知”。

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

很遗憾，What is the reason behind the warning message in Z3: "failed to find a pattern for quantifier (quantifier id: k!18) " 的答案和 z3 指南对我没有太大帮助。

【问题讨论】：

标签： z3

【解决方案1】：

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

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

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

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

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

【讨论】：