解决大问题

Question

我从模板生成问题，由于问题的性质，我不得不依赖量词。现在，求解器只能找到非常简单（可满足）问题的实例。在许多情况下，查找“未饱和”是有效的。查找“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)