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

StackOverflow https://stackoverflow.com/questions/9300754

  •  25-10-2019
  •  | 
  •  

题

（这是我第二次尝试获得帮助。如果问题/方法没有意义或不清楚，请让我知道。我也会对任何小提示或参考感到高兴，这可以帮助我了解Z3与我的SBA）

我正在使用UFBV Z3逻辑对关系规范进行有限的验证。我正在研究的当前问题需要伪造所有可能的模型（由于对可及性谓词的负面使用），这会以较高范围杀死求解器的性能。

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

但是，在某些情况下，我称之为对称性破坏公理的用法可以改善Z3的性能，但是求解器的一般行为变得不稳定。

我的一种方法（我认为最有前途的一种方法）是基于将对称性打破其域名的对称性。它介绍了关系r的每个域d和d axioms中的每个原子a ，它在r^{m}和r^{m [a+1/a]}的二进制表示上执行订单规范的模型。对于同质关系，公理会放松。

让R 子集Axa A A 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

有帮助吗？

解决方案

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

对称破裂通常是减少搜索空间的非常有效的方法。很难确切地指出您的问题正在发生的事情。我可以看到以下不稳定行为的解释：

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

    （断言（forall（（x t）（y t））（！

顺便说一句，您可以使用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的实例，并删除量化的公式。

许可以下： CC-BY-SA 和 归因
不隶属于 StackOverflow
scroll top