2

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

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

4

1 回答 1

2

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 中提供。

于 2011-09-09T14:38:36.477 回答