2

我正在尝试解决一个涉及命题可满足性（使用量词）和线性算术的问题。

这个问题我已经制定好了，Z3也能解决，但是时间长得不合理。

我一直试图通过指定战术来帮助 Z3，但我没有取得太大进展（我对逻辑理论一无所知）。

以下是一个高度简化的问题，它抓住了我要解决的问题的本质。有人可以提出建议吗？

我试图阅读像 Nelson Oppen 方法这样的东西，但是有很多不熟悉的符号，并且需要很长时间才能学习它。

另外，Z3 是否允许用户调整这些配置？最后，我如何在 z3py 中使用这些策略？

(declare-datatypes () ((newtype (item1) (item2) (item3))))

(declare-fun f (newtype newtype) Bool)

(declare-fun cost (newtype newtype) Real)

(assert (exists ((x newtype)(y newtype)) (f x y)))

(assert (forall ((x newtype)(y newtype)) (=> (f x y) (> (cost x y) 0))))

(assert (forall ((x newtype) (y newtype)) (<= (cost x y) 5)))

(check-sat)

(get-model)
4

1 回答 1

1

您编码的示例问题使用量化。Z3 使用特定过程来确定一类量化公式的可满足性，称为基于模型的量词实例化（mbqi 选项）。它通过将公式的无量词部分的候选模型扩展到量词的模型来工作。此过程可能涉及大量搜索。您可以通过使用选项 /st 运行 Z3 从搜索过程中提取统计信息，它将显示搜索过程的选定统计信息，并大致了解搜索过程中发生的情况。没有专门针对具有算术和量词的公式类别的特定策略组合（有一类公式使用位向量和量词，这些公式由此类公式的默认策略处理）。

我试图阅读像 Nelson Oppen 方法这样的东西，但是有很多不熟悉的符号，并且需要很长时间才能学习它。

这对于理解量词的搜索问题有点切题。

另外，Z3 是否允许用户调整这些配置？

是的，您可以从命令行配置 Z3。例如，您可以使用命令行禁用 MBQI：

z3 tt.smt2 -st smt.auto_config=false smt.mbqi=false

Z3 现在返回“未知”，因为执行选定实例化的较弱量词引擎将无法确定公式是否可满足。您可以按照“z3 -?”中的说明学习命令行选项。

最后，我如何在 z3py 中使用这些策略？

您可以使用 z3py 中的策略。z3.py 文件包含如何组合战术的简要信息。不过，我希望您的问题类别的难度确实与量词所涉及的搜索难度有关。在定理证明者发散的情况下，很容易提出带有量词的公式，因为这些类型的公式通常是高度不可判定的。

于 2013-12-12T17:28:37.400 回答