为啥连词的电子匹配对顺序/大小写策略敏感？

Posted 2023-03-28

【中文标题】为啥连词的电子匹配对顺序/大小写策略敏感？

【英文标题】：Why is E-matching for conjunctions sensitive to order / case-splitting strategy?为什么连词的电子匹配对顺序/大小写策略敏感？

【发布时间】：2015-01-26 12:08:50

【问题描述】：

鉴于以下简化的量词，并根据 Boogie 生成的选项设置 Z3 选项（详细信息如下），结果我得到“未知”：

(declare-fun F (Int) Bool)
(declare-fun G (Int) Bool)

(assert (forall ((x Int)) (! (and
  (F x) (G x))
  :pattern ((F x))
)))
(assert (not (forall ((x Int)) (! (and
  (G x) (F x))
  :pattern ((F x))
))))
(check-sat)

我对（我认为）Z3 会解决这个问题的理解是，将存在的（不是全部的）skolemise，这将产生 F 和 G 的地面实例。鉴于 e-graph 中的这些，我们应该能够实例化另一个量词，然后变得不满足。我可以看到 Z3 可能必须进行大小写拆分才能执行此操作，但我希望在删除量词并填充 e-graph 之后进行这种大小写拆分。

相反，在上述问题中，第一个量词没有被实例化。我做了一些观察：

在第一个量词中交换 (F x) 和 (G x) 项的顺序会导致“未饱和”没有任何量词实例化（我想一些简化发现了两个量化断言之间的相似性？）。 在第二个量词（以及第一个量词）中交换 (G x) 和 (F x) 项的顺序会导致“unsat”与单个量词实例化（这是我期望的行为一般）。 更改 smt.case_split 选项会影响行为。设置为 3（由 Boogie 选择）或 5，我们得到“未知”。设置为 0、1、2 或 4，我得到“未饱和”。

很高兴了解上述情况，以及为什么（在失败的情况下）这些术语在 skolemisation 后并不总是出现在 e-graph 中。我不确定更改 case_split 选项的效果一般是什么。目前，我认为 Boogie 不允许更改它（并覆盖在命令行上所做的任何选择）。但我觉得理想情况下，电子图应该在所有情况下都能获取信息。

这是完整文件（删除大部分选项集似乎对失败案例没有影响，除了 smt.case_split 一个）：

(set-option :print-success false)
(set-info :smt-lib-version 2.0)
(set-option :AUTO_CONFIG false)
;(set-option :MODEL.V2 true)
(set-option :smt.PHASE_SELECTION 0)
(set-option :smt.RESTART_STRATEGY 0)
(set-option :smt.RESTART_FACTOR |1.5|)
(set-option :smt.ARITH.RANDOM_INITIAL_VALUE true)
(set-option :smt.DELAY_UNITS true)
(set-option :NNF.SK_HACK true)
(set-option :smt.MBQI false)
(set-option :smt.QI.EAGER_THRESHOLD 100)
(set-option :smt.QI.COST |"(+ weight generation)"|)
(set-option :TYPE_CHECK true)
(set-option :smt.BV.REFLECT true)
(set-option :TIMEOUT 0)
(set-option :smt.QI.PROFILE true)
(set-option :smt.CASE_SPLIT 3)
; done setting options


(declare-fun F (Int) Bool)
(declare-fun G (Int) Bool)

(assert (forall ((x Int)) (! (and
  (F x) (G x))
   :pattern ((F x))
)))
(assert (not (forall ((x Int)) (! (and
(G x) (F x))
  :pattern ((F x))
))))
(check-sat)

【参考方案1】：

https://***.com/users/1096362/nikolaj-bjorner 对此问题的回答解决了这个问题： Surprising behaviour when trying to prove a forall

将证明义务翻译成析取式，然后是相应的条款相关性，解释了为什么 Z3 不将这两个连词都视为潜在触发因素。