量化列表长度限制导致不满足

如何解决量化列表长度限制导致不满足

通过以下示例，我尝试对所有可能列表的长度设置约束以量化的方式。这将导致“unsat”结果，我确信这是正确的。

有人可以详细说明为什么这是不可满足的，以及是否有办法绕过该限制而不将长度限制放在特定变量/常量上？

我发现了 this 有趣的话题，但我的问题并没有真正得到解答。此外，答案是旧的，参考 SMT-LIB 2.0 版（以及一个未量化的版本）。也许现在 Z3 能够以一种我不知道的方式做到这一点。

(set-logic ALL)
(set-option :produce-unsat-cores true)

(declare-datatypes ((List 1)) ((par (T) ((cons (head T) (tail (List T))) (nil)))))

(define-sort IntList() (List Int))

(define-fun-rec IntList.length((l IntList)) Int
    (ite
        (= l (as nil IntList))
        0
        (+ (IntList.length (tail l)) 1)
    )
)

(assert (! (forall ((this IntList)) (<= 2 (IntList.length this))) :named a10))

(check-sat)
(get-unsat-core)

我使用 Z3 master 的 commit 8abb644378ebaf1a9699e1b2fdd32075bcfcea4e 截至 2021-01-12，Win10 上的 64 位。

解决方法

这个断言：

(assert (! (forall ((this IntList)) (<= 2 (IntList.length this))) :named a10))

不满意。毫无疑问，您已经注意到，不意味着您希望 z3 只考虑长度至少为 2 的整数列表。它只是说可以根据您给出的定义生成的所有列表的大小至少为 2。这只是一个错误的陈述。这就是为什么这个脚本是 unsat。

简而言之，SMT 中的数据类型是“自由生成的”。有关其含义的详细说明，请参阅 https://stackoverflow.com/a/60998125/936310。如果您想对所有大小至少为 2 的列表进行建模，那么您必须修改您的数据类型以确保它确保您的基本情况不是 nil 情况，而是在至少有两个元素来完成列表。这是确保求解器仅考虑大小 >= 2 的列表的唯一方法。

明确地说，您的愿望是“我试图以量化的方式对所有可能列表的长度进行限制。”如果您坚持使用示例中定义的列表，则无法用量化的公理表示。（即，使用简单的 cons 和 nil。）如果这是您想要的，您将不得不说类似（伪代码）：

(assert (forall ((x IntList)) (=> (>= (length-of x) 2) 
                              ... condition you want to prove ...)))

也就是说，您必须编写一个蕴涵，并在假设您拥有的列表长度至少为 2 的情况下证明您想要什么。当然，这会很快变得非常复杂，而 SMT 求解器通常不会做好量化工作，所以要注意复杂性。

一般来说，对递归数据类型的推理并不是 SMT 求解器的强项。递归函数定义工具相对较新，对它们的支持很少，而且经常出错。任何使用递归数据类型的证明尝试都必须对任何有趣的属性使用归纳，而 SMT 求解器只是不进行开箱即用的归纳。您可能最好尝试使用 Isabelle、ACL2、Lean、HOL 等实际定理证明器。