量词消除 - 更多问题 [英] Quantifier Elimination - More questions

问题描述

非常感谢乔希和莱昂纳多回答上一个问题.

Many thanks Josh and Leonardo for answering the previous question.

我还有几个问题.

<1> 再举一个例子.

<1> Consider another example.

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

这有一个简单的解决方案 i > 0.(对于 Int 和 Real 情况)

This has a simple solution i > 0. (both for Int and Real case)

但是，当我尝试关注时，

However, when I tried following,

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

Z3 无法消除此处的量词.

Z3 Could not eliminate quantifier here.

但是，它可以消除真实情况.(当 i 和 k 都是实数时)对于整数，量词消去是否更难?

However, it could eliminate for a Real case. (when i and k are both reals) Is Quantifier Elimination more difficult for integers?

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

<2> I am using Z3 C API in my system. I am adding some non-linear constraints on Integers with quantifiers in my system. Z3 currently checks for satisfiability and gives me a correct model when the system is satisfiable.

我知道在消除量词之后，这些约束会减少为线性约束.

I know that after quantifier elimination, these constraints get reduced to linear constraints.

我认为 z3 在检查可满足性之前会自动进行量词消除.但是因为在上面的情况 1 中它不能这样做，我现在认为它通常会找到一个没有量词消除的模型.我说的对吗?

I thought that z3 does quantifier elimination automatically before checking satisfiability. But since, it couldn't do that in case 1 above, I now think, that it usually finds a model without Quantifier Elimination. Am I correct?

目前 z3 可以解决我系统中的约束.但它可能会在复杂系统上失败.在这种情况下，是否可以通过其他一些没有 z3 的方法进行量词消除，然后再向 z3 添加约束?

Currently z3 can solve the constraints in my system. But it may fail on complex systems. In such case, is it a good idea to do quantifier elimination by some other method without z3 and add constraints to z3 later?

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

<3> I can think of adding Real non-linear constraints instead of Integer non-linear constraints in my system. In that case, how can I enforce z3 to do Quantifier Elimination using C-API ?

<4> 最后，这是强制 z3 进行量词消除的好主意吗?或者它通常会更智能地找到模型而不进行量词消除?

<4> Finally, is this a good idea to enforce z3 to do Quantifier Elimination? Or it usually finds a model more intelligently without doing Quantifier Elimination?

谢谢.

推荐答案

<1> 非线性整数算法的理论不允许量词消去 (qe).此外，非线性整数算法的决策问题是不可判定的.

<1> The theory of nonlinear integer arithmetic does not admit quantifier elimination (qe). Moreover, the decision problem for nonlinear integer arithmetic is undecidable.

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

Recall that, Z3 has limited support for quantifier elimination of nonlinear real arithmetic formulas. The current procedure is based on virtual term substitution. Future versions, may have full support for nonlinear real arithmetic.

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

<2> Quantifier elimination is not enabled by default. The user must request it. Z3 may find models for satisfiable formulas even when quantifier elimination is not enabled. It uses a technique called model-based quantifier instantiation (MBQI). The Z3 online tutorial has several examples describing capabilities and limitations of this technique.

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

<3> You have to enable it when you create the Z3_context object. Any option that is set in the command line, can be provided during Z3_context object creation. Here is an example, that enables model construction and quantifier elimination:

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 上下文对象.

After that, ctx is pointing to a Z3 context object that supports model construction and quantifier elimination.

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

<4> The MBQI module is not complete even for the linear arithmetic fragment. The Z3 online tutorial describes the fragments it is complete. MBQI module is a good option for problems that contain uninterpreted functions. If your problems only use arithmetic, then quantifier elimination is usually better and more efficient. That being said, several problems can be quickly solved using MBQI.

这篇关于量词消除 - 更多问题的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！