z3 - 为大问题获取 'sat'

Question

我从模板生成问题，由于问题的性质，我不得不依赖量词。现在，求解器只能找到非常简单(可满足)问题的实例。在许多情况下，寻找“unsat”是可行的。查找“sat”很少奏效。

问题在于，即使是像定义两个不相交的集合这样的简单事物也必须用一些非常讨厌的公式来表达:

(assert (! (disjoint_1 B A) :named a2 ))
(assert (! ; axiom for "disjoint_1"
    (forall ((A Rel1)(B Rel1)) (= 
        (disjoint_1 A B) 
        (forall ((a0 Atom)) (not (and (in_1 a0 A) (in_1 a0 B)))))) 
:named ax8)) 

( Find the full problem here )

为了找到一个实例，Z3 必须找到函数 in_1 的解释。所有其他功能都依赖于它。

到目前为止，我听到以下与我的问题相关的说法:

1. 每个量词都应该有一个模式
2. 如果存在任何无限模型，实例查找将不起作用

我无法在网络或文献中找到任何关于如何实现或避免这种情况的有用信息。所以我的问题仍然是:

如何有效地找到可满足公式的实例(使用 Z3)？我如何使用模式(如果有的话)实现这一目标？

Answer 1

Z3 4.x 使用两个主要引擎来处理量词:EMatching 和 MBQI(基于模型的量词实例化)。 EMatching 引擎仅对不可满足的实例有效。也就是说，它永远无法证明一个公式(包含量词)是可满足的。另一方面，MBQI 可以做到这一点。实际上，它可以决定很多有用的片段。 Z3 guide (量词部分)描述了其中的一些片段。也就是说，Z3 没有用于一阶逻辑的有限模型查找器(如 Paradox )。这是一个有用的功能，我们可能会在将来包含它。您消息中的示例可以使用 Z3 解决。你可以试试here .

关于模式，它们是 EMatching 引擎的“提示”。由于 EMatching 引擎无法表明问题是可满足的，因此它们不会真正提供帮助。对于可满足的实例，我们可以添加模式，因为我们不希望 EMatching 引擎通过生成太多实例来妨碍 MBQI 引擎；或者我们想通过断言量词的简单实例来急切地修剪搜索空间。我们还可以使用选项 (set-option :ematching false) 禁用 EMatching 引擎。

(declare-sort Rel1)
(declare-sort Atom)
(declare-fun disjoint_1 (Rel1 Rel1) Bool)
(declare-fun in_1 (Atom Rel1) Bool)
(declare-const A Rel1)
(declare-const B Rel1)

(assert (! (disjoint_1 B A) :named a2 ))
(assert (! ; axiom for "disjoint_1"
    (forall ((A Rel1)(B Rel1)) (= 
        (disjoint_1 A B) 
        (forall ((a0 Atom)) (not (and (in_1 a0 A) (in_1 a0 B)))))) 
:named ax8)) 

(check-sat)
(get-model)