Z3中如何高效求解理论组合

Question

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

我已经制定了这个问题，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)

Answer 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 包含 关于如何组合战术的简要信息。 不过，我希望您的问题课的难度确实必须做到 与量词有关的搜索难度。摆姿势很容易 带有量词的公式，其中定理证明随着这些类型的公式而发散 通常是高度不确定的。