量词和模式(QBF公式)

Question

我正在尝试用zt的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)

然而,sat-query的结果仍然是"未知".

我猜我需要正确的模式吗？如何为嵌套量词指定它们？但是,使用量词的简单示例似乎没有模式注释.

答案是Z3中警告信息背后的原因是什么:"未能找到量词的模式(量词id:k!18)"和z3指南对我来说没有太大帮助,不幸的是.

Answer 1

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

电子匹配仅对表明问题不可满足有效.由于您的示例是可以满足的,因此E匹配不会非常有用.也就是说,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中的任何公式将返回sat或unsat(即,它不返回unknown)时,片段可由Z3决定.当然,这种说法假定我们拥有无限量的资源.也就是说,Z3 unknown在内存不足或用户指定超时时也可能失败(即返回)可判定片段.

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