z3 - 获得量化布尔变量问题的模型

Question

我正在使用 Z3 来检查具有线性整数算术、未解释函数和布尔变量上的量词的逻辑中的可满足性。Z3 没有提供可满足问题的模型，我想这是因为量词（或我选择的逻辑：AUFLIA）。

除了自己实例化所有布尔变量之外，有没有办法让 Z3 为我提供此类问题的模型？

Answer 1

Z3 原则上可以决定这个片段。我说“原则上”是因为这个片段的决策问题的复杂性非常高。例如，它包含了 NEXPTIME 完整的 Bernays-Schönfinkel 片段（又名 EPR）。Z3可以决定的片段列表可以在以下位置找到：http ://rise4fun.com/z3/tutorial/guide

我们必须确保在 Z3 中启用了基于模型的量词实例化 (MBQI)。您可以使用命令行选项MBQI=true或 SMT2 命令执行此操作

(set-option :mbqi true)

Z3 对 MBQI 步骤的迭代次数也有一个阈值。MBQI_MAX_ITERATIONS=<value>我们可以通过使用命令行选项或命令来更改阈值

(set-option :mbqi-max-iterations 1000000)

对于每个 MBQI 步骤，我们可以要求 Z3 显示当前候选模型不满足哪些量词。选项MBQI_TRACE=true

话虽如此，我最近修复了您发送给我的 SMT2 脚本暴露的错误（崩溃）。该修复程序将在 Z3 3.2 中提供。