量词消除 - 更多问题

Question

非常感谢 Josh 和 Leonardo 回答了上一个问题。

我还有几个问题。

考虑另一个例子。

(exists k) i * k > = 4 and k > 1.

这有一个简单的解决方案 i > 0。（对于 Int 和 Real 情况）

但是，当我尝试关注时，

(declare-const i Int)
(assert (exists ((k Int)) (and (>= (* i k)  4) (> k 1))))
(apply (using-params qe :qe-nonlinear true))

Z3 此处无法消除量词。

但是，它可以消除真实案例。 （当 i 和 k 都是实数时） 整数的量词消除更难吗？

我在我的系统中使用 Z3 C API。我在我的系统中添加了一些带有量词的整数的非线性约束。 Z3 目前检查可满足性，并在系统可满足时给我一个正确的模型。

我知道，在消除量词之后，这些约束被简化为线性约束。

我认为 z3 在检查可满足性之前会自动进行量词消除。但是，由于在上面的案例 1 中它无法做到这一点，我现在认为，它通常会找到一个没有量词消除的模型。我说的对吗？

目前 z3 可以解决我系统中的限制。但它可能在复杂系统上失败。 在这种情况下，在没有 z3 的情况下通过其他方法进行量词消除并在稍后对 z3 添加约束是一个好主意吗？

我可以考虑在我的系统中添加 Real 非线性约束而不是 Integer 非线性约束。在这种情况下，我如何强制 z3 使用 C-API 进行量词消除？

最后，强制 z3 进行量词消除是个好主意吗？或者它通常不用量词消除就能更智能地找到模型？

谢谢。

Answer 1

非线性整数算术理论不允许量词消除（qe）。 此外，非线性整数运算的决策问题是不可判定的。

回想一下，Z3 对非线性实数算术公式的量词消除的支持有限。当前程序基于虚拟术语替换。未来的版本，可能会完全支持非线性实数运算。

默认情况下不启用量词消除。用户必须请求它。 即使未启用量词消除，Z3 也可以找到可满足公式的模型。 它使用一种称为基于模型的量词实例化 (MBQI) 的技术。 Z3 online tutorial 有几个示例描述了该技术的功能和限制。

您必须在创建 Z3_context 对象时启用它。 在命令行中设置的任何选项都可以在 Z3_context 对象创建期间提供。下面是一个示例，它支持模型构建和量词消除：

Z3_config cfg = Z3_mk_config();
Z3_context ctx;
Z3_set_param_value(cfg, "MODEL", "true");
Z3_set_param_value(cfg, "ELIM_QUANTIFIERS", "true");
Z3_set_param_value(cfg, "ELIM_NLARITH_QUANTIFIERS", "true");
ctx = mk_context_custom(cfg, throw_z3_error);
Z3_del_config(cfg);

之后，ctx 指向一个支持模型构建和量词消除的 Z3 上下文对象。

即使对于线性算术片段，MBQI 模块也不完整。 Z3在线教程描述了它完整的片段。 MBQI 模块对于包含未解释函数的问题是一个不错的选择。如果您的问题只使用算术，那么量词消除通常会更好、更有效。话虽如此，使用 MBQI 可以快速解决几个问题。