Z3中的parthood定义答案

【问题标题】：parthood definition in Z3Z3中的parthood定义
【发布时间】：2017-10-14 13:36:25
【问题描述】：

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

(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 不会返回未知数。如果我考虑没有反对称的自反性和传递性，也是一样的。

【问题讨论】：

标签： set z3 smt

【解决方案1】：

量词本质上是不完整的。因此，Z3（或任何其他 SMT 求解器）在出现时将返回 unknown 也就不足为奇了。求解器使用一些启发式方法来处理量词，例如电子匹配；但这些仅在您有基本条款时适用。你的公式只有量化的公理，不太可能从中受益。

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

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

【讨论】：