Z3中的parthood定义 [英] parthood definition in Z3

问题描述

我试图在 Z3 中定义成对集合(使用数组定义)之间的分居关系(在下面的代码中称为 C).我写了 3 个断言来定义自反性、传递性和反对称性，但 Z3 返回未知"，我不明白为什么.

I'm trying to define in Z3 the parthood relation (called C in the code below) between pairs of sets (defined using array). I wrote 3 asserts to define reflexivity, transitivity, and antisymmetry but Z3 returns "unknown" and I don't understand why.

(define-sort Set () (Array Int Bool))
(declare-rel C (Set Set))

; reflexivity
(assert (forall ((X Set)) (C X X)))

; transitive
(assert (forall ((X Set)(Y Set)(Z Set)) 
    (=> 
        (and (C X Y) (C Y Z)) 
        (C X Z)
    )
))

; antisymmetric
(assert (forall ((X Set)(Y Set)) 
    (=> 
        (and (C X Y) (C Y X))
        (= X Y)
    )
))

(check-sat)

我注意到只有当反对称与其他 2 个断言之一一起考虑时才会返回未知数.如果我只考虑反对称属性 Z3 不会返回未知.如果我考虑没有反对称的自反性和传递性也是一样.

I noticed that the unknown is returned only when the antisymmetry is considered with one of the other 2 asserts. If I only consider the antisymmetry property Z3 doesn't return unknown. The same if I consider reflexivity and transitivity without antisymmetry.

推荐答案

量词本质上是不完整的.因此，当 Z3(或任何其他 SMT 求解器)存在时返回 unknown 也就不足为奇了.求解器使用一些启发式方法来处理量词，例如 e-matching；但这些仅在您有基本条款时才适用.你的公式只有量化的公理，不太可能从中受益.

Quantifiers are inherently incomplete. So, it's not surprising that Z3 (or any other SMT solver) will return unknown when they are present. There are a few heuristics that solvers use for handling quantifiers, such as e-matching; but those will only apply when you have ground-terms around. Your formulation, having only quantified axioms, is unlikely to benefit from that.

对于一般量词的推理，SMT 求解器根本不是最佳选择；为此，请使用定理证明器(Isabelle、Lean、Coq 等).

For reasoning about quantifiers in general, an SMT solver is simply not the best choice; use a theorem prover (Isabelle, Lean, Coq, etc.) for that.

这是 Leonardo 关于在 SMT 求解中使用量词的精彩幻灯片:https://leodemoura.github.io/files/qsmt.pdf.它有助于深入了解相关技术和困难.

Here's a nice slide deck by Leonardo on the use of quantifiers in SMT solving: https://leodemoura.github.io/files/qsmt.pdf. It can help provide some further insight into the techniques and the difficulties associated.

这篇关于Z3中的parthood定义的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！