3

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

（在这里找到完整的问题）

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

到目前为止，我听到了以下与我的问题有关的陈述：

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

我在网络或文献中找不到任何有用的信息来说明如何实现或避免这种情况。所以我的问题仍然存在：

如何有效地找到可满足公式的实例（使用 Z3）？我如何使用模式来实现这一点（如果有的话）？

4

1 回答 1

4

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

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

(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)
于 2012-10-23T14:31:47.667 回答