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