1

(这是我第二次尝试寻求帮助。如果问题/方法没有意义或不清楚,请告诉我。我也会对任何小的提示或参考感到高兴,这可以帮助我理解Z3 和我的 SBA)

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

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

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

我的一种方法(我认为最有前途的一种)基于打破其领域关系的对称性。它引入了关系 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

4

1 回答 1

4

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

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

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

    (assert (forall ((x T) (y T)) (! (=> (and (subtype xy) (subtype yx)) (= xy)) :qid 反对称)))

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

在 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 实例,并删除量化公式。

于 2012-02-17T15:23:01.323 回答