Z3 的对称性破坏——在 UFBV 逻辑的上下文中（新版本）

Question

（这是我第二次尝试寻求帮助。如果问题/方法没有意义或不清楚，请告诉我。我也会很高兴任何小的提示或参考，这可以帮助我理解Z3 与我的 SBA 的行为）

我正在使用 UFBV Z3 逻辑对关系规范进行有界验证。我正在调查的当前问题需要伪造所有可能的模型（因为对可达性谓词的负面使用），这会在更高的范围内扼杀求解器的性能。

因为只有一部分可能的模型确实很有趣（与其他模型不同构），所以我试图引入对称破坏技术（在 SAT 领域已知）。

然而，在某些情况下使用我所说的对称破坏公理可以提高 Z3 的性能，但求解器的一般行为会变得不稳定。

我的一种方法（我认为最有希望的一种）基于打破关系 w.r.t 的对称性。他们的域名。它引入了关系 R 的每个域 D 和每个原子 a \in D 公理，它们对 R^{M} 和 R^{M[a+1/a]} 的二进制表示强制执行顺序，其中 M 是规范的模型。对于齐次关系，公理是放松的。

设 R \subset AxA 是一个关系。我对 R 的宽松对称破缺公理如下所示：

;; SBA(R, A)_upToDiag
(assert
 (forall ( (ai A) (aj A) )
  (=>
   (bvult ai aj)
   (=>
    (forall ((x A))
     (=>
       (bvult x aj)
       (= (R ai x) (R (bvadd ai (_ bv1 n)) x)) 
     )
    )
    (=>
     (R ai aj)
     (R (bvadd  ai  (_ bv1 n)) aj)
)))))    

;; SBA(R, A)_diag
(assert
 (forall ( (ai A) )
  (=>
   (forall ((x A))
    (=>
      (bvult x ai)
      (= (R ai x) (R (bvadd ai (_ bv1 n)) x)) 
    )
   )
   (=>
    (R ai ai)
    (R (bvadd  ai  (_ bv1 n)) (bvadd  ai  (_ bv1 n)))
)))) 

我的问题是，使用此 SBA 的效果并不稳定/一致。它不同于从绑定到绑定和从形式规范到另一个。此外，使用所有或仅使用一个 SBA 会影响性能。

在 SAT 上下文中，所谓的对称破坏谓词 (SBP) 方法的成功基于 SAT 求解器的回溯能力，这（以某种方式）保证，如果求解器回溯，它将修剪搜索使用 SBP 等空间。

• 在 Z3 的上下文中有何不同（如果有）？
• 如何强制求解以使用这些公理修剪搜索空间（当它回溯时）？
• 对我的 SBA 使用（量词）模式会有帮助吗？

问候，

Aboubakr Achraf El Ghazi

Answer 1

在 Z3 3.2 中，有两个主要引擎用于处理量化公式：E-matching 和 MBQI（基于模型的量词实例化）。电子匹配仅在无法满足的公式中有效。 Z3 将无法证明使用此引擎可以满足公式。 MBQI 更昂贵，但它可以表明几类公式（包含量词）是可以满足的。 Z3 guide 描述了这两个引擎（和其他选项）。为了有效地使用 Z3 解决重要的问题，了解这两个引擎的工作原理非常有用。

对称性破坏通常是减少搜索空间的非常有效的方法。很难准确指出您的问题发生了什么。对于不稳定的行为，我可以看到以下解释：

• MBQI 很难创建满足 SBA 的模型。尽管 SBA 会修剪搜索空间，但如果问题是可满足的，Z3 将尝试构建满足它们的解释（模型）。因此，在这种情况下，SBA 只是开销。如果输入公式很容易满足，但在添加 SBA 时变得很难满足，则尤其如此。您可以使用选项MBQI_TRACE=true 来确认这个假设。 Z3 将显示消息，例如：[mbqi] failed k!18。其中k![line-number] 是量词ID。您可以使用标签:qid 分配您自己的ID。这是一个例子：

  (assert (forall ((x T) (y T)) (! (=> (and (subtype x y)) （亚型 y x）） (= x y)) :qid 反对称)))

顺便说一句，您可以使用 MBQI=false 禁用 MBQI 模块。

在 Z3 的未来版本中，我们计划为某些量化公式添加一个禁用 MBQI 的选项。此功能可能对 SBA 有用。

• 另一种解释是电子匹配创建了太多的 SBA 实例。您可以使用选项QI_PROFILE=true 进行确认。 Z3 会转储以下信息：

[quantifier_instances] 反对称：12 : 1 : 2.00

第一个数字是生成的实例数。如果这是问题的根源，一种解决方案是为生成过多实例的 SBA 分配限制性模式。例如，Z3 将使用(R ai aj) 作为SBA(R, A)_upToDiag 的模式。这种模式可能会创建二次实例。另一个实验在于禁用电子匹配。例如，选项

AUTO_CONFIG=false EMATCHING=false MBQI=true

您也可以尝试在上面的配置中禁用相关性传播，选项：RELEVANCY=0。

最后，另一种选择是生成您认为有用的 SBA 实例，并删除量化公式。